Theorem RootPairing.posRootForm_rootFormIn_posDef

Modification history

2025-12-16 19:53
Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean
feat: miscellaneous lemmas about root systems (#32922) …
Added RootPairing.posRootForm_rootFormIn_posDefView on Github →