eta_fin_two — Mathlib

English

Let A be a 2×2 matrix over α. Then A is equal to the matrix whose entries are the corresponding entries of A, i.e. the 2×2 matrix built from A00, A01, A10, A11.

Русский

Пусть A — матрица 2×2 над α. Тогда A равно матрице, составленной из соответствующих элементов: A_{00}, A_{01}, A_{10}, A_{11}.

LaTeX

$$$A = \begin{pmatrix} A_{00} & A_{01} \\ A_{10} & A_{11} \end{pmatrix}$$$

Lean4

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

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