Commit 2024-03-02 15:57 17a99271

View on Github →

feat(LinearAlgebra/RootSystem/Defs): Properties of pairs of roots (#10666) Given a pair of roots, we can describe the "angle" between them using the pairing between root i and coroot j together with the reverse pairing. This PR adds language for describing the various cases.

Estimated changes

Modified Mathlib/LinearAlgebra/RootSystem/Basic.lean

added theorem RootPairing.IsOrthogonal.symm

added theorem RootPairing.IsOrthogonal_comm

added theorem RootPairing.coroot_root_eq_pairing

added theorem RootPairing.coxeterWeight_swap

deleted theorem RootPairing.eq_of_forall_coroot_root_eq

added theorem RootPairing.eq_of_pairing_pairing_eq_two

added theorem RootPairing.isCrystallographic_iff

added theorem RootPairing.isReduced_iff

added theorem RootPairing.pairing_same

added theorem RootPairing.reflection_apply_root

added theorem RootPairing.reflection_mul

added theorem RootPairing.root_coroot_eq_pairing

added theorem RootPairing.root_ne

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

added def RootPairing.IsOrthogonal

added def RootPairing.coxeterWeight

added def RootPairing.pairing