Skip to content

[Merged by Bors] - chore(GroupTheory/Commutator): don't import Ring#21296

Closed
YaelDillies wants to merge 6 commits intomasterfrom
commutator_no_ring
Closed

[Merged by Bors] - chore(GroupTheory/Commutator): don't import Ring#21296
YaelDillies wants to merge 6 commits intomasterfrom
commutator_no_ring

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Jan 31, 2025 •
edited
Loading

Change group calls to simp [mul_assoc] or similar:

  • when low in the import hierarchy
  • and add a comment at each such site to this effect.

Zulip

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 31, 2025 •
edited
Loading

PR summary 8075c0ec96

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.GroupTheory.Commutator.Basic 573 452 -121 (-21.12%)
Mathlib.CategoryTheory.Action.Concrete 829 752 -77 (-9.29%)
Mathlib.GroupTheory.Abelianization 813 771 -42 (-5.17%)
Mathlib.NumberTheory.LucasLehmer 911 910 -1 (-0.11%)
Mathlib.GroupTheory.Exponent 951 950 -1 (-0.11%)
Import changes for all files
Files Import difference
Mathlib.GroupTheory.Commutator.Basic -121
Mathlib.CategoryTheory.Action.Concrete Mathlib.GroupTheory.GroupAction.Quotient -77
Mathlib.GroupTheory.Commutator.Finite -46
3 files Mathlib.GroupTheory.Abelianization Mathlib.GroupTheory.GroupAction.CardCommute Mathlib.GroupTheory.Solvable
 -42
11 files Mathlib.Algebra.Category.Grp.Adjunctions Mathlib.CategoryTheory.Action Mathlib.GroupTheory.Commensurable Mathlib.GroupTheory.Complement Mathlib.GroupTheory.FreeAbelianGroup Mathlib.GroupTheory.FreeGroup.NielsenSchreier Mathlib.GroupTheory.GroupExtension.Defs Mathlib.GroupTheory.Index Mathlib.GroupTheory.PushoutI Mathlib.GroupTheory.SemidirectProduct Mathlib.RingTheory.FreeRing
 -40
Mathlib.GroupTheory.HNNExtension -34
Mathlib.CategoryTheory.Action.Monoidal -22
3 files Mathlib.CategoryTheory.Galois.Action Mathlib.CategoryTheory.Galois.Examples Mathlib.CategoryTheory.Galois.Full
 -18
19 files Mathlib.Algebra.Algebra.ZMod Mathlib.Algebra.Homology.BifunctorFlip Mathlib.Algebra.Homology.Bifunctor Mathlib.Algebra.Homology.ComplexShapeSigns Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.Algebra.Homology.TotalComplex Mathlib.Algebra.Ring.NegOnePow Mathlib.Combinatorics.SimpleGraph.DegreeSum Mathlib.Combinatorics.SimpleGraph.Matching Mathlib.Combinatorics.SimpleGraph.UniversalVerts Mathlib.Data.ZMod.Aut Mathlib.Data.ZMod.Basic Mathlib.Data.ZMod.IntUnitsPower Mathlib.GroupTheory.GroupAction.Blocks Mathlib.GroupTheory.GroupAction.Primitive Mathlib.GroupTheory.NoncommPiCoprod Mathlib.GroupTheory.OrderOfElement Mathlib.LinearAlgebra.FiniteSpan Mathlib.RingTheory.Fintype
 -8
14 files Mathlib.Algebra.Homology.BifunctorAssociator Mathlib.Algebra.Homology.Monoidal Mathlib.CategoryTheory.Localization.Triangulated Mathlib.CategoryTheory.Triangulated.Adjunction Mathlib.CategoryTheory.Triangulated.Functor Mathlib.CategoryTheory.Triangulated.HomologicalFunctor Mathlib.CategoryTheory.Triangulated.Opposite.Functor Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated Mathlib.CategoryTheory.Triangulated.Pretriangulated Mathlib.CategoryTheory.Triangulated.Subcategory Mathlib.CategoryTheory.Triangulated.TStructure.Basic Mathlib.CategoryTheory.Triangulated.TriangleShift Mathlib.CategoryTheory.Triangulated.Triangulated Mathlib.RingTheory.WittVector.WittPolynomial
 -7
Mathlib.Data.ZMod.ValMinAbs -5
21 files Mathlib.Algebra.Homology.BifunctorHomotopy Mathlib.Algebra.Homology.BifunctorShift Mathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift Mathlib.Algebra.Homology.HomotopyCategory.HomComplex Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor Mathlib.Algebra.Homology.HomotopyCategory.MappingCone Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence Mathlib.Algebra.Homology.HomotopyCategory.Shift Mathlib.Algebra.Homology.HomotopyCategory.ShortExact Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors Mathlib.Algebra.Homology.HomotopyCategory.Triangulated Mathlib.Algebra.Homology.TotalComplexShift
 -4
669 files Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.Algebra.Category.Grp.Injective Mathlib.Algebra.Category.Grp.LargeColimits Mathlib.Algebra.Category.Grp.Ulift Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Algebra.Central.TensorProduct Mathlib.Algebra.CharP.Quotient Mathlib.Algebra.CharP.Two Mathlib.Algebra.Colimit.Ring Mathlib.Algebra.FreeAlgebra.Cardinality Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.Algebra.Lie.CartanSubalgebra Mathlib.Algebra.Lie.Character Mathlib.Algebra.Lie.EngelSubalgebra Mathlib.Algebra.Lie.Engel Mathlib.Algebra.Lie.InvariantForm Mathlib.Algebra.Lie.Nilpotent Mathlib.Algebra.Lie.Semisimple.Basic Mathlib.Algebra.Lie.Semisimple.Defs Mathlib.Algebra.Lie.Solvable Mathlib.Algebra.Module.CharacterModule Mathlib.Algebra.Order.AbsoluteValue.Equivalence Mathlib.Algebra.Order.Chebyshev Mathlib.Algebra.Order.ToIntervalMod Mathlib.Algebra.Periodic Mathlib.Algebra.Polynomial.GroupRingAction Mathlib.Analysis.Analytic.Basic Mathlib.Analysis.Analytic.CPolynomial Mathlib.Analysis.Analytic.ChangeOrigin Mathlib.Analysis.Analytic.Composition Mathlib.Analysis.Analytic.Constructions Mathlib.Analysis.Analytic.Inverse Mathlib.Analysis.Analytic.IsolatedZeros Mathlib.Analysis.Analytic.IteratedFDeriv Mathlib.Analysis.Analytic.Linear Mathlib.Analysis.Analytic.OfScalars Mathlib.Analysis.Analytic.Order Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.Analysis.Analytic.Uniqueness Mathlib.Analysis.Analytic.Within Mathlib.Analysis.Asymptotics.AsymptoticEquivalent Mathlib.Analysis.Asymptotics.Lemmas Mathlib.Analysis.Asymptotics.SpecificAsymptotics Mathlib.Analysis.Asymptotics.SuperpolynomialDecay Mathlib.Analysis.Asymptotics.TVS Mathlib.Analysis.Asymptotics.Theta Mathlib.Analysis.BoxIntegral.Box.SubboxInduction Mathlib.Analysis.BoxIntegral.Partition.Additive Mathlib.Analysis.BoxIntegral.Partition.Filter Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction Mathlib.Analysis.CStarAlgebra.Basic Mathlib.Analysis.CStarAlgebra.Classes Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary Mathlib.Analysis.CStarAlgebra.ContinuousMap Mathlib.Analysis.CStarAlgebra.Exponential Mathlib.Analysis.CStarAlgebra.Module.Synonym Mathlib.Analysis.CStarAlgebra.Multiplier Mathlib.Analysis.CStarAlgebra.Unitization Mathlib.Analysis.CStarAlgebra.lpSpace Mathlib.Analysis.Calculus.AddTorsor.AffineMap Mathlib.Analysis.Calculus.Conformal.NormedSpace Mathlib.Analysis.Calculus.ContDiff.Basic Mathlib.Analysis.Calculus.ContDiff.Bounds Mathlib.Analysis.Calculus.ContDiff.CPolynomial Mathlib.Analysis.Calculus.ContDiff.Defs Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno Mathlib.Analysis.Calculus.DSlope Mathlib.Analysis.Calculus.Darboux Mathlib.Analysis.Calculus.Deriv.Add Mathlib.Analysis.Calculus.Deriv.AffineMap Mathlib.Analysis.Calculus.Deriv.Basic Mathlib.Analysis.Calculus.Deriv.Comp Mathlib.Analysis.Calculus.Deriv.Inv Mathlib.Analysis.Calculus.Deriv.Inverse Mathlib.Analysis.Calculus.Deriv.Linear Mathlib.Analysis.Calculus.Deriv.Mul Mathlib.Analysis.Calculus.Deriv.Pi Mathlib.Analysis.Calculus.Deriv.Polynomial Mathlib.Analysis.Calculus.Deriv.Pow Mathlib.Analysis.Calculus.Deriv.Prod Mathlib.Analysis.Calculus.Deriv.Shift Mathlib.Analysis.Calculus.Deriv.Slope Mathlib.Analysis.Calculus.Deriv.Star Mathlib.Analysis.Calculus.Deriv.Support Mathlib.Analysis.Calculus.Deriv.ZPow Mathlib.Analysis.Calculus.DiffContOnCl Mathlib.Analysis.Calculus.FDeriv.Add Mathlib.Analysis.Calculus.FDeriv.Analytic Mathlib.Analysis.Calculus.FDeriv.Basic Mathlib.Analysis.Calculus.FDeriv.Bilinear Mathlib.Analysis.Calculus.FDeriv.Comp Mathlib.Analysis.Calculus.FDeriv.Equiv Mathlib.Analysis.Calculus.FDeriv.Linear Mathlib.Analysis.Calculus.FDeriv.Mul Mathlib.Analysis.Calculus.FDeriv.Pi Mathlib.Analysis.Calculus.FDeriv.Prod Mathlib.Analysis.Calculus.FDeriv.RestrictScalars Mathlib.Analysis.Calculus.FDeriv.Star Mathlib.Analysis.Calculus.FormalMultilinearSeries Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv Mathlib.Analysis.Calculus.IteratedDeriv.Defs Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas Mathlib.Analysis.Calculus.LagrangeMultipliers Mathlib.Analysis.Calculus.LineDeriv.Basic Mathlib.Analysis.Calculus.LocalExtr.Basic Mathlib.Analysis.Calculus.LocalExtr.LineDeriv Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.Analysis.Calculus.LocalExtr.Rolle Mathlib.Analysis.Calculus.LogDeriv Mathlib.Analysis.Calculus.TangentCone Mathlib.Analysis.Complex.AbelLimit Mathlib.Analysis.Complex.Asymptotics Mathlib.Analysis.Complex.Basic Mathlib.Analysis.Complex.Circle Mathlib.Analysis.Complex.Convex Mathlib.Analysis.Complex.HalfPlane Mathlib.Analysis.Complex.IsIntegral Mathlib.Analysis.Complex.ReImTopology Mathlib.Analysis.Complex.RealDeriv Mathlib.Analysis.Complex.UnitDisc.Basic Mathlib.Analysis.ConstantSpeed Mathlib.Analysis.Convex.Body Mathlib.Analysis.Convex.EGauge Mathlib.Analysis.Convex.Exposed Mathlib.Analysis.Convex.Gauge Mathlib.Analysis.Convex.PartitionOfUnity Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.Analysis.Convex.SpecificFunctions.Pow Mathlib.Analysis.Convex.Topology Mathlib.Analysis.Convex.TotallyBounded Mathlib.Analysis.Hofer Mathlib.Analysis.InnerProductSpace.Defs Mathlib.Analysis.LocallyConvex.AbsConvex Mathlib.Analysis.LocallyConvex.BalancedCoreHull Mathlib.Analysis.LocallyConvex.Barrelled Mathlib.Analysis.LocallyConvex.Basic Mathlib.Analysis.LocallyConvex.Bounded Mathlib.Analysis.LocallyConvex.ContinuousOfBounded Mathlib.Analysis.LocallyConvex.StrongTopology Mathlib.Analysis.LocallyConvex.WeakDual Mathlib.Analysis.LocallyConvex.WithSeminorms Mathlib.Analysis.MeanInequalitiesPow Mathlib.Analysis.MeanInequalities Mathlib.Analysis.Meromorphic.Basic Mathlib.Analysis.Meromorphic.Order Mathlib.Analysis.Normed.Affine.AddTorsor Mathlib.Analysis.Normed.Affine.ContinuousAffineMap Mathlib.Analysis.Normed.Affine.Isometry Mathlib.Analysis.Normed.Affine.MazurUlam Mathlib.Analysis.Normed.Algebra.Exponential Mathlib.Analysis.Normed.Algebra.Norm Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt Mathlib.Analysis.Normed.Algebra.Ultra Mathlib.Analysis.Normed.Algebra.UnitizationL1 Mathlib.Analysis.Normed.Algebra.Unitization Mathlib.Analysis.Normed.Field.InfiniteSum Mathlib.Analysis.Normed.Field.Lemmas Mathlib.Analysis.Normed.Field.ProperSpace Mathlib.Analysis.Normed.Field.Ultra Mathlib.Analysis.Normed.Field.UnitBall Mathlib.Analysis.Normed.Group.AddCircle Mathlib.Analysis.Normed.Group.BallSphere Mathlib.Analysis.Normed.Group.Completeness Mathlib.Analysis.Normed.Group.Completion Mathlib.Analysis.Normed.Group.ControlledClosure Mathlib.Analysis.Normed.Group.HomCompletion Mathlib.Analysis.Normed.Group.Hom Mathlib.Analysis.Normed.Group.InfiniteSum Mathlib.Analysis.Normed.Group.Lemmas Mathlib.Analysis.Normed.Group.NullSubmodule Mathlib.Analysis.Normed.Group.Pointwise Mathlib.Analysis.Normed.Group.Quotient Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels Mathlib.Analysis.Normed.Group.SemiNormedGrp Mathlib.Analysis.Normed.Group.Tannery Mathlib.Analysis.Normed.Group.Ultra Mathlib.Analysis.Normed.Group.Uniform Mathlib.Analysis.Normed.Group.ZeroAtInfty Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.Analysis.Normed.Lp.lpSpace Mathlib.Analysis.Normed.Module.Basic Mathlib.Analysis.Normed.Module.Completion Mathlib.Analysis.Normed.Module.Ray Mathlib.Analysis.Normed.Module.Span Mathlib.Analysis.Normed.MulAction Mathlib.Analysis.Normed.Operator.BanachSteinhaus Mathlib.Analysis.Normed.Operator.Banach Mathlib.Analysis.Normed.Operator.BoundedLinearMaps Mathlib.Analysis.Normed.Operator.Compact Mathlib.Analysis.Normed.Operator.ContinuousLinearMap Mathlib.Analysis.Normed.Operator.LinearIsometry Mathlib.Analysis.Normed.Order.Basic Mathlib.Analysis.Normed.Order.Lattice Mathlib.Analysis.Normed.Order.UpperLower Mathlib.Analysis.Normed.Ring.IsPowMulFaithful Mathlib.Analysis.Normed.Ring.SeminormFromBounded Mathlib.Analysis.Normed.Ring.SeminormFromConst Mathlib.Analysis.Normed.Ring.Seminorm Mathlib.Analysis.Normed.Ring.Ultra Mathlib.Analysis.Normed.Ring.Units Mathlib.Analysis.Normed.Ring.WithAbs Mathlib.Analysis.NormedSpace.BallAction Mathlib.Analysis.NormedSpace.ConformalLinearMap Mathlib.Analysis.NormedSpace.Connected Mathlib.Analysis.NormedSpace.DualNumber Mathlib.Analysis.NormedSpace.ENormedSpace Mathlib.Analysis.NormedSpace.Extend Mathlib.Analysis.NormedSpace.Extr Mathlib.Analysis.NormedSpace.FunctionSeries Mathlib.Analysis.NormedSpace.HomeomorphBall Mathlib.Analysis.NormedSpace.Int Mathlib.Analysis.NormedSpace.Multilinear.Basic Mathlib.Analysis.NormedSpace.Multilinear.Curry Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics Mathlib.Analysis.NormedSpace.OperatorNorm.Basic Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness Mathlib.Analysis.NormedSpace.OperatorNorm.Mul Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace Mathlib.Analysis.NormedSpace.OperatorNorm.Prod Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm Mathlib.Analysis.NormedSpace.Pointwise Mathlib.Analysis.NormedSpace.RCLike Mathlib.Analysis.NormedSpace.Real Mathlib.Analysis.NormedSpace.RieszLemma Mathlib.Analysis.NormedSpace.SphereNormEquiv Mathlib.Analysis.PSeries Mathlib.Analysis.Polynomial.Basic Mathlib.Analysis.RCLike.Basic Mathlib.Analysis.Seminorm Mathlib.Analysis.SpecialFunctions.Bernstein Mathlib.Analysis.SpecialFunctions.CompareExp Mathlib.Analysis.SpecialFunctions.Complex.Arg Mathlib.Analysis.SpecialFunctions.Complex.Circle Mathlib.Analysis.SpecialFunctions.Complex.Log Mathlib.Analysis.SpecialFunctions.Exp Mathlib.Analysis.SpecialFunctions.Exponential Mathlib.Analysis.SpecialFunctions.Log.Base Mathlib.Analysis.SpecialFunctions.Log.Basic Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Log.PosLog Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric Mathlib.Analysis.SpecialFunctions.PolynomialExp Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics Mathlib.Analysis.SpecialFunctions.Pow.Complex Mathlib.Analysis.SpecialFunctions.Pow.Continuity Mathlib.Analysis.SpecialFunctions.Pow.NNReal Mathlib.Analysis.SpecialFunctions.Pow.Real Mathlib.Analysis.SpecialFunctions.Sqrt Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse Mathlib.Analysis.SpecialFunctions.Trigonometric.Series Mathlib.Analysis.SpecificLimits.Basic Mathlib.Analysis.SpecificLimits.FloorPow Mathlib.Analysis.SpecificLimits.Normed Mathlib.Analysis.SpecificLimits.RCLike Mathlib.Analysis.SumOverResidueClass Mathlib.CategoryTheory.Abelian.ProjectiveDimension Mathlib.CategoryTheory.Galois.EssSurj Mathlib.CategoryTheory.Galois.IsFundamentalgroup Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.Combinatorics.Derangements.Exponential Mathlib.Combinatorics.SimpleGraph.Regularity.Bound Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk Mathlib.Combinatorics.SimpleGraph.Regularity.Increment Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Computability.AkraBazzi.GrowsPolynomially Mathlib.Condensed.AB Mathlib.Condensed.Basic Mathlib.Condensed.CartesianClosed Mathlib.Condensed.Discrete.Basic Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Colimit Mathlib.Condensed.Discrete.LocallyConstant Mathlib.Condensed.Discrete.Module Mathlib.Condensed.Epi Mathlib.Condensed.Equivalence Mathlib.Condensed.Explicit Mathlib.Condensed.Functors Mathlib.Condensed.Light.AB Mathlib.Condensed.Light.Basic Mathlib.Condensed.Light.CartesianClosed Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.Functors Mathlib.Condensed.Light.Limits Mathlib.Condensed.Light.Module Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.Limits Mathlib.Condensed.Module Mathlib.Condensed.Solid Mathlib.Condensed.TopCatAdjunction Mathlib.Condensed.TopComparison Mathlib.Data.Complex.Cardinality Mathlib.Data.Complex.FiniteDimensional Mathlib.Data.Nat.Choose.Lucas Mathlib.Data.Nat.Periodic Mathlib.Data.Nat.Totient Mathlib.Data.Real.Cardinality Mathlib.Data.Real.Hyperreal Mathlib.Data.Real.IsNonarchimedean Mathlib.Data.ZMod.Coprime Mathlib.Data.ZMod.Factorial Mathlib.Data.ZMod.QuotientGroup Mathlib.Data.ZMod.QuotientRing Mathlib.Data.ZMod.Units Mathlib.Dynamics.BirkhoffSum.NormedSpace Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber Mathlib.Dynamics.Ergodic.Action.Basic Mathlib.Dynamics.Ergodic.Action.Regular Mathlib.Dynamics.Ergodic.Conservative Mathlib.Dynamics.Ergodic.Ergodic Mathlib.Dynamics.Ergodic.Function Mathlib.Dynamics.Ergodic.MeasurePreserving Mathlib.Dynamics.TopologicalEntropy.CoverEntropy Mathlib.Dynamics.TopologicalEntropy.NetEntropy Mathlib.Dynamics.TopologicalEntropy.Semiconj Mathlib.Geometry.Manifold.ConformalGroupoid Mathlib.GroupTheory.CommutingProbability Mathlib.GroupTheory.CosetCover Mathlib.GroupTheory.Coxeter.Length Mathlib.GroupTheory.Exponent Mathlib.GroupTheory.FreeAbelianGroupFinsupp Mathlib.GroupTheory.GroupAction.Period Mathlib.GroupTheory.IndexNormal Mathlib.GroupTheory.Perm.Closure Mathlib.GroupTheory.Perm.Cycle.Basic Mathlib.GroupTheory.Perm.Finite Mathlib.GroupTheory.SpecificGroups.Dihedral Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv Mathlib.LinearAlgebra.Alternating.DomCoprod Mathlib.LinearAlgebra.FreeModule.IdealQuotient Mathlib.LinearAlgebra.FreeModule.Int Mathlib.LinearAlgebra.LinearDisjoint Mathlib.LinearAlgebra.Projectivization.Cardinality Mathlib.LinearAlgebra.TensorProduct.Graded.External Mathlib.LinearAlgebra.TensorProduct.Graded.Internal Mathlib.MeasureTheory.Category.MeasCat Mathlib.MeasureTheory.Constructions.BorelSpace.Basic Mathlib.MeasureTheory.Constructions.BorelSpace.Complex Mathlib.MeasureTheory.Constructions.BorelSpace.Metric Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable Mathlib.MeasureTheory.Constructions.BorelSpace.Order Mathlib.MeasureTheory.Constructions.BorelSpace.Real Mathlib.MeasureTheory.Constructions.Pi Mathlib.MeasureTheory.Constructions.Polish.Basic Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal Mathlib.MeasureTheory.Constructions.Projective Mathlib.MeasureTheory.Covering.VitaliFamily Mathlib.MeasureTheory.Covering.Vitali Mathlib.MeasureTheory.Decomposition.Exhaustion Mathlib.MeasureTheory.Decomposition.Jordan Mathlib.MeasureTheory.Decomposition.SignedHahn Mathlib.MeasureTheory.Decomposition.UnsignedHahn Mathlib.MeasureTheory.Function.AEEqFun Mathlib.MeasureTheory.Function.AEEqOfLIntegral Mathlib.MeasureTheory.Function.AEMeasurableOrder Mathlib.MeasureTheory.Function.AEMeasurableSequence Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.MeasureTheory.Function.Egorov Mathlib.MeasureTheory.Function.EssSup Mathlib.MeasureTheory.Function.Floor Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral Mathlib.MeasureTheory.Function.LpOrder Mathlib.MeasureTheory.Function.LpSeminorm.Basic Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality Mathlib.MeasureTheory.Function.LpSeminorm.Trim Mathlib.MeasureTheory.Function.LpSpace Mathlib.MeasureTheory.Function.SimpleFuncDense Mathlib.MeasureTheory.Function.SimpleFunc Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan Mathlib.MeasureTheory.Function.SpecialFunctions.Basic Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal Mathlib.MeasureTheory.Group.AEStabilizer Mathlib.MeasureTheory.Group.Action Mathlib.MeasureTheory.Group.Arithmetic Mathlib.MeasureTheory.Group.Convolution Mathlib.MeasureTheory.Group.Defs Mathlib.MeasureTheory.Group.LIntegral Mathlib.MeasureTheory.Group.MeasurableEquiv Mathlib.MeasureTheory.Group.Measure Mathlib.MeasureTheory.Group.Pointwise Mathlib.MeasureTheory.Group.Prod Mathlib.MeasureTheory.Integral.Indicator Mathlib.MeasureTheory.Integral.LebesgueNormedSpace Mathlib.MeasureTheory.Integral.Lebesgue Mathlib.MeasureTheory.Integral.Marginal Mathlib.MeasureTheory.Integral.MeanInequalities Mathlib.MeasureTheory.Integral.RieszMarkovKakutani Mathlib.MeasureTheory.Measure.AEDisjoint Mathlib.MeasureTheory.Measure.AEMeasurable Mathlib.MeasureTheory.Measure.AbsolutelyContinuous Mathlib.MeasureTheory.Measure.AddContent Mathlib.MeasureTheory.Measure.Comap Mathlib.MeasureTheory.Measure.Complex Mathlib.MeasureTheory.Measure.Content Mathlib.MeasureTheory.Measure.ContinuousPreimage Mathlib.MeasureTheory.Measure.Count Mathlib.MeasureTheory.Measure.Dirac Mathlib.MeasureTheory.Measure.Doubling Mathlib.MeasureTheory.Measure.GiryMonad Mathlib.MeasureTheory.Measure.Haar.Basic Mathlib.MeasureTheory.Measure.HasOuterApproxClosed Mathlib.MeasureTheory.Measure.Map Mathlib.MeasureTheory.Measure.MeasureSpaceDef Mathlib.MeasureTheory.Measure.MeasureSpace Mathlib.MeasureTheory.Measure.MutuallySingular Mathlib.MeasureTheory.Measure.NullMeasurable Mathlib.MeasureTheory.Measure.OpenPos Mathlib.MeasureTheory.Measure.Prod Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving Mathlib.MeasureTheory.Measure.Regular Mathlib.MeasureTheory.Measure.RegularityCompacts Mathlib.MeasureTheory.Measure.Restrict Mathlib.MeasureTheory.Measure.Stieltjes Mathlib.MeasureTheory.Measure.Sub Mathlib.MeasureTheory.Measure.Trim Mathlib.MeasureTheory.Measure.Typeclasses Mathlib.MeasureTheory.Measure.WithDensity Mathlib.MeasureTheory.Order.Group.Lattice Mathlib.MeasureTheory.Order.Lattice Mathlib.MeasureTheory.OuterMeasure.Caratheodory Mathlib.MeasureTheory.OuterMeasure.Induced Mathlib.MeasureTheory.OuterMeasure.OfFunction Mathlib.MeasureTheory.VectorMeasure.Basic Mathlib.ModelTheory.Algebra.Field.CharP Mathlib.ModelTheory.Algebra.Ring.FreeCommRing Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.NumberTheory.DirichletCharacter.Basic Mathlib.NumberTheory.EulerProduct.Basic Mathlib.NumberTheory.FLT.Four Mathlib.NumberTheory.Harmonic.Int Mathlib.NumberTheory.LegendreSymbol.ZModChar Mathlib.NumberTheory.LucasLehmer Mathlib.NumberTheory.MulChar.Basic Mathlib.NumberTheory.Ostrowski Mathlib.NumberTheory.Padics.Hensel Mathlib.NumberTheory.Padics.MahlerBasis Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.NumberTheory.Padics.PadicNumbers Mathlib.NumberTheory.Padics.ProperSpace Mathlib.NumberTheory.Padics.RingHoms Mathlib.NumberTheory.Pell Mathlib.NumberTheory.PrimeCounting Mathlib.NumberTheory.PythagoreanTriples Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.NumberTheory.VonMangoldt Mathlib.Order.Filter.ZeroAndBoundedAtFilter Mathlib.Probability.ConditionalProbability Mathlib.Probability.Distributions.Geometric Mathlib.Probability.Distributions.Poisson Mathlib.Probability.Independence.Basic Mathlib.Probability.Independence.Kernel Mathlib.Probability.Kernel.Basic Mathlib.Probability.Kernel.Composition.Basic Mathlib.Probability.Kernel.Composition.CompNotation Mathlib.Probability.Kernel.Composition.ParallelComp Mathlib.Probability.Kernel.Defs Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes Mathlib.Probability.Kernel.Invariance Mathlib.Probability.Kernel.MeasurableLIntegral Mathlib.Probability.Kernel.Proper Mathlib.Probability.ProbabilityMassFunction.Basic Mathlib.Probability.ProbabilityMassFunction.Binomial Mathlib.Probability.ProbabilityMassFunction.Constructions Mathlib.Probability.ProbabilityMassFunction.Monad Mathlib.Probability.UniformOn Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.RepresentationTheory.Rep Mathlib.RingTheory.Binomial Mathlib.RingTheory.Flat.Basic Mathlib.RingTheory.Flat.CategoryTheory Mathlib.RingTheory.Flat.Equalizer Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.RingTheory.Flat.FaithfullyFlat.Basic Mathlib.RingTheory.Flat.Localization Mathlib.RingTheory.Flat.Stability Mathlib.RingTheory.FreeCommRing Mathlib.RingTheory.Ideal.Quotient.Index Mathlib.RingTheory.LinearDisjoint Mathlib.RingTheory.MvPolynomial.FreeCommRing Mathlib.RingTheory.MvPowerSeries.PiTopology Mathlib.RingTheory.Polynomial.Chebyshev Mathlib.RingTheory.Polynomial.Dickson Mathlib.RingTheory.PowerSeries.Binomial Mathlib.RingTheory.PowerSeries.PiTopology Mathlib.RingTheory.RingHom.Flat Mathlib.RingTheory.TensorProduct.Nontrivial Mathlib.RingTheory.ZMod Mathlib.SetTheory.Cardinal.Free Mathlib.SetTheory.Nimber.Field Mathlib.Tactic.ReduceModChar Mathlib.Topology.Algebra.Algebra.Equiv Mathlib.Topology.Algebra.Algebra Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits Mathlib.Topology.Algebra.ClopenNhdofOne Mathlib.Topology.Algebra.ClosedSubgroup Mathlib.Topology.Algebra.ContinuousAffineMap Mathlib.Topology.Algebra.FilterBasis Mathlib.Topology.Algebra.Group.CompactOpen Mathlib.Topology.Algebra.Group.Quotient Mathlib.Topology.Algebra.InfiniteSum.Module Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean Mathlib.Topology.Algebra.LinearTopology Mathlib.Topology.Algebra.Module.Alternating.Basic Mathlib.Topology.Algebra.Module.Alternating.Topology Mathlib.Topology.Algebra.Module.Basic Mathlib.Topology.Algebra.Module.Cardinality Mathlib.Topology.Algebra.Module.CharacterSpace Mathlib.Topology.Algebra.Module.Equiv Mathlib.Topology.Algebra.Module.LinearMapPiProd Mathlib.Topology.Algebra.Module.LinearMap Mathlib.Topology.Algebra.Module.LinearPMap Mathlib.Topology.Algebra.Module.LocallyConvex Mathlib.Topology.Algebra.Module.ModuleTopology Mathlib.Topology.Algebra.Module.Multilinear.Basic Mathlib.Topology.Algebra.Module.Multilinear.Bounded Mathlib.Topology.Algebra.Module.Multilinear.Topology Mathlib.Topology.Algebra.Module.Simple Mathlib.Topology.Algebra.Module.Star Mathlib.Topology.Algebra.Module.StrongTopology Mathlib.Topology.Algebra.Module.UniformConvergence Mathlib.Topology.Algebra.Module.WeakDual Mathlib.Topology.Algebra.NonUnitalAlgebra Mathlib.Topology.Algebra.NonUnitalStarAlgebra Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology Mathlib.Topology.Algebra.Nonarchimedean.Bases Mathlib.Topology.Algebra.Nonarchimedean.Basic Mathlib.Topology.Algebra.Nonarchimedean.Completion Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected Mathlib.Topology.Algebra.OpenSubgroup Mathlib.Topology.Algebra.Polynomial Mathlib.Topology.Algebra.PontryaginDual Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous Mathlib.Topology.Algebra.Ring.Ideal Mathlib.Topology.Algebra.SeparationQuotient.Basic Mathlib.Topology.Algebra.SeparationQuotient.Section Mathlib.Topology.Algebra.StarSubalgebra Mathlib.Topology.Algebra.TopologicallyNilpotent Mathlib.Topology.Algebra.UniformField Mathlib.Topology.Algebra.UniformFilterBasis Mathlib.Topology.Algebra.UniformGroup.Basic Mathlib.Topology.Algebra.UniformRing Mathlib.Topology.Algebra.Valued.LocallyCompact Mathlib.Topology.Algebra.Valued.NormedValued Mathlib.Topology.Algebra.Valued.ValuationTopology Mathlib.Topology.Algebra.Valued.ValuedField Mathlib.Topology.Baire.BaireMeasurable Mathlib.Topology.Baire.CompleteMetrizable Mathlib.Topology.Bornology.BoundedOperation Mathlib.Topology.Category.CompHaus.Basic Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.Topology.Category.CompHaus.Frm Mathlib.Topology.Category.CompHaus.Limits Mathlib.Topology.Category.CompHaus.Projective Mathlib.Topology.Category.CompactlyGenerated Mathlib.Topology.Category.Compactum Mathlib.Topology.Category.DeltaGenerated Mathlib.Topology.Category.LightProfinite.AsLimit Mathlib.Topology.Category.LightProfinite.Basic Mathlib.Topology.Category.LightProfinite.EffectiveEpi Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Topology.Category.LightProfinite.Limits Mathlib.Topology.Category.LightProfinite.Sequence Mathlib.Topology.Category.Locale Mathlib.Topology.Category.Profinite.AsLimit Mathlib.Topology.Category.Profinite.Basic Mathlib.Topology.Category.Profinite.CofilteredLimit Mathlib.Topology.Category.Profinite.EffectiveEpi Mathlib.Topology.Category.Profinite.Extend Mathlib.Topology.Category.Profinite.Limits Mathlib.Topology.Category.Profinite.Nobeling Mathlib.Topology.Category.Profinite.Product Mathlib.Topology.Category.Profinite.Projective Mathlib.Topology.Category.Stonean.Adjunctions Mathlib.Topology.Category.Stonean.Basic Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Topology.Category.Stonean.Limits Mathlib.Topology.Compactness.CompactlyGeneratedSpace Mathlib.Topology.Compactness.DeltaGeneratedSpace Mathlib.Topology.ContinuousMap.Algebra Mathlib.Topology.ContinuousMap.Bounded.Basic Mathlib.Topology.ContinuousMap.Bounded.Star Mathlib.Topology.ContinuousMap.BoundedCompactlySupported Mathlib.Topology.ContinuousMap.Compact Mathlib.Topology.ContinuousMap.CompactlySupported Mathlib.Topology.ContinuousMap.ContinuousMapZero Mathlib.Topology.ContinuousMap.Ideals Mathlib.Topology.ContinuousMap.Lattice Mathlib.Topology.ContinuousMap.LocallyConstant Mathlib.Topology.ContinuousMap.Periodic Mathlib.Topology.ContinuousMap.Polynomial Mathlib.Topology.ContinuousMap.StarOrdered Mathlib.Topology.ContinuousMap.Star Mathlib.Topology.ContinuousMap.StoneWeierstrass Mathlib.Topology.ContinuousMap.Units Mathlib.Topology.ContinuousMap.Weierstrass Mathlib.Topology.ContinuousMap.ZeroAtInfty Mathlib.Topology.Germ Mathlib.Topology.Instances.AddCircle Mathlib.Topology.Instances.Complex Mathlib.Topology.Instances.Irrational Mathlib.Topology.Instances.RatLemmas Mathlib.Topology.Instances.Real.Lemmas Mathlib.Topology.Instances.RealVectorSpace Mathlib.Topology.Instances.TrivSqZeroExt Mathlib.Topology.Instances.ZMultiples Mathlib.Topology.Maps.Proper.CompactlyGenerated Mathlib.Topology.MetricSpace.Algebra Mathlib.Topology.MetricSpace.CantorScheme Mathlib.Topology.MetricSpace.Closeds Mathlib.Topology.MetricSpace.Completion Mathlib.Topology.MetricSpace.Contracting Mathlib.Topology.MetricSpace.GromovHausdorffRealized Mathlib.Topology.MetricSpace.GromovHausdorff Mathlib.Topology.MetricSpace.HausdorffDistance Mathlib.Topology.MetricSpace.HolderNorm Mathlib.Topology.MetricSpace.Holder Mathlib.Topology.MetricSpace.Kuratowski Mathlib.Topology.MetricSpace.PartitionOfUnity Mathlib.Topology.MetricSpace.Perfect Mathlib.Topology.MetricSpace.PiNat Mathlib.Topology.MetricSpace.Polish Mathlib.Topology.MetricSpace.ThickenedIndicator Mathlib.Topology.MetricSpace.Thickening Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps Mathlib.Topology.Metrizable.Urysohn Mathlib.Topology.Order.Category.FrameAdjunction Mathlib.Topology.PartitionOfUnity Mathlib.Topology.Separation.CompletelyRegular Mathlib.Topology.Separation.NotNormal Mathlib.Topology.Sheaves.CommRingCat Mathlib.Topology.Sheaves.MayerVietoris Mathlib.Topology.TietzeExtension Mathlib.Topology.UniformSpace.Dini Mathlib.Topology.UniformSpace.Matrix Mathlib.Topology.UrysohnsBounded Mathlib.Topology.UrysohnsLemma Mathlib.Topology.VectorBundle.Basic Mathlib.Topology.VectorBundle.Constructions Mathlib.Topology.VectorBundle.Hom
 -1

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.

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

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Jan 31, 2025
This was referenced Jan 31, 2025
Closed
Closed
Ruben-VandeVelde
Ruben-VandeVelde approved these changes Feb 1, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The group removal makes me a bit sad, but not enough to block. Would you mind either filing an issue to create a lightweight replacement tactic and listing all the PRs where you're making such changes, or adding code comments where you've removed the group calls?

maintainer merge?

@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 1, 2025

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Feb 1, 2025
@YaelDillies YaelDillies mentioned this pull request Feb 1, 2025
Open
@YaelDillies
Copy link
Copy Markdown
Contributor Author

YaelDillies commented Feb 1, 2025

Issue is here: #21324

@adomani
Copy link
Copy Markdown
Contributor

adomani commented Feb 1, 2025

Issue is here: #21324

For reference, I added the comment below also to the issue:

It looks like the implementation of group involves defining (implicitly) a simp-set. Would it not be possible to define the tactic and a partial simp-set that does not require ring, and add the ring-based lemmas to the Ring file and make them part of the group simp-set?

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Feb 2, 2025

I'm happy with moving the "heavy" functionality of group into a differently named tactic, but I don't want to remove group even if it is just simp with a small simp-set.

@kim-em kim-em removed the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Feb 2, 2025
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 3, 2025
@YaelDillies
Copy link
Copy Markdown
Contributor Author

YaelDillies commented Feb 3, 2025

Per Zulip, this doesn't depend on #21360 anymore.

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Feb 3, 2025
grunweg
grunweg reviewed Feb 5, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@grunweg grunweg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! Just one nit; my impression is that the zulip discussion has converges on this strategy.
maintainer delegate

@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 5, 2025

🚀 Pull request has been placed on the maintainer queue by grunweg.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Feb 5, 2025
@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Feb 5, 2025

Oh, and can you update the PR description to match the discussion outcome, please? (I don't think #21324 is necessary any more?)

YaelDillies
YaelDillies commented Feb 5, 2025
View reviewed changes
@YaelDillies @grunweg
whoops
8075c0e 
Co-authored-by: grunweg <rothgami@math.hu-berlin.de>
jcommelin
jcommelin reviewed Feb 6, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Feb 6, 2025
@ghost ghost removed the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Feb 6, 2025
mathlib-bors bot pushed a commit that referenced this pull request Feb 6, 2025
@YaelDillies
chore(GroupTheory/Commutator): don't import Ring (#21296)
d75602f 
Change `group` calls to `simp [mul_assoc]` or similar:
* when low in the import hierarchy
* and add a comment at each such site to this effect.

[Zulip](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2321296.20don't.20import.20Ring.20in.20GroupTheory.2ECommutator.2EBasic)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 6, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(GroupTheory/Commutator): don't import Ring [Merged by Bors] - chore(GroupTheory/Commutator): don't import Ring Feb 6, 2025
@mathlib-bors mathlib-bors bot closed this Feb 6, 2025
@mathlib-bors mathlib-bors bot deleted the commutator_no_ring branch February 6, 2025 17:53
Julian added a commit that referenced this pull request Feb 7, 2025
@Julian
Merge remote-tracking branch 'origin/master' into bhargava-factorial
53aa24b 
* origin/master:
  chore: update Mathlib dependencies 2025-02-06 (#21523)
  fix(MathlibTest/TransImports): stop inspecting the `Lean` package (#21492)
  style(Mathlib/Computability/Halting): `RePred` to `REPred` (#21216)
  feat(Data/Set/Card): add `ncard_le_encard` (#21467)
  feat(Order): lemmas for `Order.succ` and `Order.pred` in `Fin` (#21437)
  feat(LinearAlgebra/LinearIndependent): linear independence + subsingletons (#21511)
  feat: for continuous linear maps in a normed ring, `flip mul = mul` (#21507)
  chore(GroupTheory/Commutator): don't import `Ring` (#21296)
  chore(Data/Complex/Abs): add `protected` to results that already exists in root namespace (#21454)
  chore(*): `erw`s that can now become `rw`s (#21510)
  chore: allow create-adaptation-pr.sh to continue when bump branch already exists (#21486)
  feat(CategoryTheory): equivalence between `Ind C` and left exact functors from `C` to `Type` (#21430)
  chore: add test to TCSynth.lean (#21499)
  feat: the category of ind-objects satisfies the AB5 axiom (#21350)
  refactor(RepresentationTheory): `ConcreteCategory` instances for `Rep` (#21465)
  chore: split Mathlib.Order.Filter.Basic (#21403)
  chore: update Mathlib dependencies 2025-02-06 (#21487)
  chore(Cache): Add support for $MATHLIB_CACHE_DIR (#21480)
  feat(CategoryTheory): a closed monoidal category is an ordinary enriched category over itself (#21436)
  feat(AlgebraicTopology): notation X ^[n] for cosimplicial objects (#21485)
  chore: upgrade dependencies manually (#21484)
  refactor(Analysis/Normed): `ConcreteCategory` refactor for `SemiNormedGrp` (#21477)
  refactor(LinearAlgebra): `ConcreteCategory` instance for `QuadraticModuleCat` (#21471)
  refactor(MeasureTheory): `ConcreteCategory` instance for `MeasCat` (#21468)
  refactor(Topology/Category): clean up remaining uses of `HasForget` (#21458)
  refactor(CategoryTheory): `ConcreteCategory` instances for pointed types (#21470)
  feat(CategoryTheory/Action): `ConcreteCategory` instances for `Action` (#21462)
  feat(CategoryTheory): `ConcreteCategory` instance for `DifferentialObject` (#21464)
  feat(Analysis/Normed/Group/SeparationQuotient): add normed lifts and `mk` (#18178)
  chore: rename `encard_le_card` to `encard_le_encard` (#21426)
  feat: add theorem about the norm of cross products (#20920)
  feat(Data/Matroid/Circuit): circuit elimination and finitary matroids (#21172)
  feat(LinearAlgebra/ExteriorPower): add iMulti_family definition for product of a family of vectors (#21397)
pfaffelh pushed a commit that referenced this pull request Feb 7, 2025
@YaelDillies
chore(GroupTheory/Commutator): don't import Ring (#21296)
99f4285 
Change `group` calls to `simp [mul_assoc]` or similar:
* when low in the import hierarchy
* and add a comment at each such site to this effect.

[Zulip](https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2321296.20don't.20import.20Ring.20in.20GroupTheory.2ECommutator.2EBasic)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@grunweg grunweg grunweg left review comments

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde approved these changes

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

7 participants

@YaelDillies @adomani @kim-em @grunweg @jcommelin @Ruben-VandeVelde @mathlib4-dependent-issues-bot