Commit 2025-04-09 10:11 6c7393e4

View on Github →

feat(LinearAlgebra/RootSystem): Generalize RootPairing.pairing_zero_iff (#23833) Generalize RootPairing.pairing_zero_iff

Estimated changes

Modified Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean

modified theorem RootPairing.Base.cartanMatrix_le_zero_of_ne

modified theorem RootPairing.Base.cartanMatrix_mem_of_ne

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

added theorem RootPairing.coxeterWeight_zero_iff_isOrthogonal

added theorem RootPairing.isFixedPt_reflection_perm_iff

added theorem RootPairing.isOrthogonal_iff_pairing_eq_zero

added theorem RootPairing.pairing_zero_iff'

added theorem RootPairing.pairing_zero_iff

added theorem RootPairing.reflection_perm_eq_iff_smul_coroot

added theorem RootPairing.reflection_perm_eq_iff_smul_root

added theorem RootPairing.reflection_perm_eq_of_pairing_eq_zero'

added theorem RootPairing.reflection_perm_eq_of_pairing_eq_zero

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

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

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

Modified Mathlib/LinearAlgebra/RootSystem/Reduced.lean

modified theorem RootPairing.pairingIn_neg_one_neg_four_iff

modified theorem RootPairing.pairingIn_one_four_iff

modified theorem RootPairing.pairing_neg_one_neg_four_iff

modified theorem RootPairing.pairing_one_four_iff

Modified Mathlib/LinearAlgebra/RootSystem/RootPositive.lean

modified theorem RootPairing.InvariantForm.apply_root_root_zero_iff

deleted theorem RootPairing.InvariantForm.coxeterWeight_zero_iff_isOrthogonal

deleted theorem RootPairing.InvariantForm.isOrthogonal_iff_pairing_eq_zero

deleted theorem RootPairing.InvariantForm.pairing_zero_iff