ofNat_fin_three — Mathlib

English

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

Русский

Для любого n с AtLeastTwo в 3×3 случае diag(ofNat(n), ofNat(n), ofNat(n)).

LaTeX

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

Lean4

theorem ofNat_fin_three (n : ℕ) [n.AtLeastTwo] :
    (ofNat(n) : Matrix (Fin 3) (Fin 3) α) = !![ofNat(n), 0, 0; 0, ofNat(n), 0; 0, 0, ofNat(n)] :=
  natCast_fin_three _

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