The ZMod n-algebra structure on rings whose characteristic divides n

instance ZMod.instSubsingletonAlgebra (R : Type u_1) [Ring R] (p : ℕ) : Subsingleton (Algebra (ZMod p) R)

@[reducible, inline]

abbrev ZMod.algebra' (R : Type u_1) [Ring R] {n : ℕ} (m : ℕ) [CharP R m] (h : m ∣ n) : Algebra (ZMod n) R

The ZMod n-algebra structure on rings whose characteristic m divides n. See note [reducible non-instances].

Equations

• ZMod.algebra' R m h = { smul := fun (a : ZMod n) (r : R) => a.cast * r, algebraMap := ZMod.castHom h R, commutes' := ⋯, smul_def' := ⋯ }

@[reducible, inline]

abbrev ZMod.algebra (R : Type u_1) [Ring R] (p : ℕ) [CharP R p] : Algebra (ZMod p) R

The ZMod p-algebra structure on a ring of characteristic p. This is not an instance since it creates a diamond with Algebra.id. See note [reducible non-instances].

Equations

• ZMod.algebra R p = ZMod.algebra' R p ⋯