toMatrix_injective — Mathlib

English

The map toMatrix is injective: distinct PEquivs yield distinct matrices.

Русский

Сюрьминг toMatrix инъективно: различные PEquiv дают разные матрицы.

LaTeX

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

Lean4

theorem toMatrix_injective [DecidableEq n] [MulZeroOneClass α] [Nontrivial α] :
    Function.Injective (@toMatrix m n α _ _ _) := by
  intro f g
  refine not_imp_not.1 ?_
  simp only [Matrix.ext_iff.symm, toMatrix_apply, PEquiv.ext_iff, not_forall, exists_imp]
  intro i hi
  use i
  rcases hf : f i with - | fi
  · rcases hg : g i with - | gi
    · rw [hf, hg] at hi; exact (hi rfl).elim
    · use gi
      simp
  · use fi
    simp [hf.symm, Ne.symm hi]

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