natCast_def — Mathlib

English

For every natural number n, the n-th natural cast into MonoidAlgebra R M equals the basis element at 1 with coefficient n, i.e., (n : MonoidAlgebra R M) = single (1_M) (n : R).

Русский

Для каждого натурального числа n отображение n в MonoidAlgebra R M равно базисному элементу с индекатором 1 и коэффициентом n: (n : MonoidAlgebra R M) = single (1_M) (n : R).

LaTeX

$$$ (n : \mathrm{MonoidAlgebra}\; R\; M) = \operatorname{single}(1_M) (n : R) $$$

Lean4

@[to_additive (dont_translate := R)]
theorem natCast_def (n : ℕ) : (n : MonoidAlgebra R M) = single (1 : M) (n : R) :=
  rfl

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