Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-11-17 10:36
e6a0ede3
View on Github →
feat: miscellaneous root system lemmas (
#29147
)
Estimated changes
Modified
Mathlib/LinearAlgebra/RootSystem/Defs.lean
added
theorem
RootPairing.coxeterWeight_flip
added
theorem
RootPairing.pairing_flip
Modified
Mathlib/LinearAlgebra/RootSystem/Finite/G2.lean
Modified
Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean
added
theorem
RootPairing.smul_coroot_eq_of_root_add_root_eq
Modified
Mathlib/LinearAlgebra/RootSystem/Reduced.lean