natCast_fin_three — Mathlib

English

For any natural n, the n-cast into a 3×3 matrix is the diagonal matrix with n on the diagonal in α.

Русский

Для любого натурального n отображение n в α в матрицу 3×3 даёт диагональную матрицу diag(n,n,n).

LaTeX

$$$\big(n:\mathbb{N}\big) \;\text{cast} = \begin{pmatrix} \uparrow n & 0 & 0 \\ 0 & \uparrow n & 0 \\ 0 & 0 & \uparrow n \end{pmatrix}$$$

Lean4

theorem natCast_fin_three (n : ℕ) : (n : Matrix (Fin 3) (Fin 3) α) = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] :=
  by
  ext i j
  fin_cases i <;> fin_cases j <;> rfl

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