mathlib4 feat: define `AddConstEquiv`

[x] depends on: #9725
[x] depends on: #9724

Jan 13 '24 21:01 urkud

This PR/issue depends on:

~~leanprover-community/mathlib4#9725~~
~~leanprover-community/mathlib4#9724~~ By Dependent Issues (🤖). Happy coding!

Jan 23 '24 01:01 leanprover-community-mathlib4-bot

Should this be written in terms of VAdd instead? Then you could show that all affine equivalences are VAddConstEquivs

May 06 '24 09:05 eric-wieser

@eric-wieser The only application I have in mind is a lift of a circle map/homeomorphism to the real line. Do you have some applications of VAdd version in mind? I mean, some nontrivial result that will benefit from this generalization. If no, then I would prefer to postpone this generalization until we need it.

May 21 '24 19:05 urkud

PR summary f0f2b2adaa

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Algebra.AddConstMap.Equiv`	578

Declarations diff

+ AddConstEquiv + Simps.symm_apply + coe_toEquiv + equivUnits + ext + instDiv + instGroup + instInv + instMul + instOne + instPowInt + instPowNat + refl + refl_trans + self_trans_symm + symm + symm_refl + symm_symm + symm_trans_self + toAddConstMapHom + toEnd + toEquiv_inj + toEquiv_injective + toPerm + trans + trans_refl ++ instance {G H : Type*} [Add G] [Add H] {a : G} {b : H} :

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>

Jun 29 '24 19:06 github-actions[bot]

!bench

Jun 29 '24 20:06 urkud

Here are the benchmark results for commit d345bdf8beb24ee14049f12811c2ad279f0c718f. There were no significant changes against commit 03cf1129cb3dc60979585c23d29728cb6393e95c.