Theorem RootPairing.pairingIn_rat

Modification history

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