etaExpand_eq — Mathlib

English

For any matrix A, etaExpand A = A, i.e., expansion is identity for matrices of Fin indices under the stated encoding.

Русский

Для любой матрицы A, etaExpand A = A, то есть расширение есть тождество.

LaTeX

$$$\\eta\\mathrm{Expand} \\; A = A$$$

Lean4

/-- This can be used to prove
```lean
example (A : Matrix (Fin 2) (Fin 2) α) :
  A = !![A 0 0, A 0 1;
         A 1 0, A 1 1] :=
(etaExpand_eq _).symm
```
-/
theorem etaExpand_eq {m n} (A : Matrix (Fin m) (Fin n) α) : etaExpand A = A :=
  by
  simp_rw [etaExpand, FinVec.etaExpand_eq, Matrix.of]
    -- This to be in the above `simp_rw` before https://github.com/leanprover/lean4/pull/2644

  erw [Equiv.refl_apply]

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