Theorem LinearMap.finrank_eq_of_isPerfPair

Modification history

2025-12-16 19:53
Mathlib/LinearAlgebra/PerfectPairing/Restrict.lean
feat: miscellaneous lemmas about root systems (#32922) …
Added LinearMap.finrank_eq_of_isPerfPairView on Github →