chore: move MulDistribMulAction under Algebra.Group

[YaelDillies]

The motivation is that it is additivisable (even though it currently isn't) and is used in group theory files.

---

• depends on: chore(Algebra/Group/Action): group similar lemmas #21028

[github-actions]

PR summary 089d5fe02e

Import changes exceeding 2%

%	File
+99.48%	Mathlib.Algebra.Group.Action.End
+6.63%	Mathlib.Algebra.Group.Action.Pretransitive
+4.06%	Mathlib.GroupTheory.GroupAction.DomAct.Basic

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Group.Action.End	191	381	+190 (+99.48%)
Mathlib.Algebra.Group.Action.Basic	387	217	-170 (-43.93%)
Mathlib.Algebra.Group.Action.Pretransitive	196	209	+13 (+6.63%)
Mathlib.GroupTheory.GroupAction.DomAct.Basic	271	282	+11 (+4.06%)
Mathlib.GroupTheory.Subgroup.Centralizer	449	441	-8 (-1.78%)
Mathlib.GroupTheory.GroupAction.Defs	407	414	+7 (+1.72%)
Mathlib.Algebra.Group.Aut	383	389	+6 (+1.57%)
Mathlib.Algebra.BigOperators.GroupWithZero.Action	614	619	+5 (+0.81%)
Mathlib.Algebra.Group.Action.Faithful	192	193	+1 (+0.52%)
Mathlib.Algebra.Group.Action.TypeTags	195	196	+1 (+0.51%)

Import changes for all files

Files	Import difference
Mathlib.Algebra.Group.Action.Basic	-170
Mathlib.GroupTheory.GroupAction.Embedding	-116
3 files Mathlib.Algebra.AddTorsor Mathlib.GroupTheory.GroupAction.Support Mathlib.LinearAlgebra.AffineSpace.Basic	-100
3 files Mathlib.Algebra.Group.Pointwise.Set.Finite Mathlib.GroupTheory.Commutator.Basic Mathlib.GroupTheory.Subgroup.Centralizer	-8
5 files Mathlib.Algebra.Field.Action.ConjAct Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas Mathlib.Algebra.GroupWithZero.Action.ConjAct Mathlib.GroupTheory.Commutator.Finite Mathlib.GroupTheory.GroupAction.ConjAct	-7
Mathlib.Algebra.Ring.Action.ConjAct	-5
5 files Mathlib.Algebra.Tropical.BigOperators Mathlib.Data.Finsupp.SMulWithZero Mathlib.Dynamics.BirkhoffSum.Basic Mathlib.GroupTheory.Perm.List Mathlib.GroupTheory.Perm.Support	-2
307 files Mathlib.Algebra.BigOperators.Associated Mathlib.Algebra.BigOperators.Fin Mathlib.Algebra.BigOperators.Finsupp Mathlib.Algebra.BigOperators.Intervals Mathlib.Algebra.BigOperators.Pi Mathlib.Algebra.CharP.Lemmas Mathlib.Algebra.CharP.Reduced Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries Mathlib.Algebra.ContinuedFractions.Computation.Approximations Mathlib.Algebra.ContinuedFractions.Computation.Basic Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat Mathlib.Algebra.ContinuedFractions.Computation.Translations Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv Mathlib.Algebra.ContinuedFractions.Determinant Mathlib.Algebra.Field.Subfield.Defs Mathlib.Algebra.GeomSum Mathlib.Algebra.Group.Graph Mathlib.Algebra.Group.NatPowAssoc Mathlib.Algebra.Group.PNatPowAssoc Mathlib.Algebra.Group.Pointwise.Set.Card Mathlib.Algebra.Group.Subgroup.Finsupp Mathlib.Algebra.Group.Subgroup.Ker Mathlib.Algebra.Group.Subgroup.Lattice Mathlib.Algebra.Group.Subgroup.Map Mathlib.Algebra.Group.Subgroup.ZPowers.Basic Mathlib.Algebra.Group.Submonoid.Finsupp Mathlib.Algebra.Group.Submonoid.Membership Mathlib.Algebra.GroupPower.IterateHom Mathlib.Algebra.GroupWithZero.Action.Pi Mathlib.Algebra.GroupWithZero.Pointwise.Set.Card Mathlib.Algebra.Order.AbsoluteValue.Basic Mathlib.Algebra.Order.AbsoluteValue.Euclidean Mathlib.Algebra.Order.Archimedean.Basic Mathlib.Algebra.Order.Archimedean.Hom Mathlib.Algebra.Order.Archimedean.IndicatorCard Mathlib.Algebra.Order.Archimedean.Submonoid Mathlib.Algebra.Order.BigOperators.Ring.Finset Mathlib.Algebra.Order.CauSeq.Basic Mathlib.Algebra.Order.CauSeq.BigOperators Mathlib.Algebra.Order.CauSeq.Completion Mathlib.Algebra.Order.CompleteField Mathlib.Algebra.Order.Field.Basic Mathlib.Algebra.Order.Field.Power Mathlib.Algebra.Order.Field.Subfield Mathlib.Algebra.Order.Floor Mathlib.Algebra.Order.Group.Pointwise.Interval Mathlib.Algebra.Order.GroupWithZero.Action.Synonym Mathlib.Algebra.Order.Nonneg.Floor Mathlib.Algebra.Order.Round Mathlib.Algebra.PresentedMonoid.Basic Mathlib.Algebra.Regular.Pow Mathlib.Algebra.Ring.BooleanRing Mathlib.Algebra.Ring.Divisibility.Lemmas Mathlib.Algebra.Ring.Identities Mathlib.Algebra.Ring.Subring.Units Mathlib.AlgebraicTopology.CechNerve Mathlib.AlgebraicTopology.Quasicategory.Basic Mathlib.AlgebraicTopology.Quasicategory.Nerve Mathlib.AlgebraicTopology.Quasicategory.StrictSegal Mathlib.AlgebraicTopology.SimplexCategory Mathlib.AlgebraicTopology.SimplicialCategory.Basic Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject Mathlib.AlgebraicTopology.SimplicialNerve Mathlib.AlgebraicTopology.SimplicialObject.Basic Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal Mathlib.AlgebraicTopology.SimplicialObject.Split Mathlib.AlgebraicTopology.SimplicialSet.Basic Mathlib.AlgebraicTopology.SimplicialSet.Boundary Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat Mathlib.AlgebraicTopology.SimplicialSet.Horn Mathlib.AlgebraicTopology.SimplicialSet.KanComplex Mathlib.AlgebraicTopology.SimplicialSet.Monoidal Mathlib.AlgebraicTopology.SimplicialSet.Nerve Mathlib.AlgebraicTopology.SimplicialSet.Path Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal Mathlib.CategoryTheory.Comma.CardinalArrow Mathlib.CategoryTheory.Limits.SmallComplete Mathlib.CategoryTheory.Presentable.Basic Mathlib.CategoryTheory.Presentable.IsCardinalFiltered Mathlib.Combinatorics.Additive.AP.Three.Defs Mathlib.Combinatorics.Colex Mathlib.Combinatorics.Enumerative.Catalan Mathlib.Combinatorics.Enumerative.Composition Mathlib.Combinatorics.Enumerative.DyckWord Mathlib.Combinatorics.Enumerative.Partition Mathlib.Combinatorics.Schnirelmann Mathlib.Combinatorics.SetFamily.AhlswedeZhang Mathlib.Combinatorics.SetFamily.FourFunctions Mathlib.Combinatorics.SetFamily.KruskalKatona Mathlib.Combinatorics.SetFamily.LYM Mathlib.Combinatorics.SimpleGraph.Acyclic Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting Mathlib.Combinatorics.SimpleGraph.Density Mathlib.Combinatorics.SimpleGraph.Girth Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform Mathlib.Combinatorics.SimpleGraph.Triangle.Basic Mathlib.Combinatorics.SimpleGraph.Triangle.Counting Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite Mathlib.Computability.Ackermann Mathlib.Computability.DFA Mathlib.Computability.Encoding Mathlib.Computability.EpsilonNFA Mathlib.Computability.MyhillNerode Mathlib.Computability.NFA Mathlib.Data.Fin.Tuple.BubbleSortInduction Mathlib.Data.Fin.Tuple.NatAntidiagonal Mathlib.Data.Fin.Tuple.Reflection Mathlib.Data.Fin.Tuple.Sort Mathlib.Data.Finite.Card Mathlib.Data.Finite.Perm Mathlib.Data.Finset.Density Mathlib.Data.Fintype.Units Mathlib.Data.Int.CardIntervalMod Mathlib.Data.Int.Log Mathlib.Data.Matroid.Basic Mathlib.Data.Matroid.Circuit Mathlib.Data.Matroid.Closure Mathlib.Data.Matroid.Constructions Mathlib.Data.Matroid.Dual Mathlib.Data.Matroid.IndepAxioms Mathlib.Data.Matroid.Map Mathlib.Data.Matroid.Rank.Cardinal Mathlib.Data.Matroid.Restrict Mathlib.Data.Matroid.Sum Mathlib.Data.NNRat.BigOperators Mathlib.Data.NNRat.Floor Mathlib.Data.Nat.Cast.Order.Field Mathlib.Data.Nat.Choose.Central Mathlib.Data.Nat.Choose.Mul Mathlib.Data.Nat.Choose.Sum Mathlib.Data.Nat.Count Mathlib.Data.Nat.Digits Mathlib.Data.Nat.Factorial.BigOperators Mathlib.Data.Nat.Factorial.DoubleFactorial Mathlib.Data.Nat.Fib.Basic Mathlib.Data.Nat.Fib.Zeckendorf Mathlib.Data.Nat.Hyperoperation Mathlib.Data.Nat.Multiplicity Mathlib.Data.Nat.Nth Mathlib.Data.Nat.PartENat Mathlib.Data.Nat.Prime.Nth Mathlib.Data.Num.Prime Mathlib.Data.Ordmap.Ordset Mathlib.Data.PNat.Xgcd Mathlib.Data.Rat.BigOperators Mathlib.Data.Rat.Cardinal Mathlib.Data.Rat.Cast.CharZero Mathlib.Data.Rat.Cast.Defs Mathlib.Data.Rat.Cast.Lemmas Mathlib.Data.Rat.Cast.Order Mathlib.Data.Rat.Floor Mathlib.Data.Real.Archimedean Mathlib.Data.Real.Basic Mathlib.Data.Real.Sign Mathlib.Data.Set.Card Mathlib.Data.Sign Mathlib.Data.W.Cardinal Mathlib.Deprecated.Cardinal.Continuum Mathlib.Deprecated.Cardinal.Finite Mathlib.Deprecated.Cardinal.PartENat Mathlib.Dynamics.FixedPoints.Basic Mathlib.Dynamics.FixedPoints.Topology Mathlib.Dynamics.PeriodicPts.Defs Mathlib.GroupTheory.Coprod.Basic Mathlib.GroupTheory.FreeGroup.Basic Mathlib.GroupTheory.FreeGroup.IsFreeGroup Mathlib.GroupTheory.FreeGroup.Reduce Mathlib.GroupTheory.MonoidLocalization.Away Mathlib.GroupTheory.MonoidLocalization.Basic Mathlib.GroupTheory.MonoidLocalization.Cardinality Mathlib.GroupTheory.MonoidLocalization.Order Mathlib.GroupTheory.NoncommCoprod Mathlib.GroupTheory.OreLocalization.Cardinality Mathlib.GroupTheory.Perm.Basic Mathlib.GroupTheory.Perm.DomMulAct Mathlib.GroupTheory.Perm.Subgroup Mathlib.GroupTheory.Perm.ViaEmbedding Mathlib.MeasureTheory.MeasurableSpace.Card Mathlib.ModelTheory.Algebra.Field.Basic Mathlib.ModelTheory.Algebra.Ring.Basic Mathlib.ModelTheory.Basic Mathlib.ModelTheory.Bundled Mathlib.ModelTheory.Definability Mathlib.ModelTheory.DirectLimit Mathlib.ModelTheory.ElementaryMaps Mathlib.ModelTheory.ElementarySubstructures Mathlib.ModelTheory.Encoding Mathlib.ModelTheory.FinitelyGenerated Mathlib.ModelTheory.Fraisse Mathlib.ModelTheory.LanguageMap Mathlib.ModelTheory.PartialEquiv Mathlib.ModelTheory.Quotients Mathlib.ModelTheory.Semantics Mathlib.ModelTheory.Skolem Mathlib.ModelTheory.Substructures Mathlib.ModelTheory.Syntax Mathlib.NumberTheory.ADEInequality Mathlib.NumberTheory.FactorisationProperties Mathlib.NumberTheory.FrobeniusNumber Mathlib.NumberTheory.Harmonic.Defs Mathlib.NumberTheory.Padics.PadicNorm Mathlib.NumberTheory.Padics.PadicVal.Basic Mathlib.NumberTheory.Primorial Mathlib.Order.Category.OmegaCompletePartialOrder Mathlib.Order.CompletePartialOrder Mathlib.Order.Extension.Well Mathlib.Order.Filter.AtTopBot.Archimedean Mathlib.Order.Filter.AtTopBot.Floor Mathlib.Order.Filter.CardinalInter Mathlib.Order.Filter.Cocardinal Mathlib.Order.FixedPoints Mathlib.Order.Interval.Finset.Box Mathlib.Order.Interval.Set.IsoIoo Mathlib.Order.Monotone.MonovaryOrder Mathlib.Order.OmegaCompletePartialOrder Mathlib.RingTheory.ChainOfDivisors Mathlib.RingTheory.Coprime.Basic Mathlib.RingTheory.Coprime.Lemmas Mathlib.RingTheory.Nilpotent.Basic Mathlib.RingTheory.NonUnitalSubsemiring.Basic Mathlib.RingTheory.Radical Mathlib.RingTheory.UniqueFactorizationDomain.Basic Mathlib.RingTheory.UniqueFactorizationDomain.Finite Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity Mathlib.RingTheory.UniqueFactorizationDomain.Nat Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors Mathlib.SetTheory.Cardinal.Aleph Mathlib.SetTheory.Cardinal.Arithmetic Mathlib.SetTheory.Cardinal.Basic Mathlib.SetTheory.Cardinal.Cofinality Mathlib.SetTheory.Cardinal.Continuum Mathlib.SetTheory.Cardinal.CountableCover Mathlib.SetTheory.Cardinal.Divisibility Mathlib.SetTheory.Cardinal.ENat Mathlib.SetTheory.Cardinal.Finite Mathlib.SetTheory.Cardinal.HasCardinalLT Mathlib.SetTheory.Cardinal.SchroederBernstein Mathlib.SetTheory.Cardinal.ToNat Mathlib.SetTheory.Cardinal.UnivLE Mathlib.SetTheory.Game.Birthday Mathlib.SetTheory.Game.Domineering Mathlib.SetTheory.Game.Nim Mathlib.SetTheory.Game.Ordinal Mathlib.SetTheory.Game.Short Mathlib.SetTheory.Game.State Mathlib.SetTheory.Nimber.Basic Mathlib.SetTheory.Ordinal.Arithmetic Mathlib.SetTheory.Ordinal.Basic Mathlib.SetTheory.Ordinal.CantorNormalForm Mathlib.SetTheory.Ordinal.Enum Mathlib.SetTheory.Ordinal.Exponential Mathlib.SetTheory.Ordinal.FixedPointApproximants Mathlib.SetTheory.Ordinal.FixedPoint Mathlib.SetTheory.Ordinal.NaturalOps Mathlib.SetTheory.Ordinal.Notation Mathlib.SetTheory.Ordinal.Principal Mathlib.SetTheory.Ordinal.Rank Mathlib.SetTheory.Ordinal.Topology Mathlib.SetTheory.Surreal.Basic Mathlib.SetTheory.ZFC.Rank Mathlib.Tactic.Bound Mathlib.Tactic.CancelDenoms Mathlib.Tactic.Group Mathlib.Tactic.IntervalCases Mathlib.Tactic.Linarith.Frontend Mathlib.Tactic.Linarith Mathlib.Tactic.LinearCombination' Mathlib.Tactic.NormNum.DivMod Mathlib.Tactic.NormNum.Eq Mathlib.Tactic.NormNum.GCD Mathlib.Tactic.NormNum.Ineq Mathlib.Tactic.NormNum.Inv Mathlib.Tactic.NormNum.IsCoprime Mathlib.Tactic.NormNum.NatFib Mathlib.Tactic.NormNum.NatSqrt Mathlib.Tactic.NormNum.OfScientific Mathlib.Tactic.NormNum Mathlib.Tactic.Positivity.Finset Mathlib.Tactic.Positivity Mathlib.Tactic.Rify Mathlib.Tactic.Ring.Basic Mathlib.Tactic.Ring.Compare Mathlib.Tactic.Ring.PNat Mathlib.Tactic.Ring.RingNF Mathlib.Tactic.Ring Mathlib.Topology.ContinuousMap.Ordered Mathlib.Topology.Instances.Discrete Mathlib.Topology.Instances.Sign Mathlib.Topology.Order.Basic Mathlib.Topology.Order.DenselyOrdered Mathlib.Topology.Order.ExtendFrom Mathlib.Topology.Order.Filter Mathlib.Topology.Order.IntermediateValue Mathlib.Topology.Order.IsLUB Mathlib.Topology.Order.LeftRightLim Mathlib.Topology.Order.LeftRightNhds Mathlib.Topology.Order.MonotoneConvergence Mathlib.Topology.Order.Monotone Mathlib.Topology.Order.NhdsSet Mathlib.Topology.Order.ProjIcc Mathlib.Topology.Order.T5 Mathlib.Topology.UniformSpace.AbsoluteValue	-1
60 files Mathlib.Algebra.AddConstMap.Equiv Mathlib.Algebra.Category.BoolRing Mathlib.Algebra.Category.Grp.Basic Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup Mathlib.Algebra.Category.Grp.FiniteGrp Mathlib.Algebra.Category.Grp.ForgetCorepresentable Mathlib.Algebra.Category.Grp.Zero Mathlib.Algebra.Category.GrpWithZero Mathlib.Algebra.Category.MonCat.Adjunctions Mathlib.Algebra.Category.MonCat.Basic Mathlib.Algebra.Category.MonCat.Colimits Mathlib.Algebra.Category.MonCat.ForgetCorepresentable Mathlib.Algebra.Category.Ring.Basic Mathlib.Algebra.Category.Ring.Colimits Mathlib.Algebra.CharP.ExpChar Mathlib.Algebra.Field.Subfield.Basic Mathlib.Algebra.Group.Action.Faithful Mathlib.Algebra.Group.Action.Option Mathlib.Algebra.Group.Action.Pi Mathlib.Algebra.Group.Action.Sigma Mathlib.Algebra.Group.Action.Sum Mathlib.Algebra.Group.Action.TypeTags Mathlib.Algebra.Group.Action.Units Mathlib.Algebra.Group.Subgroup.Actions Mathlib.Algebra.GroupWithZero.Action.Faithful Mathlib.Algebra.Module.PointwisePi Mathlib.Algebra.Order.UpperLower Mathlib.Algebra.Quandle Mathlib.Algebra.Ring.Action.Group Mathlib.Algebra.Ring.AddAut Mathlib.Algebra.Ring.Aut Mathlib.Algebra.Ring.Subring.Basic Mathlib.Algebra.Ring.Subring.MulOpposite Mathlib.Algebra.Star.Basic Mathlib.Algebra.Star.BigOperators Mathlib.Algebra.Star.Center Mathlib.Algebra.Star.Pointwise Mathlib.Algebra.Star.Prod Mathlib.Algebra.Star.Rat Mathlib.Algebra.Star.StarRingHom Mathlib.CategoryTheory.Action.Basic Mathlib.CategoryTheory.Category.Grpd Mathlib.CategoryTheory.Limits.Shapes.SingleObj Mathlib.CategoryTheory.Monoidal.Internal.Types Mathlib.CategoryTheory.SingleObj Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1 Mathlib.Data.Set.Pointwise.Iterate Mathlib.Data.Set.Pointwise.SMul Mathlib.Data.Set.Pointwise.Support Mathlib.GroupTheory.ClassEquation Mathlib.GroupTheory.GroupAction.Basic Mathlib.GroupTheory.GroupAction.FixedPoints Mathlib.GroupTheory.GroupAction.FixingSubgroup Mathlib.GroupTheory.Subgroup.Center Mathlib.LinearAlgebra.Matrix.SemiringInverse Mathlib.Order.Filter.Pointwise Mathlib.RingTheory.NonUnitalSubring.Basic Mathlib.RingTheory.SimpleRing.Field Mathlib.SetTheory.Cardinal.Subfield Mathlib.Topology.Bornology.Absorbs	1
194 files Mathlib.Algebra.AddConstMap.Basic Mathlib.Algebra.BigOperators.Finprod Mathlib.Algebra.BigOperators.Module Mathlib.Algebra.Colimit.DirectLimit Mathlib.Algebra.Group.ForwardDiff Mathlib.Algebra.Homology.Linear Mathlib.Algebra.Module.LinearMap.End Mathlib.Algebra.Module.LinearMap.Rat Mathlib.Algebra.Module.Rat Mathlib.Algebra.Order.Floor.Div Mathlib.Algebra.Order.Module.Algebra Mathlib.Algebra.Order.Module.Pointwise Mathlib.Algebra.Order.Module.Rat Mathlib.Algebra.Squarefree.Basic Mathlib.AlgebraicTopology.MooreComplex Mathlib.CategoryTheory.Adhesive Mathlib.CategoryTheory.CofilteredSystem Mathlib.CategoryTheory.EffectiveEpi.Extensive Mathlib.CategoryTheory.Extensive Mathlib.CategoryTheory.Idempotents.SimplicialObject Mathlib.CategoryTheory.Linear.LinearFunctor Mathlib.CategoryTheory.Monoidal.Linear Mathlib.CategoryTheory.Monoidal.Subcategory Mathlib.CategoryTheory.Quotient.Linear Mathlib.CategoryTheory.Sites.Coherent.Basic Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology Mathlib.CategoryTheory.Sites.Coherent.Comparison Mathlib.CategoryTheory.Sites.Coherent.Equivalence Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves Mathlib.CategoryTheory.Sites.Coherent.RegularTopology Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit Mathlib.CategoryTheory.Sites.Coherent.SheafComparison Mathlib.CategoryTheory.Sites.ConstantSheaf Mathlib.CategoryTheory.Sites.DenseSubsite.Basic Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv Mathlib.CategoryTheory.Sites.EpiMono Mathlib.CategoryTheory.Sites.Equivalence Mathlib.CategoryTheory.Sites.LeftExact Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.CategoryTheory.Sites.Pullback Mathlib.CategoryTheory.Sites.Spaces Mathlib.CategoryTheory.Sites.Subsheaf Mathlib.Combinatorics.Hall.Basic Mathlib.Combinatorics.SimpleGraph.Ends.Defs Mathlib.Combinatorics.SimpleGraph.Ends.Properties Mathlib.Combinatorics.SimpleGraph.Finsubgraph Mathlib.Combinatorics.SimpleGraph.Regularity.Energy Mathlib.Data.DFinsupp.Lex Mathlib.Data.DFinsupp.Order Mathlib.Data.Finsupp.AList Mathlib.Data.Finsupp.Antidiagonal Mathlib.Data.Finsupp.Basic Mathlib.Data.Finsupp.Multiset Mathlib.Data.Finsupp.Order Mathlib.Data.Finsupp.PWO Mathlib.Data.Finsupp.Pointwise Mathlib.Data.Holor Mathlib.Data.Int.AbsoluteValue Mathlib.Data.Matrix.CharP Mathlib.Data.Nat.Choose.Factorization Mathlib.Data.Nat.Factorization.Basic Mathlib.Data.Nat.Factorization.Defs Mathlib.Data.Nat.Factorization.Induction Mathlib.Data.Nat.Factorization.PrimePow Mathlib.Data.Nat.Factorization.Root Mathlib.Data.Nat.Squarefree Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits Mathlib.Geometry.RingedSpace.PresheafedSpace Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.Geometry.RingedSpace.Stalks Mathlib.NumberTheory.MaricaSchoenheim Mathlib.NumberTheory.SmoothNumbers Mathlib.RingTheory.LocalRing.Subring Mathlib.RingTheory.Localization.Defs Mathlib.RingTheory.Localization.Integer Mathlib.RingTheory.OreLocalization.Ring Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid Mathlib.Topology.Algebra.Constructions Mathlib.Topology.Algebra.InfiniteSum.Defs Mathlib.Topology.Algebra.Order.Support Mathlib.Topology.Algebra.Support Mathlib.Topology.Baire.LocallyCompactRegular Mathlib.Topology.Category.CompHausLike.Basic Mathlib.Topology.Category.CompHausLike.EffectiveEpi Mathlib.Topology.Category.CompHausLike.Limits Mathlib.Topology.Category.CompHausLike.SigmaComparison Mathlib.Topology.Category.FinTopCat Mathlib.Topology.Category.Sequential Mathlib.Topology.Category.TopCat.Adjunctions Mathlib.Topology.Category.TopCat.Basic Mathlib.Topology.Category.TopCat.EffectiveEpi Mathlib.Topology.Category.TopCat.EpiMono Mathlib.Topology.Category.TopCat.Limits.Basic Mathlib.Topology.Category.TopCat.Limits.Cofiltered Mathlib.Topology.Category.TopCat.Limits.Konig Mathlib.Topology.Category.TopCat.Limits.Products Mathlib.Topology.Category.TopCat.Limits.Pullbacks Mathlib.Topology.Category.TopCat.OpenNhds Mathlib.Topology.Category.TopCat.Opens Mathlib.Topology.Category.TopCat.Yoneda Mathlib.Topology.Category.UniformSpace Mathlib.Topology.ClopenBox Mathlib.Topology.CompactOpen Mathlib.Topology.Compactification.OnePoint Mathlib.Topology.Compactness.Paracompact Mathlib.Topology.Constructible Mathlib.Topology.ContinuousMap.Basic Mathlib.Topology.ContinuousMap.CocompactMap Mathlib.Topology.ContinuousMap.Interval Mathlib.Topology.ContinuousMap.SecondCountableSpace Mathlib.Topology.ContinuousMap.Sigma Mathlib.Topology.ContinuousMap.T0Sierpinski Mathlib.Topology.Covering Mathlib.Topology.DiscreteQuotient Mathlib.Topology.ExtremallyDisconnected Mathlib.Topology.FiberBundle.Basic Mathlib.Topology.FiberBundle.Constructions Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle Mathlib.Topology.FiberBundle.Trivialization Mathlib.Topology.FiberPartition Mathlib.Topology.Gluing Mathlib.Topology.Hom.Open Mathlib.Topology.Homeomorph Mathlib.Topology.IsLocalHomeomorph Mathlib.Topology.JacobsonSpace Mathlib.Topology.KrullDimension Mathlib.Topology.LocalAtTarget Mathlib.Topology.LocallyConstant.Basic Mathlib.Topology.Maps.Proper.Basic Mathlib.Topology.Maps.Proper.UniversallyClosed Mathlib.Topology.NoetherianSpace Mathlib.Topology.Order.Category.AlexDisc Mathlib.Topology.Order.Compact Mathlib.Topology.Order.LawsonTopology Mathlib.Topology.Order.LowerUpperTopology Mathlib.Topology.Order.MonotoneContinuity Mathlib.Topology.Order.Rolle Mathlib.Topology.Order.ScottTopology Mathlib.Topology.Order.UpperLowerSetTopology Mathlib.Topology.PartialHomeomorph Mathlib.Topology.QuasiSeparated Mathlib.Topology.Sequences Mathlib.Topology.Sets.Closeds Mathlib.Topology.Sets.Compacts Mathlib.Topology.Sets.Opens Mathlib.Topology.Sets.Order Mathlib.Topology.Sheaves.Forget Mathlib.Topology.Sheaves.Functors Mathlib.Topology.Sheaves.Limits Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Topology.Sheaves.PUnit Mathlib.Topology.Sheaves.PresheafOfFunctions Mathlib.Topology.Sheaves.Presheaf Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.Topology.Sheaves.SheafCondition.Sites Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.Topology.Sheaves.Sheaf Mathlib.Topology.Sheaves.Sheafify Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.Sheaves.Stalks Mathlib.Topology.Sober Mathlib.Topology.Specialization Mathlib.Topology.Spectral.Hom Mathlib.Topology.UniformSpace.AbstractCompletion Mathlib.Topology.UniformSpace.Ascoli Mathlib.Topology.UniformSpace.Cauchy Mathlib.Topology.UniformSpace.CompactConvergence Mathlib.Topology.UniformSpace.CompleteSeparated Mathlib.Topology.UniformSpace.Completion Mathlib.Topology.UniformSpace.Equicontinuity Mathlib.Topology.UniformSpace.Equiv Mathlib.Topology.UniformSpace.HeineCantor Mathlib.Topology.UniformSpace.Pi Mathlib.Topology.UniformSpace.UniformConvergenceTopology Mathlib.Topology.UniformSpace.UniformConvergence Mathlib.Topology.UniformSpace.UniformEmbedding	2
133 files Mathlib.Algebra.Algebra.Defs Mathlib.Algebra.Algebra.Field Mathlib.Algebra.Group.Action.Opposite Mathlib.Algebra.Group.Action.Prod Mathlib.Algebra.Group.ConjFinite Mathlib.Algebra.Group.EvenFunction Mathlib.Algebra.Group.Subgroup.Finite Mathlib.Algebra.Group.Submonoid.Operations Mathlib.Algebra.GroupWithZero.Action.Opposite Mathlib.Algebra.GroupWithZero.Action.Units Mathlib.Algebra.GroupWithZero.Units.Lemmas Mathlib.Algebra.Homology.Additive Mathlib.Algebra.Homology.Augment Mathlib.Algebra.Homology.CommSq Mathlib.Algebra.Homology.DifferentialObject Mathlib.Algebra.Homology.Double Mathlib.Algebra.Homology.Embedding.Boundary Mathlib.Algebra.Homology.Embedding.Restriction Mathlib.Algebra.Homology.Functor Mathlib.Algebra.Homology.HomologicalBicomplex Mathlib.Algebra.Homology.HomologicalComplexBiprod Mathlib.Algebra.Homology.HomologicalComplexLimits Mathlib.Algebra.Homology.HomologicalComplex Mathlib.Algebra.Homology.ImageToKernel Mathlib.Algebra.Homology.ShortComplex.Abelian Mathlib.Algebra.Homology.Single Mathlib.Algebra.Homology.Square Mathlib.Algebra.ModEq Mathlib.Algebra.Module.Basic Mathlib.Algebra.Module.Equiv.Defs Mathlib.Algebra.Module.Equiv.Opposite Mathlib.Algebra.Module.LinearMap.Defs Mathlib.Algebra.Module.LinearMap.Prod Mathlib.Algebra.Module.ULift Mathlib.Algebra.NoZeroSMulDivisors.Defs Mathlib.Algebra.NoZeroSMulDivisors.Pi Mathlib.Algebra.NoZeroSMulDivisors.Prod Mathlib.Algebra.Order.Field.Pointwise Mathlib.Algebra.Ring.Semireal.Defs Mathlib.Algebra.Ring.Subsemiring.Basic Mathlib.Algebra.Ring.Subsemiring.MulOpposite Mathlib.Algebra.Ring.SumsOfSquares Mathlib.Algebra.SMulWithZero Mathlib.Algebra.Tropical.Basic Mathlib.Algebra.Tropical.Lattice Mathlib.CategoryTheory.Abelian.Basic Mathlib.CategoryTheory.Abelian.FunctorCategory Mathlib.CategoryTheory.Abelian.NonPreadditive Mathlib.CategoryTheory.Abelian.Subobject Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems Mathlib.CategoryTheory.Dialectica.Monoidal Mathlib.CategoryTheory.Generator.Basic Mathlib.CategoryTheory.Generator.Indization Mathlib.CategoryTheory.Generator.Presheaf Mathlib.CategoryTheory.Generator.Sheaf Mathlib.CategoryTheory.Idempotents.Basic Mathlib.CategoryTheory.Idempotents.Biproducts Mathlib.CategoryTheory.Idempotents.FunctorCategories Mathlib.CategoryTheory.Idempotents.FunctorExtension Mathlib.CategoryTheory.Idempotents.HomologicalComplex Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi Mathlib.CategoryTheory.Idempotents.Karoubi Mathlib.CategoryTheory.Linear.Basic Mathlib.CategoryTheory.Linear.FunctorCategory Mathlib.CategoryTheory.Localization.SmallShiftedHom Mathlib.CategoryTheory.Monoidal.Preadditive Mathlib.CategoryTheory.Noetherian Mathlib.CategoryTheory.Preadditive.AdditiveFunctor Mathlib.CategoryTheory.Preadditive.Basic Mathlib.CategoryTheory.Preadditive.Biproducts Mathlib.CategoryTheory.Preadditive.EilenbergMoore Mathlib.CategoryTheory.Preadditive.EndoFunctor Mathlib.CategoryTheory.Preadditive.FunctorCategory Mathlib.CategoryTheory.Preadditive.LeftExact Mathlib.CategoryTheory.Quotient.Preadditive Mathlib.CategoryTheory.Shift.InducedShiftSequence Mathlib.CategoryTheory.Shift.Pullback Mathlib.CategoryTheory.Shift.ShiftSequence Mathlib.CategoryTheory.Shift.ShiftedHom Mathlib.CategoryTheory.Simple Mathlib.CategoryTheory.Sites.Adjunction Mathlib.CategoryTheory.Sites.Canonical Mathlib.CategoryTheory.Sites.CartesianClosed Mathlib.CategoryTheory.Sites.ChosenFiniteProducts Mathlib.CategoryTheory.Sites.CompatiblePlus Mathlib.CategoryTheory.Sites.CompatibleSheafification Mathlib.CategoryTheory.Sites.ConcreteSheafification Mathlib.CategoryTheory.Sites.Continuous Mathlib.CategoryTheory.Sites.CoverLifting Mathlib.CategoryTheory.Sites.CoverPreserving Mathlib.CategoryTheory.Sites.Coverage Mathlib.CategoryTheory.Sites.CoversTop Mathlib.CategoryTheory.Sites.IsSheafOneHypercover Mathlib.CategoryTheory.Sites.Limits Mathlib.CategoryTheory.Sites.Localization Mathlib.CategoryTheory.Sites.OneHypercover Mathlib.CategoryTheory.Sites.Over Mathlib.CategoryTheory.Sites.Plus Mathlib.CategoryTheory.Sites.PreservesSheafification Mathlib.CategoryTheory.Sites.SheafHom Mathlib.CategoryTheory.Sites.Sheaf Mathlib.CategoryTheory.Sites.Sheafification Mathlib.CategoryTheory.Sites.Subcanonical Mathlib.CategoryTheory.Sites.Types Mathlib.CategoryTheory.Sites.Whiskering Mathlib.CategoryTheory.Subobject.FactorThru Mathlib.CategoryTheory.Subobject.Lattice Mathlib.CategoryTheory.Subobject.Limits Mathlib.CategoryTheory.Triangulated.Rotate Mathlib.Combinatorics.Enumerative.IncidenceAlgebra Mathlib.Data.DFinsupp.Module Mathlib.Data.DFinsupp.Multiset Mathlib.Data.DFinsupp.Sigma Mathlib.GroupTheory.Congruence.Basic Mathlib.GroupTheory.GroupAction.Ring Mathlib.GroupTheory.Submonoid.Center Mathlib.GroupTheory.Submonoid.Centralizer Mathlib.MeasureTheory.Constructions.Cylinders Mathlib.MeasureTheory.MeasurableSpace.Basic Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated Mathlib.MeasureTheory.MeasurableSpace.Embedding Mathlib.MeasureTheory.MeasurableSpace.NCard Mathlib.MeasureTheory.MeasurableSpace.Pi Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict Mathlib.MeasureTheory.MeasurableSpace.Prod Mathlib.NumberTheory.ArithmeticFunction Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue Mathlib.Order.Filter.FilterProduct Mathlib.RingTheory.HahnSeries.Addition Mathlib.RingTheory.Ideal.Lattice Mathlib.RingTheory.Ideal.Prime Mathlib.RingTheory.Spectrum.Prime.Defs Mathlib.Topology.Algebra.Constructions.DomMulAct	3
16 files Mathlib.Algebra.Group.Subgroup.Basic Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas Mathlib.Algebra.Group.Subgroup.Order Mathlib.Algebra.Module.Pi Mathlib.Algebra.Ring.CentroidHom Mathlib.Data.Matrix.Defs Mathlib.Data.Matrix.Diagonal Mathlib.GroupTheory.Goursat Mathlib.GroupTheory.PresentedGroup Mathlib.GroupTheory.Subgroup.Simple Mathlib.Order.Filter.Germ.Basic Mathlib.Order.Filter.Germ.OrderedMonoid Mathlib.Order.Filter.Ring Mathlib.RingTheory.Ideal.BigOperators Mathlib.RingTheory.Ideal.Quotient.Defs Mathlib.RingTheory.TwoSidedIdeal.Operations	4
35 files Mathlib.Algebra.BigOperators.GroupWithZero.Action Mathlib.Algebra.CharZero.Quotient Mathlib.Algebra.DirectSum.Basic Mathlib.Algebra.DirectSum.Ring Mathlib.Algebra.Group.Conj Mathlib.Algebra.GroupWithZero.Conj Mathlib.Algebra.Module.BigOperators Mathlib.Algebra.Module.Submodule.EqLocus Mathlib.Algebra.Module.Submodule.Equiv Mathlib.Algebra.Module.Submodule.Invariant Mathlib.Algebra.Module.Submodule.IterateMapComap Mathlib.Algebra.Module.Submodule.Ker Mathlib.Algebra.Module.Submodule.LinearMap Mathlib.Algebra.Module.Submodule.Map Mathlib.Algebra.Module.Submodule.Range Mathlib.Combinatorics.Enumerative.InclusionExclusion Mathlib.Combinatorics.Pigeonhole Mathlib.Combinatorics.SimpleGraph.IncMatrix Mathlib.Data.DFinsupp.BigOperators Mathlib.Data.DFinsupp.Submonoid Mathlib.Data.Matrix.Mul Mathlib.Data.Matrix.PEquiv Mathlib.Data.NNRat.Lemmas Mathlib.GroupTheory.Coset.Defs Mathlib.LinearAlgebra.BilinearMap Mathlib.LinearAlgebra.Matrix.Orthogonal Mathlib.MeasureTheory.Constructions.SubmoduleQuotient Mathlib.RingTheory.Ideal.Defs Mathlib.RingTheory.SimpleRing.Basic Mathlib.RingTheory.SimpleRing.Defs Mathlib.RingTheory.TwoSidedIdeal.Basic Mathlib.RingTheory.TwoSidedIdeal.BigOperators Mathlib.RingTheory.TwoSidedIdeal.Instances Mathlib.RingTheory.TwoSidedIdeal.Kernel Mathlib.RingTheory.TwoSidedIdeal.Lattice	5
7 files Mathlib.Algebra.Group.Aut Mathlib.Algebra.Module.LinearMap.Basic Mathlib.Algebra.Module.Submodule.Lattice Mathlib.Algebra.Module.Submodule.RestrictScalars Mathlib.GroupTheory.QuotientGroup.Defs Mathlib.LinearAlgebra.Quotient.Defs Mathlib.LinearAlgebra.Span.Defs	6
4 files Mathlib.Algebra.GradedMonoid Mathlib.Algebra.GradedMulAction Mathlib.Algebra.Module.Submodule.Basic Mathlib.GroupTheory.GroupAction.Defs	7
Mathlib.Algebra.Module.Hom Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero	8
5 files Mathlib.Algebra.Module.Submodule.Defs Mathlib.Algebra.Module.Submodule.Order Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise Mathlib.GroupTheory.GroupAction.SubMulAction Mathlib.GroupTheory.GroupAction.Transitive	10
Mathlib.Algebra.Order.Module.Defs Mathlib.GroupTheory.GroupAction.DomAct.Basic	11
Mathlib.Algebra.Module.End Mathlib.Algebra.NoZeroSMulDivisors.Basic	12
3 files Mathlib.Algebra.Group.Action.Pretransitive Mathlib.Algebra.Module.NatInt Mathlib.Algebra.Ring.Action.Invariant	13
Mathlib.Algebra.Ring.Action.Subobjects	22
Mathlib.RingTheory.OreLocalization.Basic	23
Mathlib.Algebra.Order.Module.Synonym	54
Mathlib.GroupTheory.GroupAction.Pointwise	97
Mathlib.RingTheory.Congruence.Basic Mathlib.RingTheory.Congruence.Opposite	100
Mathlib.GroupTheory.GroupAction.DomAct.ActionHom	109
Mathlib.Algebra.Group.Submonoid.DistribMulAction	121
Mathlib.Algebra.Regular.SMul	142
Mathlib.Algebra.Module.Prod	157
3 files Mathlib.Algebra.Module.RingHom Mathlib.Algebra.PUnitInstances.Module Mathlib.GroupTheory.GroupAction.Hom	159
Mathlib.Algebra.GroupWithZero.Action.Prod	163
4 files Mathlib.Algebra.Module.Defs Mathlib.Algebra.Module.MinimalAxioms Mathlib.Algebra.Module.Opposite Mathlib.Algebra.Ring.Action.Field	166
Mathlib.Algebra.Ring.Action.Basic	169
Mathlib.Algebra.GroupWithZero.Action.End	172
Mathlib.Algebra.Group.Action.End	190

---

Declarations diff

+ LeftCancelMonoid.faithfulSMul
+ instance (priority := 910) Mul.toOpSMul (α : Type*) [Mul α] : SMul αᵐᵒᵖ α := ⟨(· * ·)⟩
- AddAction.functionEnd
- AddAction.ofEndHom
- AddAction.toEndHom
- Function.End.apply_FaithfulSMul

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.

---

No changes to technical debt.

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

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• chore(Algebra/Group/Action): group similar lemmas #21028
  By Dependent Issues (🤖). Happy coding!