perf: add AddMonoid shortcut instance for linear maps

[JovanGerb]

The hierarchy of classes is such that AddCommMonoid is not a direct parent of AddCommGroup. This means that when unifying an instance that comes from AddCommMonoid with one that comes from AddCommGroup, we end up having to go through the shared parent AddMonoid. Hence, it can be beneficial to have a separately defined AddMonoid instance.

It might be worth it to try to switch up the order of the parents of AddCommGroup/CommGroup in the extends clause, and see if that has beneficial effects. Though this will affect many things, and in particular won't interact well with the backward.respectTransparency mess that is going on at the moment.

---

[github-actions]

PR summary 08657ed7f8

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ addMonoid
+ instance : AddMonoid (ContinuousMultilinearMap R M₁ M₂) := fast_instance%
+ instance : AddMonoid (MultilinearMap R M₁ M₂) := fast_instance%
+ instance : AddMonoid (M₁ →SL[σ₁₂] M₂)

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 scripts/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
13074	1	backward.isDefEq

Current commit e6921ef955
Reference commit 08657ed7f8

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).

[JovanGerb]

!bench

[leanprover-radar]

Benchmark results for e6921ef against 08657ed are in! @JovanGerb

• ✅ build//instructions: -502.1G (-0.29%)

Large changes (1✅)

• ✅ build/module/Mathlib.Analysis.Analytic.IteratedFDeriv//instructions: -6.8G (-12.99%)

Medium changes (20✅)

• ✅ build/module/Mathlib.Algebra.Lie.TraceForm//instructions: -8.7G (-8.26%)
• ✅ build/module/Mathlib.Algebra.Lie.Weights.IsSimple//instructions: -6.3G (-6.32%)
• ✅ build/module/Mathlib.AlgebraicGeometry.Morphisms.Flat//instructions: -11.5G (-4.77%)
• ✅ build/module/Mathlib.Analysis.Calculus.ContDiff.Basic//instructions: -7.2G (-7.25%)
• ✅ build/module/Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries//instructions: -22.5G (-12.11%)
• ✅ build/module/Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno//instructions: -14.8G (-9.92%)
• ✅ build/module/Mathlib.Analysis.Calculus.ContDiff.RestrictScalars//instructions: -1.5G (-6.91%)
• ✅ build/module/Mathlib.Analysis.Calculus.FDeriv.Analytic//instructions: -17.0G (-8.74%)
• ✅ build/module/Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap//instructions: -10.6G (-9.78%)
• ✅ build/module/Mathlib.Analysis.InnerProductSpace.Adjoint//instructions: -30.0G (-9.18%)
• ✅ build/module/Mathlib.Analysis.InnerProductSpace.LinearMap//instructions: -8.3G (-8.62%)
• ✅ build/module/Mathlib.Analysis.Normed.Module.Multilinear.Curry//instructions: -19.3G (-13.00%)
• ✅ build/module/Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm//instructions: -9.7G (-9.26%)
• ✅ build/module/Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv//instructions: -14.7G (-12.17%)
• ✅ build/module/Mathlib.Geometry.Manifold.ContMDiff.NormedSpace//instructions: -12.0G (-10.49%)
• ✅ build/module/Mathlib.Geometry.Manifold.MFDeriv.NormedSpace//instructions: -14.3G (-10.31%)
• ✅ build/module/Mathlib.Geometry.Manifold.VectorBundle.Hom//instructions: -8.5G (-6.81%)
• ✅ build/module/Mathlib.Geometry.Manifold.VectorBundle.Riemannian//instructions: -7.1G (-5.81%)
• ✅ build/module/Mathlib.LinearAlgebra.Dual.Lemmas//instructions: -16.2G (-8.87%)
• ✅ build/module/Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence//instructions: -9.1G (-6.50%)

Small changes (40✅)

Too many entries to display here. View the full report on radar instead.

[JovanGerb]

The longest pole has shortened by 1.2% 🎉

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.