natCast_fst — Mathlib

English

For every natural number n, the fst component of n acting as a multiplier is the scalar operator by n on A.

Русский

Для каждого натурального числа n функтор fst от n, рассматриваемого как элемент умножителя, равен линейному оператору умножения на n на A.

LaTeX

$$$ (n : \\mathcal{M}(\\mathbb{K}, A)).\\mathrm{fst} = n \\cdot \\mathrm{id}_A $$$

Lean4

theorem natCast_fst (n : ℕ) : (n : 𝓜(𝕜, A)).fst = n :=
  rfl

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