natCast_def — Mathlib

English

For AddMonoid End M, the natural cast of n ∈ ℕ to an endomorphism equals the action endomorphism given by n-fold addition.

Русский

Для End(M) действия натурального числа n равны соответствующему эндоморфизму, задаваемому n-разовым сложением.

LaTeX

$$$(n : \\mathbb{N}) \\text{ viewed as } (\\text{AddMonoidEnd } M) = \\text{toAddMonoidEnd } \\mathbb{N} M\\ n$$$

Lean4

theorem natCast_def (n : ℕ) : (↑n : AddMonoid.End M) = DistribMulAction.toAddMonoidEnd ℕ M n :=
  rfl

Похожие утверждения