Mathlib Map

Theorems · Theorem · linear algebra

Matrix.ext_iff

∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M N : Matrix m n α}, (∀ (i : m) (j : n), M i j = N i j) ↔ M = N
Defined in
Mathlib.LinearAlgebra.Matrix.Defs
Cited by
18 results in Mathlib
Foundations
Depth 6 from the axioms · uses propext, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Matrix.ext · cited by 540Matrix.extMatrix.diagonal_injective · cited by 6Matrix.diagonal_injectiveMatrix.map_injective · cited by 5Matrix.map_injectiveMatrix.transpose_injective · cited by 2Matrix.transpose_injectiveMatrix.conjTranspose_mul_self_eq_zero · cited by 1Matrix.conjTranspose_mul_…Matrix.IsSymm.ext_iff · cited by 1IsSymm.ext_iffMatrix.diag_eq_of_commute_single · cited by 1Matrix.diag_eq_of_commute…Matrix.row_eq_zero_of_commute_single · cited by 1Matrix.row_eq_zero_of_com…Matrix.SpecialLinearGroup.ext_iff · cited by 1SpecialLinearGroup.ext_iffMatrix.col_eq_zero_of_commute_single · cited by 1Matrix.col_eq_zero_of_com…CategoryTheory.Mat.hom_ext · cited by 1Mat.hom_extPEquiv.toMatrix_injective · cited by 0PEquiv.toMatrix_injectivemulLeftLinearMap_eq_zero_iff · cited by 0mulLeftLinearMap_eq_zero_…Matrix.hadamard_self_eq_self_iff · cited by 0Matrix.hadamard_self_eq_s…Matrix.SpecialLinearGroup.toGL_mem_center_iff · cited by 0SpecialLinearGroup.toGL_m…Matrix · cited by 4303MatrixMatrix.ext_iffCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Matrixstatement and proof · cited by 4,303

Cited by18

Results whose statement or proof uses this declaration.