toEnd_natCast — Mathlib

English

For every natural number n, the endomorphism of CentroidHom α arising from n, when viewed as an endomorphism of α, is the map a ↦ n·a; equivalently, (n : CentroidHom α).toEnd equals the natural embedding of n into End α.

Русский

Для каждого натурального числа n соответствующий ему эндоморфизм CentroidHom α, рассматриваемый как эндоморфизм α, есть умножение на n: a ↦ n·a; то есть (n : CentroidHom α).toEnd совпадает с естественным вложением n в End α.

LaTeX

$$$ (n : CentroidHom \alpha).toEnd = \uparrow n $$$

Lean4

@[simp, norm_cast]
theorem toEnd_natCast (n : ℕ) : (n : CentroidHom α).toEnd = ↑n :=
  rfl

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