Commit 2025-07-08 00:25 350e70c6

View on Github →

feat: add lemma 3.5 from Geck (#26592) This is the statement that [eᵢ, fⱼ] = 0 if i ≠ j where eᵢ, fⱼ are generators of a simple Lie algebra associated to a root system. The immediate next task is to remove the [P.IsNotG2] assumption.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

Modified Mathlib/Data/Matrix/Mul.lean

Modified Mathlib/Data/Matrix/Notation.lean

added theorem injective_pair_iff_ne

Modified Mathlib/LinearAlgebra/RootSystem/Base.lean

added theorem RootPairing.Base.chainBotCoeff_eq_zero

added theorem RootPairing.Base.chainTopCoeff_eq_of_ne

added theorem RootPairing.Base.linearIndependent_pair_of_ne

Modified Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean

added theorem RootPairing.Base.cartanMatrix_apply_eq_zero_iff

added theorem RootPairing.Base.cartanMatrix_eq_neg_chainTopCoeff

Modified Mathlib/LinearAlgebra/RootSystem/Chain.lean

added theorem RootPairing.chainTopCoeff_of_add

Modified Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Basic.lean

modified theorem RootPairing.GeckConstruction.cartanSubalgebra_le_lieAlgebra

modified theorem RootPairing.GeckConstruction.isSl2Triple

added theorem RootPairing.GeckConstruction.lie_e_f_mul_ω

added theorem RootPairing.GeckConstruction.lie_e_f_ne

modified theorem RootPairing.GeckConstruction.lie_e_f_same

modified theorem RootPairing.GeckConstruction.lie_h_e

modified theorem RootPairing.GeckConstruction.lie_h_f

modified theorem RootPairing.GeckConstruction.lie_h_h

modified theorem RootPairing.GeckConstruction.ω_mul_e

modified theorem RootPairing.GeckConstruction.ω_mul_f

modified theorem RootPairing.GeckConstruction.ω_mul_h

Modified Mathlib/LinearAlgebra/RootSystem/GeckConstruction/Lemmas.lean

added theorem RootPairing.Base.root_sub_mem_iff_root_add_mem