Def RootPairing.GeckConstruction.cartanSubalgebra

Modification history

2025-07-08 08:42

Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Basic.lean

feat: add induction principle for positive roots relative to a base of a root system (#26819)

Modified RootPairing.GeckConstruction.cartanSubalgebra View on Github →

2025-06-02 15:20

Mathlib/LinearAlgebra/RootSystem/GeckConstruction.lean

feat: implement Geck's construction of a Lie algebra associated to a root system with distinguished base (#25285)

Added RootPairing.GeckConstruction.cartanSubalgebra View on Github →