Commit 2026-01-28 16:03 6c7f3746

View on Github →

feat(LinearAlgebra/BilinearForm): Harmonize definitions of "Nondegenerate" (#34110) Change the definitions of Matrix.Nondegenerate and LinearMap.BilinForm.Nondegenerate to require nondegeneracy on both sides (left-separating and right-separating), matching existing LinearMap.Nondegenerate. Zulip discussion: #mathlib4 > Nondegenerate bilinear / quadratic forms

Estimated changes

Modified Mathlib/Algebra/Lie/InvariantForm.lean

Modified Mathlib/Algebra/Lie/Killing.lean

Modified Mathlib/Algebra/Lie/Weights/Killing.lean

Modified Mathlib/FieldTheory/Finite/Trace.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Properties.lean

modified theorem LinearMap.BilinForm.Nondegenerate.flip

deleted def LinearMap.BilinForm.Nondegenerate

modified theorem LinearMap.BilinForm.dualBasis_dualBasis

modified theorem LinearMap.BilinForm.dualBasis_dualBasis_flip

modified theorem LinearMap.BilinForm.dualBasis_flip_dualBasis

modified theorem LinearMap.BilinForm.dualBasis_injective

modified theorem LinearMap.BilinForm.dualBasis_involutive

deleted theorem LinearMap.BilinForm.nonDegenerateFlip_iff

added theorem LinearMap.BilinForm.nondegenerate_flip_iff

deleted theorem LinearMap.BilinForm.nondegenerate_iff_ker_eq_bot

modified theorem LinearMap.BilinForm.toDual_def

Modified Mathlib/LinearAlgebra/Matrix/BilinearForm.lean

added theorem LinearMap.BilinForm.Nondegenerate.ofSeparatingLeft

added theorem LinearMap.BilinForm.Nondegenerate.ofSeparatingRight

added theorem LinearMap.BilinForm.SeparatingLeft.toMatrix'

added theorem LinearMap.BilinForm.SeparatingLeft.toMatrix

added theorem LinearMap.BilinForm.SeparatingRight.toMatrix'

added theorem LinearMap.BilinForm.SeparatingRight.toMatrix

added theorem LinearMap.BilinForm.nondegenerate_iff_ker_eq_bot

added theorem LinearMap.BilinForm.separatingLeft_toMatrix'_iff

added theorem LinearMap.BilinForm.separatingLeft_toMatrix_iff

added theorem LinearMap.BilinForm.separatingRight_toMatrix'_iff

added theorem LinearMap.BilinForm.separatingRight_toMatrix_iff

added theorem Matrix.SeparatingLeft.toBilin'

added theorem Matrix.SeparatingLeft.toBilin

added theorem Matrix.SeparatingRight.toBilin'

added theorem Matrix.SeparatingRight.toBilin

added theorem Matrix.separatingLeft_toBilin'_iff

added theorem Matrix.separatingLeft_toBilin_iff

added theorem Matrix.separatingRight_toBilin'_iff

added theorem Matrix.separatingRight_toBilin_iff

Modified Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean

added theorem Matrix.Nondegenerate.eq_zero_of_ortho'

modified theorem Matrix.Nondegenerate.eq_zero_of_ortho

added theorem Matrix.Nondegenerate.exists_not_ortho_of_ne_zero'

modified theorem Matrix.Nondegenerate.exists_not_ortho_of_ne_zero

added structure Matrix.Nondegenerate

deleted def Matrix.Nondegenerate

added def Matrix.SeparatingLeft

added def Matrix.SeparatingRight

modified theorem Matrix.eq_zero_of_mulVec_eq_zero

modified theorem Matrix.eq_zero_of_vecMul_eq_zero

modified theorem Matrix.nondegenerate_def

modified theorem Matrix.nondegenerate_of_det_ne_zero

added theorem Matrix.separatingLeft_def

added theorem Matrix.separatingRight_def

Modified Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean

added theorem LinearMap.Nondegenerate.toMatrix₂'

added theorem LinearMap.Nondegenerate.toMatrix₂

modified theorem LinearMap.SeparatingLeft.toMatrix₂'

modified theorem LinearMap.SeparatingLeft.toMatrix₂

added theorem LinearMap.SeparatingRight.toMatrix₂'

added theorem LinearMap.SeparatingRight.toMatrix₂

added theorem LinearMap.nondegenerate_iff_det_ne_zero

added theorem LinearMap.nondegenerate_of_det_ne_zero

added theorem LinearMap.nondegenerate_toLinearMap₂'_iff_det_ne_zero

added theorem LinearMap.nondegenerate_toLinearMap₂'_of_det_ne_zero'

deleted theorem LinearMap.nondegenerate_toMatrix_iff

modified theorem LinearMap.nondegenerate_toMatrix₂'_iff

added theorem LinearMap.nondegenerate_toMatrix₂_iff

modified theorem LinearMap.separatingLeft_iff_det_ne_zero

modified theorem LinearMap.separatingLeft_of_det_ne_zero

modified theorem LinearMap.separatingLeft_toLinearMap₂'_iff_det_ne_zero

modified theorem LinearMap.separatingLeft_toLinearMap₂'_of_det_ne_zero'

added theorem LinearMap.separatingLeft_toMatrix₂'_iff

added theorem LinearMap.separatingLeft_toMatrix₂_iff

added theorem LinearMap.separatingRight_iff_det_ne_zero

added theorem LinearMap.separatingRight_of_det_ne_zero

added theorem LinearMap.separatingRight_toLinearMap₂'_iff_det_ne_zero

added theorem LinearMap.separatingRight_toLinearMap₂'_of_det_ne_zero'

added theorem LinearMap.separatingRight_toMatrix₂'_iff

added theorem LinearMap.separatingRight_toMatrix₂_iff

modified theorem Matrix.Nondegenerate.toLinearMap₂'

modified theorem Matrix.Nondegenerate.toLinearMap₂

added theorem Matrix.SeparatingLeft.toLinearMap₂'

added theorem Matrix.SeparatingLeft.toLinearMap₂

added theorem Matrix.SeparatingRight.toLinearMap₂'

added theorem Matrix.SeparatingRight.toLinearMap₂

added theorem Matrix.nondegenerate_toLinearMap₂'_iff

added theorem Matrix.nondegenerate_toLinearMap₂'_iff_nondegenerate_toLinearMap₂

added theorem Matrix.nondegenerate_toLinearMap₂_iff

modified theorem Matrix.separatingLeft_toLinearMap₂'_iff

modified theorem Matrix.separatingLeft_toLinearMap₂'_iff_separatingLeft_toLinearMap₂

modified theorem Matrix.separatingLeft_toLinearMap₂_iff

added theorem Matrix.separatingRight_toLinearMap₂'_iff

added theorem Matrix.separatingRight_toLinearMap₂'_iff_separatingRight_toLinearMap₂

added theorem Matrix.separatingRight_toLinearMap₂_iff

Modified Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean

deleted theorem Matrix.exists_mulVec_eq_zero_iff'

deleted theorem Matrix.exists_mulVec_eq_zero_iff_aux

added theorem Matrix.separatingLeft_iff_det_ne_zero

added theorem Matrix.separatingRight_iff_det_ne_zero

Modified Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean

Modified Mathlib/LinearAlgebra/SesquilinearForm/Basic.lean

added theorem LinearMap.Nondegenerate.congr

added theorem LinearMap.SeparatingRight.congr

added theorem LinearMap.nondegenerate_congr_iff

added theorem LinearMap.separatingRight_congr_iff