natCast_apply — Mathlib

English

For any natural number n, the endomorphism corresponding to n acts by n times the input: (n : End_R(M)) m = n · m.

Русский

Для любого натурального числа n соответствующий ему эндоморфизм действует как умножение на n: (n : End_R(M)) m = n · m.

LaTeX

$$$ (n : \mathrm{End}_R(M)) (m) = n \cdot m $$$

Lean4

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

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