English
For any ring R, there is a canonical ℤ-algebra structure on R, with the algebra map given by Int.castRingHom R and with the ℤ-action corresponding to ordinary integer multiplication.
Русский
Для любого кольца R существует каноническая ℤ-алгебраическая структура на R; отображение алгебры ℤ → R задано Int.castRingHom R, а действие целых на R соответствует обычному умножению на целые.
LaTeX
$$$\text{Algebra over }\mathbb{Z}\; R\;\text{with }\mathrm{algebraMap}_{\mathbb{Z}} R = \mathrm{Int.castRingHom\;} R.$$$
Lean4
/-- Ring ⥤ ℤ-Alg -/
instance (priority := 99) toIntAlgebra : Algebra ℤ R
where
commutes' := Int.cast_commute
smul_def' _ _ := zsmul_eq_mul _ _
algebraMap := Int.castRingHom R
