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

• (_ : Subsingleton (Algebra (ZMod p) R)) = (_ : Subsingleton (Algebra (ZMod p) R))

@[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 (_ : ∀ (a : ZMod n) (r : R), ZMod.cast a * r = r * ZMod.cast a) (_ : ∀ (a : ZMod n) (r : R), a • r = a • r)

@[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 (_ : p ∣ p)