Def RootPairing.Base.height

Modification history

2025-07-17 18:28

Mathlib/LinearAlgebra/RootSystem/Base.lean

feat: add root system induction principle equivalent to connectedness of Dynkin diagram (#26965) …

Added RootPairing.Base.height View on Github →