mathlib3

feat(analysis/calculus/fderiv/exp): derivative of `exp ℝ (A x)` in non-commutative rings

#19056

Open