Commit 2025-12-16 19:53 80eb32f8

View on Github →

feat: miscellaneous lemmas about root systems (#32922) These are useful when proving that a root system has a base.

Estimated changes

Modified Mathlib/LinearAlgebra/PerfectPairing/Restrict.lean

added theorem LinearMap.finrank_eq_of_isPerfPair

Modified Mathlib/LinearAlgebra/RootSystem/BaseChange.lean

Modified Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean

added theorem RootPairing.posRootForm_rootFormIn_posDef

Modified Mathlib/LinearAlgebra/RootSystem/IsValuedIn.lean

added theorem RootPairing.finrank_corootSpanIn

added theorem RootPairing.finrank_rootSpanIn

added theorem RootPairing.pairingIn_rat

added theorem RootPairing.toLinearMap_apply_apply_mem_range_algebraMap