Commit 2025-02-10 10:42 6ad6b20a

View on Github →

feat: a finite-dimensional Lie algebra with a irreducible faithful finite-dimensional trace-free representation is semisimple (#21614) Over a field of characteristic zero.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Lie/Abelian.lean

added theorem LieAlgebra.center_eq_bot

added theorem LieAlgebra.isFaithful_self_iff

added theorem LieModule.isFaithful_iff_ker_eq_bot

added theorem LieModule.ker_eq_bot

Modified Mathlib/Algebra/Lie/Derivation/Killing.lean

Modified Mathlib/Algebra/Lie/OfAssociative.lean

added theorem LieModule.ext_of_isFaithful

added theorem LieModule.isFaithful_iff'

added theorem LieModule.toEnd_eq_iff

added theorem LieModule.toEnd_eq_zero_iff

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

deleted theorem LieAlgebra.HasTrivialRadical.center_eq_bot

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

added theorem LieAlgebra.hasCentralRadical_of_radical_le

added theorem LieSubmodule.eq_top_of_isIrreducible

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

added theorem LieAlgebra.hasCentralRadical_and_of_isIrreducible_of_isFaithful

added theorem LieAlgebra.hasTrivialRadical_and_of_isIrreducible_of_isFaithful

Modified Mathlib/Algebra/Module/LinearMap/End.lean

added theorem Module.End.commute_id_left

added theorem Module.End.commute_id_right