Commit 2025-03-02 14:09 cf215ba5

View on Github →

feat: define exponential of nilpotent elements of a ℚ-algebra (#22316) Define exponential map for algebras

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Nilpotent/Exp.lean

added theorem IsNilpotent.exp_add_of_commute

added theorem IsNilpotent.exp_eq_truncated

added theorem IsNilpotent.exp_of_nilpotent_is_unit

added theorem IsNilpotent.exp_zero_eq_one