Commit 2025-02-14 13:43 c5d6ae91

View on Github →

feat: characterise linearly dependent roots of root pairings (#21851) And gather related results together in a new file.

Estimated changes

Modified Mathlib.lean

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

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

added theorem LinearIndependent.pair_symm_iff

Modified Mathlib/LinearAlgebra/RootSystem/BaseChange.lean

Modified Mathlib/LinearAlgebra/RootSystem/Basic.lean

deleted theorem RootPairing.coxeterWeight_ne_four_of_linearIndependent

deleted theorem RootPairing.infinite_of_linearIndependent_coxeterWeight_four

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

deleted def RootPairing.IsReduced

added theorem RootPairing.coroot_eq_neg_iff

added def RootPairing.indexNeg

deleted theorem RootPairing.isReduced_iff

modified theorem RootPairing.ne_zero'

modified theorem RootPairing.ne_zero

added theorem RootPairing.root_eq_neg_iff

Created Mathlib/LinearAlgebra/RootSystem/Reduced.lean

added def RootPairing.IsReduced

added theorem RootPairing.coxeterWeight_eq_four_iff_not_linearIndependent

added theorem RootPairing.coxeterWeight_ne_four_of_linearIndependent

added theorem RootPairing.infinite_of_linInd_coxeterWeight_four

added theorem RootPairing.isReduced_iff

added theorem RootPairing.linearIndependent_iff_coxeterWeight_ne_four

added theorem RootPairing.pairing_neg_one_neg_four_iff'

added theorem RootPairing.pairing_neg_one_neg_four_iff

added theorem RootPairing.pairing_neg_two_neg_two_iff

added theorem RootPairing.pairing_one_four_iff'

added theorem RootPairing.pairing_one_four_iff

added theorem RootPairing.pairing_smul_root_eq_of_not_linInd

added theorem RootPairing.pairing_two_two_iff