toMatrix_symm — Mathlib

English

The map toMatrix from PEquiv is injective: if two PEquivs have the same toMatrix entries, they are equal.

Русский

Отображение toMatrix из PEquiv инъективно: равенство матриц определяет PEquiv полностью.

LaTeX

$$$\\text{Injective}(\\mathrm{toMatrix})$$$

Lean4

theorem toMatrix_symm [DecidableEq m] [DecidableEq n] [Zero α] [One α] (f : m ≃. n) :
    (f.symm.toMatrix : Matrix n m α) = f.toMatrixᵀ := by
  ext
  simp only [transpose, mem_iff_mem f, toMatrix_apply]
  congr

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