Theorem RootPairing.infinite_of_linearly_independent_coxeterWeight_four

Modification history

2024-12-03 14:07
Mathlib/LinearAlgebra/RootSystem/Basic.lean
feat(LinearAlgebra/RootSystem/Finite): Coxeter weights are bounded above by 4 (#19343) …
Deleted RootPairing.infinite_of_linearly_independent_coxeterWeight_fourView on Github →
2024-08-10 20:14
Mathlib/LinearAlgebra/RootSystem/Basic.lean
feat (LinearAlgebra/RootSystem) : infinitely many roots when two are parallel (#15582) …
Added RootPairing.infinite_of_linearly_independent_coxeterWeight_fourView on Github →