Commit 2025-03-16 23:10 6bad32a5

View on Github →

feat: the exponential of nilpotent Lie algebra derivatation is an automorphism (#22607)

Estimated changes

Modified Mathlib/Algebra/Lie/Basic.lean

added def LieRing.toNonUnitalNonAssocRing

added theorem lie_sum

added theorem sum_lie

added theorem sum_lie_sum

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

added theorem LieDerivation.exp_apply

Modified Mathlib/Algebra/Lie/NonUnitalNonAssocAlgebra.lean

Modified Mathlib/RingTheory/Nilpotent/Exp.lean

added theorem IsNilpotent.exp_mul_exp_neg_self

added theorem IsNilpotent.exp_neg_mul_exp_self

added theorem IsNilpotent.exp_zero

deleted theorem IsNilpotent.exp_zero_eq_one