English
For a ring R of characteristic p, there is a canonical ZMod p-algebra structure on R. This is the characteristic-p analogue of the previous construction, giving R a natural algebra structure over Z/pZ.
Русский
Для кольца R с характеристикой p существует каноническая ZMod p-алгебраическая структура на R. Это характер-п аналог конструкции, обеспечивающий R естественную структуру над Z/pZ.
LaTeX
$$$R \text{ имеет каноническую } (\mathbb{Z}/p\mathbb{Z})\text{-алгебру над R; соответствующее отображение } \mathbb{Z}/p\mathbb{Z} \to R \text{ задаётся редукцией } p.$$$
Lean4
/-- 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]. -/
abbrev algebra (p : ℕ) [CharP R p] : Algebra (ZMod p) R :=
algebra' R p dvd_rfl
