feat: for nilpotent derivations, exponential is multiplicative

[ocfnash]

---

Hacked together in final moments over lunch so may need polish.

Intended to help with #22607

[github-actions]

PR summary 6f700a4890

Import changes exceeding 2%

%	File
+25.45%	Mathlib.RingTheory.Nilpotent.Exp
+2.42%	Mathlib.RingTheory.TensorProduct.Basic

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.RingTheory.Nilpotent.Exp	829	1040	+211 (+25.45%)
Mathlib.RingTheory.TensorProduct.Basic	950	973	+23 (+2.42%)

Import changes for all files

Files	Import difference
35 files Mathlib.Algebra.Category.Ring.Epi Mathlib.Algebra.Module.FinitePresentation Mathlib.Algebra.Module.Presentation.Finite Mathlib.LinearAlgebra.BilinearForm.DualLattice Mathlib.LinearAlgebra.BilinearForm.Orthogonal Mathlib.LinearAlgebra.BilinearForm.Properties Mathlib.LinearAlgebra.BilinearForm.TensorProduct Mathlib.LinearAlgebra.Dual.Lemmas Mathlib.LinearAlgebra.PerfectPairing.Basic Mathlib.LinearAlgebra.RootSystem.Base Mathlib.LinearAlgebra.RootSystem.CartanMatrix Mathlib.LinearAlgebra.RootSystem.Defs Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas Mathlib.LinearAlgebra.RootSystem.Hom Mathlib.LinearAlgebra.RootSystem.OfBilinear Mathlib.LinearAlgebra.RootSystem.Reduced Mathlib.LinearAlgebra.RootSystem.RootPairingCat Mathlib.LinearAlgebra.RootSystem.RootPositive Mathlib.LinearAlgebra.TensorProduct.RightExactness Mathlib.LinearAlgebra.TensorProduct.Vanishing Mathlib.RingTheory.Bialgebra.MonoidAlgebra Mathlib.RingTheory.EssentialFiniteness Mathlib.RingTheory.FiniteStability Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra Mathlib.RingTheory.Ideal.Quotient.Index Mathlib.RingTheory.Localization.Algebra Mathlib.RingTheory.Localization.BaseChange Mathlib.RingTheory.MatrixPolynomialAlgebra Mathlib.RingTheory.MvPolynomial.Localization Mathlib.RingTheory.PolynomialAlgebra Mathlib.RingTheory.QuotSMulTop Mathlib.RingTheory.TensorProduct.Finite Mathlib.RingTheory.TensorProduct.MvPolynomial Mathlib.RingTheory.TensorProduct.Quotient	1
12 files Mathlib.Algebra.Algebra.Subalgebra.Centralizer Mathlib.Algebra.Azumaya.Defs Mathlib.Algebra.Azumaya.Matrix Mathlib.Algebra.Category.BialgebraCat.Basic Mathlib.Algebra.Category.HopfAlgebraCat.Basic Mathlib.LinearAlgebra.TensorProduct.Graded.External Mathlib.LinearAlgebra.TensorProduct.Graded.Internal Mathlib.LinearAlgebra.TensorProduct.Subalgebra Mathlib.RingTheory.Bialgebra.Basic Mathlib.RingTheory.Bialgebra.Equiv Mathlib.RingTheory.Bialgebra.Hom Mathlib.RingTheory.HopfAlgebra.Basic	10
Mathlib.RingTheory.IsTensorProduct	12
5 files Mathlib.Algebra.Module.Bimodule Mathlib.LinearAlgebra.TensorProduct.Opposite Mathlib.RingTheory.MatrixAlgebra Mathlib.RingTheory.TensorProduct.Basic Mathlib.RingTheory.TensorProduct.Pi	23
Mathlib.RingTheory.Nilpotent.Exp	211

---

Declarations diff

+ commute_exp_left_of_commute
+ exp_eq_sum
+ exp_mul_of_derivation
+ instance {R M N : Type*} [CommRing R] [AddCommGroup M] [AddCommGroup N]
+ lTensorAlgHom
+ map_exp
+ rTensorAlgHom
- exp_eq_truncated

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[ocfnash]

Note that Mathlib.RingTheory.Nilpotent.Exp is currently a leaf file so I claim the import increase is OK.

[ocfnash]

Thanks for the review. Out of time for today. WIP pushed up.