natCast_apply — Mathlib

English

Natural-numbers act on AddMonoid.End M by evaluation: (↑n : End(M)) m = n·m for all m in M, when M is AddCommMonoid.

Русский

Естественные числа действуют на AddMonoid.End M через отображение: (↑n : End(M)) m = n·m для всех m, когда M – AddCommMonoid.

LaTeX

$$$(\\uparrow n)(m) = n \\cdot m$ for all $m\\in M$; here $M$ is AddCommMonoid.$$

Lean4

/-- See also `AddMonoid.End.natCast_def`. -/
@[simp]
theorem natCast_apply [AddCommMonoid M] (n : ℕ) (m : M) : (↑n : AddMonoid.End M) m = n • m :=
  rfl

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