Commit 2025-08-11 08:45 9439afee

View on Github →

feat: the Geck Construction yields trace-free matrices (#27831) This will be used with LieAlgebra.hasTrivialRadical_of_isIrreducible_of_isFaithful (and a proof of irreducibility) to prove semisimplicity.

Estimated changes

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

added theorem LieAlgebra.trace_toEnd_eq_zero

Modified Mathlib/Data/Matrix/Mul.lean

added theorem Matrix.pow_col_eq_zero_of_le

added theorem Matrix.pow_row_eq_zero_of_le

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

added theorem RootPairing.GeckConstruction.isNilpotent_e

added theorem RootPairing.GeckConstruction.isNilpotent_f

added theorem RootPairing.GeckConstruction.trace_toEnd_eq_zero

modified theorem RootPairing.GeckConstruction.ω_mul_ω

Modified Mathlib/Order/ConditionallyCompleteLattice/Finset.lean

added theorem Finite.ciInf_le

added theorem Finite.le_ciSup

Modified Mathlib/RingTheory/Finiteness/Nilpotent.lean

added theorem Matrix.isNilpotent_iff

added theorem Matrix.isNilpotent_iff_forall_col

added theorem Matrix.isNilpotent_iff_forall_row

added theorem Matrix.isNilpotent_transpose_iff

Modified Mathlib/RingTheory/Nilpotent/Lemmas.lean

added theorem Matrix.isNilpotent_toLin'_iff