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

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

Equations

• ⋯ = ⋯

@[reducible]

def 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 = let __src := ZMod.castHom h R; Algebra.mk __src ⋯ ⋯

@[reducible]

def 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 ⋯