Theorem RootPairing.rootSpan_eq_top_iff

Modification history

2025-01-09 09:30
Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean
feat: make spanning condition in `RootSystem` symmetric for roots and coroots. (#20564) …
Added RootPairing.rootSpan_eq_top_iffView on Github →