English
For rings of characteristic m divides n, there is a canonical algebra structure of ZMod n on R given by casting via castHom h: ZMod n → R, with smul defined by (a,r) ↦ cast a · r, and the scalar action commuting with the ring multiplication.
Русский
Для колец характеристик m, делящей n, существует каноническая структура ZMod n над R, задаваемая через отображение castHom и действие скаляров.
LaTeX
$$$$\\text{abbrev } \\text{algebra'}(h) : \\mathbb{Z}/n\\mathbb{Z} \\to \\operatorname{End}(R)$$$$
Lean4
/-- The `ZMod n`-algebra structure on rings whose characteristic `m` divides `n`.
See note [reducible non-instances]. -/
abbrev algebra' (h : m ∣ n) : Algebra (ZMod n) R
where
algebraMap := ZMod.castHom h R
smul := fun a r => cast a * r
commutes' := fun a r =>
show (cast a * r : R) = r * cast a
by
rcases ZMod.intCast_surjective a with ⟨k, rfl⟩
change ZMod.castHom h R k * r = r * ZMod.castHom h R k
rw [map_intCast, Int.cast_comm]
smul_def' := fun _ _ => rfl
