[EtienneC30]

Also add an abbrev that provides a monoid instance for a FunLike type satisfying (f * g) x = f (g x) and 1 x = x.

---

[github-actions]

PR summary 46d2f47f6f

Import changes exceeding 2%

%	File
+3.78%	Mathlib.Algebra.AddConstMap.Basic

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.AddConstMap.Basic	821	852	+31 (+3.78%)

Import changes for all files

Files	Import difference
Mathlib.Algebra.AddConstMap.Basic Mathlib.Algebra.AddConstMap.Equiv	31

---

Declarations diff (regex)

+ compMonoid
+ instance : IsMulApplyEqComp (G →+c[a, a] G)
+ instance : IsNPowApplyEqIterate (G →+c[a, a] G)
+ instance : IsOneApplyEqSelf (G →+c[a, a] G)
+ instance : Monoid (G →+c[a, a] G) := fast_instance% FunLike.compMonoid
+ instance {K : Type*} [VAdd K H] [VAddAssocClass K H H] : IsVAddApply K (G →+c[a, b] H)
- instance : Monoid (G →+c[a, a] G)

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 46d2f47).

• +5 new declarations
• −0 removed declarations

+AddConstMap.instIsMulApplyEqComp
+AddConstMap.instIsNPowApplyEqIterate
+AddConstMap.instIsOneApplyEqSelf
+AddConstMap.instIsVAddApply
+FunLike.compMonoid

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 46d2f47f6f
Reference commit 401d9e6852

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py 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).