chore: split BigOperators/Group

[BoltonBailey]

Splits Algebra/BigOperators/Group/* into Algebra/BigOperators/Group/* and Algebra/BigOperators/Monoid/*. Then also splits off a Algebra/BigOperators/Monoid/Fintype/ directory from Algebra/BigOperators/Monoid/Finset/ This has the benefit of:

• Removing a longFile linter violation
• The majority of lemmas/defs here use Monoid rather than Group, so they will now live in appropriately named directories.

---

[github-actions]

PR summary 20e7cba5ae

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.BigOperators.Group.List.Lemmas	403	383	-20 (-4.96%)
Mathlib.Data.List.Prime	427	425	-2 (-0.47%)
Mathlib.Data.Multiset.Bind	429	427	-2 (-0.47%)
Mathlib.Algebra.BigOperators.Ring.Multiset	471	469	-2 (-0.42%)
Mathlib.Data.PNat.Factors	532	530	-2 (-0.38%)
Mathlib.Data.Fintype.EquivFin	458	457	-1 (-0.22%)
Mathlib.Data.Nat.GCD.BigOperators	461	460	-1 (-0.22%)
Mathlib.Algebra.Regular.Pow	468	467	-1 (-0.21%)
Mathlib.Algebra.BigOperators.RingEquiv	472	471	-1 (-0.21%)
Mathlib.GroupTheory.Congruence.BigOperators	477	476	-1 (-0.21%)
Mathlib.Algebra.Group.Submonoid.Membership	499	498	-1 (-0.20%)
Mathlib.Algebra.Star.BigOperators	531	530	-1 (-0.19%)
Mathlib.Algebra.BigOperators.Option	537	536	-1 (-0.19%)
Mathlib.Data.Multiset.Fintype	537	536	-1 (-0.19%)
Mathlib.Data.Finset.NoncommProd	538	537	-1 (-0.19%)
Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite	539	538	-1 (-0.19%)
Mathlib.Data.Finsupp.BigOperators	540	539	-1 (-0.19%)
Mathlib.Algebra.Group.Pointwise.Set.BigOperators	541	540	-1 (-0.18%)
Mathlib.NumberTheory.Harmonic.Defs	541	540	-1 (-0.18%)
Mathlib.Algebra.BigOperators.GroupWithZero.Finset	542	541	-1 (-0.18%)
Mathlib.Data.Finset.Slice	543	542	-1 (-0.18%)
Mathlib.Combinatorics.SetFamily.Shatter	544	543	-1 (-0.18%)
Mathlib.Algebra.BigOperators.NatAntidiagonal	545	544	-1 (-0.18%)
Mathlib.Algebra.GradedMonoid	545	544	-1 (-0.18%)
Mathlib.Data.Rat.BigOperators	548	547	-1 (-0.18%)
Mathlib.Dynamics.BirkhoffSum.Basic	549	548	-1 (-0.18%)
Mathlib.GroupTheory.MonoidLocalization.Basic	551	550	-1 (-0.18%)
Mathlib.Order.Partition.Finpartition	551	550	-1 (-0.18%)
Mathlib.Algebra.Order.BigOperators.Group.Finset	558	557	-1 (-0.18%)
Mathlib.RingTheory.UniqueFactorizationDomain.Defs	559	558	-1 (-0.18%)
Mathlib.RingTheory.Prime	560	559	-1 (-0.18%)
Mathlib.Order.Filter.AtTopBot.BigOperators	561	560	-1 (-0.18%)
Mathlib.Algebra.Module.Submodule.LinearMap	562	561	-1 (-0.18%)
Mathlib.Algebra.BigOperators.Ring.Nat	569	568	-1 (-0.18%)
Mathlib.Data.Holor	574	573	-1 (-0.17%)
Mathlib.Algebra.Tropical.BigOperators	578	577	-1 (-0.17%)
Mathlib.Algebra.Group.EvenFunction	589	588	-1 (-0.17%)
Mathlib.Algebra.BigOperators.WithTop	590	589	-1 (-0.17%)
Mathlib.RingTheory.Multiplicity	614	613	-1 (-0.16%)
Mathlib.CategoryTheory.Preadditive.Basic	615	614	-1 (-0.16%)
Mathlib.RingTheory.HahnSeries.Addition	645	644	-1 (-0.16%)
Mathlib.Data.Nat.Factorial.DoubleFactorial	669	668	-1 (-0.15%)
Mathlib.Data.Nat.Fib.Basic	671	670	-1 (-0.15%)
Mathlib.CategoryTheory.Preadditive.FunctorCategory	674	673	-1 (-0.15%)
Mathlib.GroupTheory.QuotientGroup.Basic	676	675	-1 (-0.15%)
Mathlib.Algebra.Order.Rearrangement	694	693	-1 (-0.14%)
Mathlib.CategoryTheory.Preadditive.Biproducts	701	700	-1 (-0.14%)
Mathlib.RingTheory.Localization.Defs	710	709	-1 (-0.14%)
Mathlib.Algebra.BigOperators.Intervals	715	714	-1 (-0.14%)

Import changes for all files

Files	Import difference
There are 3618 files with changed transitive imports taking up over 159084 characters: this is too many to display!
You can run scripts/import_trans_difference.sh all locally to see the whole output.

---

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

---

Decrease in tech debt: (relative, absolute) = (1.00, 0.02)

Current number	Change	Type
41	-1	large files

Current commit 20e7cba5ae
Reference commit 5308324503

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