mathlib4 chore: Split `Algebra.Group.Center`

trafficstars

Additivise a few more lemmas. Unify inv_mem_center/inv_mem_center₀, div_mem_center/div_mem_center₀. Move the few remaining lemmas about GroupWithZero to a new file Algebra.GroupWithZero.Center. Do the same with Algebra.Group.Centralizer.

[x] depends on: #13030

May 19 '24 09:05 YaelDillies

- div_mem_center₀ - inv_mem_center₀

You can run this locally as follows

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

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

May 24 '24 20:05 github-actions[bot]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/center.20and.20centralizer

Jun 06 '24 13:06 Ruben-VandeVelde

Conclusion seems to be that it's fine to merge the files.

Jun 07 '24 18:06 YaelDillies

PR summary 47b3c1e856

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Group.Centralizer	230	0	-230 (-100.00%)
Mathlib.Algebra.Ring.Centralizer	235	234	-1 (-0.43%)
Mathlib.Algebra.GroupWithZero.Center	236	235	-1 (-0.42%)
Mathlib.GroupTheory.Subsemigroup.Centralizer	369	368	-1 (-0.27%)
Mathlib.Algebra.Star.Center	537	536	-1 (-0.19%)
Mathlib.RingTheory.NonUnitalSubsemiring.Basic	549	548	-1 (-0.18%)
Mathlib.Algebra.Ring.Subsemiring.Basic	568	567	-1 (-0.18%)
Mathlib.Algebra.Ring.CentroidHom	578	577	-1 (-0.17%)

Import changes for all files

Files	Import difference
Too many changes (2095)!

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

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

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

Jun 07 '24 18:06 github-actions[bot]

I think this is doing too much all at once, so I'll split off some changes the coming days

Jun 18 '24 09:06 Ruben-VandeVelde

This PR/issue depends on:

~~leanprover-community/mathlib4#13030~~
~~leanprover-community/mathlib4#13921~~
~~leanprover-community/mathlib4#13944~~
~~leanprover-community/mathlib4#14331~~ By Dependent Issues (🤖). Happy coding!