Commit 2025-03-31 15:58 041e230c

View on Github →

feat(RingTheory/Nilpotent): prepare exp calculations (#23423) Changes for IsNilpotent.exp calculations

Estimated changes

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

modified theorem LieDerivation.exp_apply

added theorem LieDerivation.exp_map_apply

Modified Mathlib/RingTheory/Nilpotent/Exp.lean

added theorem IsNilpotent.exp_smul_eq_sum