Theorem RootPairing.finrank_rootSpanIn

Modification history

2026-01-15 19:06
Mathlib/LinearAlgebra/RootSystem/IsValuedIn.lean
feat: the rank of the ℤ-span of the roots of a root system is the dimension (#33846) …
Modified RootPairing.finrank_rootSpanInView on Github →
2025-12-16 19:53
Mathlib/LinearAlgebra/RootSystem/IsValuedIn.lean
feat: miscellaneous lemmas about root systems (#32922) …
Added RootPairing.finrank_rootSpanInView on Github →