Commit 2026-03-15 17:09 11fa0b4c

View on Github →

feat: add Ad.lean for collecting adjoint action properties (#36628) Add Ad.lean for collecting adjoint action properties

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Lie/AdjointAction/Basic.lean

added theorem LieAlgebra.ad_isSemisimple_of_isSemisimple

added theorem LieAlgebra.ad_nilpotent_of_nilpotent

added theorem LieAlgebra.commute_ad_of_commute

added theorem LieAlgebra.isNilpotent_ad_of_isNilpotent

added theorem LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad

Renamed Mathlib/Algebra/Lie/Derivation/AdjointAction.lean to Mathlib/Algebra/Lie/AdjointAction/Derivation.lean

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

Modified Mathlib/Algebra/Lie/Engel.lean

Modified Mathlib/Algebra/Lie/Nilpotent.lean

deleted theorem LieAlgebra.ad_nilpotent_of_nilpotent

deleted theorem LieAlgebra.isNilpotent_ad_of_isNilpotent

deleted theorem LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

added theorem Polynomial.aeval_op_apply