English
Let M be a module over the natural numbers, i.e. an AddCommMonoid with a ℕ-action. Then for every n ∈ ℕ and x ∈ M, the action of n on x agrees with the canonical n-fold addition: h.smul n x = n • x.
Русский
Пусть M — абелева моноида c действием по ℕ. Тогда для любого n ∈ ℕ и x ∈ M действие целого числа n на x совпадает с каноническим n-разовым сложением: h.smul n x = n • x.
LaTeX
$$$\\forall {M : \\text{Type*}} [\\text{AddCommMonoid } M] (h : \\text{Module } \\mathbb{N} M) (n : \\mathbb{N}) (x : M),\\ h.smul n x = n \\cdot x$$$
Lean4
/-- Convert back any exotic `ℕ`-smul to the canonical instance. This should not be needed since in
mathlib all `AddCommMonoid`s should normally have exactly one `ℕ`-module structure by design.
-/
theorem nat_smul_eq_nsmul (h : Module ℕ M) (n : ℕ) (x : M) : h.smul n x = n • x :=
Nat.cast_smul_eq_nsmul ..
