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