Commit 2025-03-14 11:29 8b48c438
View on Github →feat: for nilpotent derivations, exponential is multiplicative (#22875)
We prove that if D
is a nilpotent derivation of an algebra (not necessarily associative or unital) then exp D (x * y) = (exp D x) * (exp D y)
.
Note that I have not added a deprecation for IsNilpotent.exp_eq_truncated
since it is only 12 days old.