Commit 2025-06-02 15:20 ce1e4bec

View on Github →

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

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Lie/Semisimple/Lemmas.lean

deleted theorem LieAlgebra.hasTrivialRadical_and_of_isIrreducible_of_isFaithful

added theorem LieAlgebra.hasTrivialRadical_of_isIrreducible_of_isFaithful

Modified Mathlib/LinearAlgebra/RootSystem/Defs.lean

added theorem RootPairing.pairing_eq_add_of_root_eq_add

Created Mathlib/LinearAlgebra/RootSystem/GeckConstruction.lean

added def RootPairing.GeckConstruction.cartanSubalgebra

added theorem RootPairing.GeckConstruction.cartanSubalgebra_le_lieAlgebra

added def RootPairing.GeckConstruction.e

added def RootPairing.GeckConstruction.f

added def RootPairing.GeckConstruction.h

added theorem RootPairing.GeckConstruction.isSl2Triple

added def RootPairing.GeckConstruction.lieAlgebra

added theorem RootPairing.GeckConstruction.lie_e_f_same

added theorem RootPairing.GeckConstruction.lie_h_e

added theorem RootPairing.GeckConstruction.lie_h_f

added theorem RootPairing.GeckConstruction.lie_h_h

added def RootPairing.GeckConstruction.ω

added theorem RootPairing.GeckConstruction.ω_mul_e

added theorem RootPairing.GeckConstruction.ω_mul_f

added theorem RootPairing.GeckConstruction.ω_mul_h

added theorem RootPairing.GeckConstruction.ω_mul_ω

Modified Mathlib/LinearAlgebra/RootSystem/IsValuedIn.lean

added theorem RootPairing.pairingIn_eq_add_of_root_eq_add