ofNat_fin_two — Mathlib

English

For any n with n.AtLeastTwo, the matrix ofNat(n) in Fin 2 is the diagonal matrix with ofNat(n) on the diagonal.

Русский

Для любого n с условием AtLeastTwo, матрица ofNat(n) в размерности 2×2 равна диагональной матрице diag(ofNat(n), ofNat(n)).

LaTeX

$$$\mathrm{ofNat}(n) = \begin{pmatrix} \mathrm{ofNat}(n) & 0 \\ 0 & \mathrm{ofNat}(n) \end{pmatrix}$$$

Lean4

theorem ofNat_fin_two (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : Matrix (Fin 2) (Fin 2) α) = !![ofNat(n), 0; 0, ofNat(n)] :=
  natCast_fin_two _

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