English
For any semiring R, there is a canonical Algebra structure of ℕ on R, with algebra map given by the natural cast Nat → R and the scalar action given by multiplication by that cast.
Русский
Для любого полупрерывного кольца R существует каноническая структура алгебры над ℕ на R: алгебраическое отображение Nat → R задано естественным образом, а действие скаляров ℕ на R совпадает с умножением.
LaTeX
$$$\text{Nat-algebra structure on }R:\; \text{algebraMap}_{\mathbb{N},R} = \mathrm{Nat.castRingHom} \, R.$$$
Lean4
/-- Semiring ⥤ ℕ-Alg -/
instance (priority := 99) toNatAlgebra : Algebra ℕ R
where
commutes' := Nat.cast_commute
smul_def' _ _ := nsmul_eq_mul _ _
algebraMap := Nat.castRingHom R
