Theorem RootPairing.coxeterWeight_mem_set_of_isCrystallographic

Modification history

2024-12-09 13:51

Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean

feat: non-degeneracy of root pairing form without assuming ordered scalars (#19767) …

Modified RootPairing.coxeterWeight_mem_set_of_isCrystallographic View on Github →

2024-12-03 14:07

Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean

feat(LinearAlgebra/RootSystem/Finite): Coxeter weights are bounded above by 4 (#19343) …

Added RootPairing.coxeterWeight_mem_set_of_isCrystallographic View on Github →