Nondegenerate

📁 Source: Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean

Statistics

Metric	Count
Definitions Nondegenerate, SeparatingLeft, SeparatingRight	3
Theorems eq_zero_of_ortho, eq_zero_of_ortho', exists_not_ortho_of_ne_zero, exists_not_ortho_of_ne_zero', separatingLeft, separatingRight, eq_zero_of_mulVec_eq_zero, eq_zero_of_vecMul_eq_zero, nondegenerate_def, nondegenerate_of_det_ne_zero, separatingLeft_def, separatingRight_def	12
Total	15

Matrix

Definitions

Name	Category	Theorems
Nondegenerate 📖	CompData	19 math math: RootPairing.Base.cartanMatrixIn_nondegenerate, RootPairing.Base.cartanMatrix_nondegenerate, Nondegenerate.smul_iff, LinearMap.BilinForm.nondegenerate_toMatrix_iff, nondegenerate_of_det_ne_zero, nondegenerate_toBilin'_iff, nondegenerate_toBilin_iff, LinearMap.BilinForm.nondegenerate_toMatrix'_iff, nondegenerate_toLinearMap₂_iff, LinearMap.nondegenerate_toMatrix₂'_iff, Nondegenerate.of_det_ne_zero, LinearMap.nondegenerate_toMatrix₂_iff, nondegenerate_def, LinearMap.Nondegenerate.toMatrix₂', nondegenerate_toLinearMap₂'_iff, LinearMap.Nondegenerate.toMatrix₂, LinearMap.BilinForm.Nondegenerate.toMatrix', LinearMap.BilinForm.Nondegenerate.toMatrix, nondegenerate_iff_det_ne_zero
SeparatingLeft 📖	MathDef	15 math math: LinearMap.BilinForm.separatingLeft_toMatrix'_iff, separatingLeft_def, LinearMap.separatingLeft_toMatrix₂'_iff, LinearMap.BilinForm.SeparatingLeft.toMatrix', LinearMap.BilinForm.SeparatingLeft.toMatrix, LinearMap.SeparatingLeft.toMatrix₂, separatingLeft_toLinearMap₂'_iff, separatingLeft_toBilin'_iff, separatingLeft_iff_det_ne_zero, separatingLeft_toLinearMap₂_iff, Nondegenerate.separatingLeft, LinearMap.separatingLeft_toMatrix₂_iff, separatingLeft_toBilin_iff, LinearMap.SeparatingLeft.toMatrix₂', LinearMap.BilinForm.separatingLeft_toMatrix_iff
SeparatingRight 📖	MathDef	15 math math: LinearMap.SeparatingRight.toMatrix₂', separatingRight_toLinearMap₂'_iff, separatingRight_toLinearMap₂_iff, Nondegenerate.separatingRight, separatingRight_toBilin_iff, LinearMap.BilinForm.SeparatingRight.toMatrix, LinearMap.separatingRight_toMatrix₂'_iff, separatingRight_iff_det_ne_zero, LinearMap.BilinForm.separatingRight_toMatrix'_iff, LinearMap.BilinForm.separatingRight_toMatrix_iff, LinearMap.SeparatingRight.toMatrix₂, separatingRight_toBilin'_iff, LinearMap.separatingRight_toMatrix₂_iff, separatingRight_def, LinearMap.BilinForm.SeparatingRight.toMatrix'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_of_mulVec_eq_zero 📖	—	mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—	eq_zero_of_vecMul_eq_zero det_transpose vecMul_transpose
eq_zero_of_vecMul_eq_zero 📖	—	vecMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—	Nondegenerate.eq_zero_of_ortho nondegenerate_of_det_ne_zero dotProduct_mulVec zero_dotProduct
nondegenerate_def 📖	mathematical	—	Nondegenerate Finite.of_fintype Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Finite.of_fintype separatingLeft_def Nondegenerate.separatingLeft separatingRight_def Nondegenerate.separatingRight
nondegenerate_of_det_ne_zero 📖	mathematical	—	Nondegenerate Finite.of_fintype	—	Finite.of_fintype nondegenerate_def mulVec_cramer dotProduct_smul Algebra.to_smulCommClass dotProduct_single mul_one IsDomain.to_noZeroDivisors Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq dotProduct_mulVec vecMul_vecMul adjugate_mul Finset.sum_congr single_vecMul mul_ite MulZeroClass.mul_zero one_mul ite_mul MulZeroClass.zero_mul Finset.sum_ite_eq
separatingLeft_def 📖	mathematical	—	SeparatingLeft Finite.of_fintype Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Finite.of_fintype Lean.Meta.FastSubsingleton.elim Fintype.instFastSubsingleton
separatingRight_def 📖	mathematical	—	SeparatingRight Finite.of_fintype Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Finite.of_fintype Lean.Meta.FastSubsingleton.elim Fintype.instFastSubsingleton

Matrix.Nondegenerate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_of_ortho 📖	mathematical	Matrix.Nondegenerate Finite.of_fintype dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.mulVec MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	Pi.instZero	—	Finite.of_fintype Matrix.nondegenerate_def
eq_zero_of_ortho' 📖	mathematical	Matrix.Nondegenerate Finite.of_fintype dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NonUnitalNonAssocSemiring.toAddCommMonoid Matrix.mulVec MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	Pi.instZero	—	Finite.of_fintype Matrix.nondegenerate_def
exists_not_ortho_of_ne_zero 📖	—	Matrix.Nondegenerate Finite.of_fintype	—	—	Finite.of_fintype eq_zero_of_ortho
exists_not_ortho_of_ne_zero' 📖	—	Matrix.Nondegenerate Finite.of_fintype	—	—	Finite.of_fintype eq_zero_of_ortho'
separatingLeft 📖	mathematical	Matrix.Nondegenerate	Matrix.SeparatingLeft	—	—
separatingRight 📖	mathematical	Matrix.Nondegenerate	Matrix.SeparatingRight	—	—

---

← Back to Index