one_fin_three — Mathlib

English

The 3×3 identity matrix over α is the matrix with 1 on the diagonal and 0 elsewhere.

Русский

3×3 единичная матрица над α имеет единицы на диагонали и нули вне диагонали.

LaTeX

$$$1_{3} = \begin{pmatrix}1 & 0 & 0 \\ 0 & 1 & 0 \\ 0 & 0 & 1\end{pmatrix}$$$

Lean4

theorem one_fin_three : (1 : Matrix (Fin 3) (Fin 3) α) = !![1, 0, 0; 0, 1, 0; 0, 0, 1] :=
  by
  ext i j
  fin_cases i <;> fin_cases j <;> rfl

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