Theorems · Inductive type · linear algebra
Matrix.Nondegenerate
{m : Type u_1} →
{n : Type u_2} → {R : Type u_3} → [NonUnitalNonAssocSemiring R] → [Finite m] → [Finite n] → Matrix m n R → PropA matrix M is nondegenerate if it is both left-separating and right-separating.
See also Matrix.Nonsingular.
- Cited by
- 49 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Matrixstatement · cited by 4,303
- Finitestatement · cited by 3,029
- NonUnitalNonAssocSemiringstatement · cited by 1,081
Cited by56
Results whose statement or proof uses this declaration.
- Matrix.nondegenerate_iff_det_ne_zerostatement · cited by 13
- Matrix.Nondegenerate.separatingLeftstatement and proof · cited by 4
- Matrix.Nondegenerate.separatingRightstatement and proof · cited by 4
- Matrix.nondegenerate_toLinearMap₂'_iffstatement and proof · cited by 4
- LinearMap.BilinForm.nondegenerate_toMatrix_iffstatement · cited by 4
- LieAlgebra.Basis.linearIndependent_baseSuppproof · cited by 3
- Matrix.nondegenerate_defstatement · cited by 3
- Matrix.nondegenerate_toLinearMap₂_iffstatement and proof · cited by 3
- Matrix.Nondegenerate.of_det_mem_nonZeroDivisorsstatement · cited by 3
- LinearMap.nondegenerate_toMatrix₂'_iffstatement · cited by 2
- LinearMap.nondegenerate_toMatrix₂_iffstatement · cited by 2
- LieAlgebra.Basis.extproof · cited by 2