eta_fin_three — Mathlib

English

Let A be a 3×3 matrix over α. Then A is equal to the 3×3 matrix whose entries are the corresponding entries of A: A_{ij} for i,j ∈ {0,1,2}.

Русский

Пусть A — матрица 3×3 над α. Тогда A равно матрице, составленной из соответствующих элементов A_{ij} для i,j ∈ {0,1,2}.

LaTeX

$$$A = \begin{pmatrix} A_{00} & A_{01} & A_{02} \\ A_{10} & A_{11} & A_{12} \\ A_{20} & A_{21} & A_{22} \end{pmatrix}$$$

Lean4

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

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