refactor: split the `group` tactic into `group` and `group_exp` #21360

YaelDillies · 2025-02-03T07:13:27Z

This is motivated by the fact that group is used in files that shouldn't know about Field, which is used internally in ring, and is generally a large import (120 files!).

Closes #21324.

github-actions · 2025-02-03T07:14:23Z

PR summary 371f00e4ee

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.Group	503	135	-368 (-73.16%)

Import changes for all files

Files	Import difference
`Mathlib.Tactic.Group`	-368
`Mathlib.GroupTheory.Commutator.Basic`	-118
`Mathlib.CategoryTheory.Action.Concrete` `Mathlib.GroupTheory.GroupAction.Quotient`	-74
`Mathlib.GroupTheory.Commutator.Finite`	-45
3 files `Mathlib.GroupTheory.Abelianization` `Mathlib.GroupTheory.GroupAction.CardCommute` `Mathlib.GroupTheory.Solvable`	-41
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`	-39
`Mathlib.GroupTheory.HNNExtension`	-33
`Mathlib.CategoryTheory.Action.Monoidal`	-21
3 files `Mathlib.CategoryTheory.Galois.Action` `Mathlib.CategoryTheory.Galois.Examples` `Mathlib.CategoryTheory.Galois.Full`	-17
18 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.NoncommPiCoprod` `Mathlib.GroupTheory.OrderOfElement` `Mathlib.LinearAlgebra.FiniteSpan` `Mathlib.RingTheory.Fintype`	-7
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`	-6
`Mathlib.Data.ZMod.ValMinAbs`	-4
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`	-3
328 files `Mathlib.Algebra.Category.ModuleCat.Differentials.Basic` `Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf` `Mathlib.Algebra.Category.ModuleCat.ExteriorPower` `Mathlib.Algebra.CharP.LinearMaps` `Mathlib.Algebra.Lie.Classical` `Mathlib.Algebra.Lie.Matrix` `Mathlib.Algebra.Lie.SkewAdjoint` `Mathlib.Algebra.Lie.Weights.Killing` `Mathlib.Algebra.Lie.Weights.RootSystem` `Mathlib.Algebra.Module.DedekindDomain` `Mathlib.Algebra.Module.PID` `Mathlib.Algebra.Module.Presentation.Differentials` `Mathlib.Algebra.Module.Torsion` `Mathlib.Algebra.Module.ZMod` `Mathlib.Algebra.Polynomial.Module.FiniteDimensional` `Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ` `Mathlib.AlgebraicGeometry.Morphisms.Etale` `Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified` `Mathlib.AlgebraicGeometry.Morphisms.Smooth` `Mathlib.AlgebraicGeometry.Sites.Etale` `Mathlib.Analysis.CStarAlgebra.ApproximateUnit` `Mathlib.Analysis.CStarAlgebra.CStarMatrix` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order` `Mathlib.Analysis.CStarAlgebra.GelfandDuality` `Mathlib.Analysis.CStarAlgebra.Hom` `Mathlib.Analysis.CStarAlgebra.Module.Constructions` `Mathlib.Analysis.CStarAlgebra.Module.Defs` `Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart` `Mathlib.Analysis.CStarAlgebra.Spectrum` `Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap` `Mathlib.Analysis.Complex.Conformal` `Mathlib.Analysis.Complex.IntegerCompl` `Mathlib.Analysis.Complex.Isometry` `Mathlib.Analysis.Complex.Polynomial.Basic` `Mathlib.Analysis.Complex.Polynomial.UnitTrinomial` `Mathlib.Analysis.Complex.UpperHalfPlane.Basic` `Mathlib.Analysis.Complex.UpperHalfPlane.Exp` `Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty` `Mathlib.Analysis.Complex.UpperHalfPlane.Manifold` `Mathlib.Analysis.Complex.UpperHalfPlane.Metric` `Mathlib.Analysis.Complex.UpperHalfPlane.Topology` `Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality` `Mathlib.Analysis.Fourier.ZMod` `Mathlib.Analysis.InnerProductSpace.JointEigenspace` `Mathlib.Analysis.InnerProductSpace.Semisimple` `Mathlib.Analysis.InnerProductSpace.StarOrder` `Mathlib.Analysis.Normed.Algebra.Basic` `Mathlib.Analysis.Normed.Algebra.Spectrum` `Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent` `Mathlib.Combinatorics.Additive.CauchyDavenport` `Mathlib.Combinatorics.Additive.ErdosGinzburgZiv` `Mathlib.Combinatorics.SimpleGraph.LapMatrix` `Mathlib.FieldTheory.AbelRuffini` `Mathlib.FieldTheory.AbsoluteGaloisGroup` `Mathlib.FieldTheory.CardinalEmb` `Mathlib.FieldTheory.Cardinality` `Mathlib.FieldTheory.ChevalleyWarning` `Mathlib.FieldTheory.Differential.Basic` `Mathlib.FieldTheory.Differential.Liouville` `Mathlib.FieldTheory.Finite.Basic` `Mathlib.FieldTheory.Finite.GaloisField` `Mathlib.FieldTheory.Finite.Polynomial` `Mathlib.FieldTheory.Finite.Trace` `Mathlib.FieldTheory.Galois.Basic` `Mathlib.FieldTheory.Galois.GaloisClosure` `Mathlib.FieldTheory.Galois.Infinite` `Mathlib.FieldTheory.Galois.Profinite` `Mathlib.FieldTheory.IsPerfectClosure` `Mathlib.FieldTheory.IsSepClosed` `Mathlib.FieldTheory.Isaacs` `Mathlib.FieldTheory.JacobsonNoether` `Mathlib.FieldTheory.KrullTopology` `Mathlib.FieldTheory.KummerExtension` `Mathlib.FieldTheory.Minpoly.MinpolyDiv` `Mathlib.FieldTheory.PolynomialGaloisGroup` `Mathlib.FieldTheory.PrimitiveElement` `Mathlib.FieldTheory.PurelyInseparable.Basic` `Mathlib.FieldTheory.PurelyInseparable.PerfectClosure` `Mathlib.FieldTheory.PurelyInseparable.Tower` `Mathlib.FieldTheory.SeparableClosure` `Mathlib.GroupTheory.FiniteAbelian.Basic` `Mathlib.GroupTheory.FiniteAbelian.Duality` `Mathlib.GroupTheory.Frattini` `Mathlib.GroupTheory.Nilpotent` `Mathlib.GroupTheory.Order.Min` `Mathlib.GroupTheory.PGroup` `Mathlib.GroupTheory.Schreier` `Mathlib.GroupTheory.SchurZassenhaus` `Mathlib.GroupTheory.SpecificGroups.Cyclic` `Mathlib.GroupTheory.SpecificGroups.KleinFour` `Mathlib.GroupTheory.SpecificGroups.Quaternion` `Mathlib.GroupTheory.SpecificGroups.ZGroup` `Mathlib.GroupTheory.Sylow` `Mathlib.GroupTheory.Torsion` `Mathlib.GroupTheory.Transfer` `Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange` `Mathlib.LinearAlgebra.CliffordAlgebra.Basic` `Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory` `Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation` `Mathlib.LinearAlgebra.CliffordAlgebra.Contraction` `Mathlib.LinearAlgebra.CliffordAlgebra.Equivs` `Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv` `Mathlib.LinearAlgebra.CliffordAlgebra.Even` `Mathlib.LinearAlgebra.CliffordAlgebra.Fold` `Mathlib.LinearAlgebra.CliffordAlgebra.Grading` `Mathlib.LinearAlgebra.CliffordAlgebra.Inversion` `Mathlib.LinearAlgebra.CliffordAlgebra.Prod` `Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup` `Mathlib.LinearAlgebra.CliffordAlgebra.Star` `Mathlib.LinearAlgebra.Dimension.Torsion.Basic` `Mathlib.LinearAlgebra.Dimension.Torsion.Finite` `Mathlib.LinearAlgebra.Eigenspace.Semisimple` `Mathlib.LinearAlgebra.ExteriorAlgebra.Basic` `Mathlib.LinearAlgebra.ExteriorAlgebra.Grading` `Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating` `Mathlib.LinearAlgebra.ExteriorPower.Basic` `Mathlib.LinearAlgebra.ExteriorPower.Pairing` `Mathlib.LinearAlgebra.JordanChevalley` `Mathlib.LinearAlgebra.Matrix.BilinearForm` `Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField` `Mathlib.LinearAlgebra.Matrix.FixedDetMatrices` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card` `Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs` `Mathlib.LinearAlgebra.Matrix.LDL` `Mathlib.LinearAlgebra.Matrix.PosDef` `Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup` `Mathlib.LinearAlgebra.Matrix.SchurComplement` `Mathlib.LinearAlgebra.Matrix.SesquilinearForm` `Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup` `Mathlib.LinearAlgebra.Matrix.ToLinearEquiv` `Mathlib.LinearAlgebra.QuadraticForm.Basic` `Mathlib.LinearAlgebra.QuadraticForm.Basis` `Mathlib.LinearAlgebra.QuadraticForm.Complex` `Mathlib.LinearAlgebra.QuadraticForm.Dual` `Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv` `Mathlib.LinearAlgebra.QuadraticForm.Isometry` `Mathlib.LinearAlgebra.QuadraticForm.Prod` `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal` `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric` `Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat` `Mathlib.LinearAlgebra.QuadraticForm.Real` `Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries` `Mathlib.LinearAlgebra.QuadraticForm.TensorProduct` `Mathlib.LinearAlgebra.Reflection` `Mathlib.LinearAlgebra.RootSystem.BaseChange` `Mathlib.LinearAlgebra.RootSystem.Base` `Mathlib.LinearAlgebra.RootSystem.Basic` `Mathlib.LinearAlgebra.RootSystem.CartanMatrix` `Mathlib.LinearAlgebra.RootSystem.Defs` `Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear` `Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate` `Mathlib.LinearAlgebra.RootSystem.Hom` `Mathlib.LinearAlgebra.RootSystem.OfBilinear` `Mathlib.LinearAlgebra.RootSystem.RootPairingCat` `Mathlib.LinearAlgebra.RootSystem.RootPositive` `Mathlib.LinearAlgebra.RootSystem.WeylGroup` `Mathlib.LinearAlgebra.Semisimple` `Mathlib.NumberTheory.ClassNumber.Finite` `Mathlib.NumberTheory.ClassNumber.FunctionField` `Mathlib.NumberTheory.Cyclotomic.Basic` `Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter` `Mathlib.NumberTheory.Cyclotomic.Discriminant` `Mathlib.NumberTheory.Cyclotomic.Embeddings` `Mathlib.NumberTheory.Cyclotomic.Gal` `Mathlib.NumberTheory.Cyclotomic.PID` `Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots` `Mathlib.NumberTheory.Cyclotomic.Rat` `Mathlib.NumberTheory.Cyclotomic.Three` `Mathlib.NumberTheory.DirichletCharacter.Bounds` `Mathlib.NumberTheory.DirichletCharacter.GaussSum` `Mathlib.NumberTheory.DirichletCharacter.Orthogonality` `Mathlib.NumberTheory.EulerProduct.DirichletLSeries` `Mathlib.NumberTheory.FLT.Three` `Mathlib.NumberTheory.FermatPsp` `Mathlib.NumberTheory.Fermat` `Mathlib.NumberTheory.FunctionField` `Mathlib.NumberTheory.GaussSum` `Mathlib.NumberTheory.JacobiSum.Basic` `Mathlib.NumberTheory.LSeries.DirichletContinuation` `Mathlib.NumberTheory.LSeries.Dirichlet` `Mathlib.NumberTheory.LSeries.Nonvanishing` `Mathlib.NumberTheory.LSeries.PrimesInAP` `Mathlib.NumberTheory.LSeries.ZMod` `Mathlib.NumberTheory.LegendreSymbol.AddCharacter` `Mathlib.NumberTheory.LegendreSymbol.Basic` `Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas` `Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum` `Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity` `Mathlib.NumberTheory.LucasPrimality` `Mathlib.NumberTheory.ModularForms.Basic` `Mathlib.NumberTheory.ModularForms.CongruenceSubgroups` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence` `Mathlib.NumberTheory.ModularForms.Identities` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold` `Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable` `Mathlib.NumberTheory.ModularForms.LevelOne` `Mathlib.NumberTheory.ModularForms.QExpansion` `Mathlib.NumberTheory.ModularForms.SlashActions` `Mathlib.NumberTheory.ModularForms.SlashInvariantForms` `Mathlib.NumberTheory.Modular` `Mathlib.NumberTheory.MulChar.Duality` `Mathlib.NumberTheory.MulChar.Lemmas` `Mathlib.NumberTheory.NumberField.AdeleRing` `Mathlib.NumberTheory.NumberField.Basic` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone` `Mathlib.NumberTheory.NumberField.ClassNumber` `Mathlib.NumberTheory.NumberField.Completion` `Mathlib.NumberTheory.NumberField.Discriminant.Basic` `Mathlib.NumberTheory.NumberField.Discriminant.Defs` `Mathlib.NumberTheory.NumberField.Embeddings` `Mathlib.NumberTheory.NumberField.EquivReindex` `Mathlib.NumberTheory.NumberField.FinitePlaces` `Mathlib.NumberTheory.NumberField.FractionalIdeal` `Mathlib.NumberTheory.NumberField.House` `Mathlib.NumberTheory.NumberField.Norm` `Mathlib.NumberTheory.NumberField.ProductFormula` `Mathlib.NumberTheory.NumberField.Units.Basic` `Mathlib.NumberTheory.NumberField.Units.DirichletTheorem` `Mathlib.NumberTheory.NumberField.Units.Regulator` `Mathlib.NumberTheory.PrimesCongruentOne` `Mathlib.NumberTheory.SumFourSquares` `Mathlib.NumberTheory.SumTwoSquares` `Mathlib.NumberTheory.Wilson` `Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity` `Mathlib.RingTheory.AdicCompletion.Algebra` `Mathlib.RingTheory.AdicCompletion.AsTensorProduct` `Mathlib.RingTheory.AdicCompletion.Exactness` `Mathlib.RingTheory.AdicCompletion.Functoriality` `Mathlib.RingTheory.Complex` `Mathlib.RingTheory.DedekindDomain.Different` `Mathlib.RingTheory.DedekindDomain.Dvr` `Mathlib.RingTheory.DedekindDomain.IntegralClosure` `Mathlib.RingTheory.DedekindDomain.PID` `Mathlib.RingTheory.DiscreteValuationRing.TFAE` `Mathlib.RingTheory.Discriminant` `Mathlib.RingTheory.Etale.Basic` `Mathlib.RingTheory.Etale.Field` `Mathlib.RingTheory.Etale.Kaehler` `Mathlib.RingTheory.Etale.Pi` `Mathlib.RingTheory.Extension` `Mathlib.RingTheory.FractionalIdeal.Norm` `Mathlib.RingTheory.Generators` `Mathlib.RingTheory.Ideal.Cotangent` `Mathlib.RingTheory.Ideal.Norm.AbsNorm` `Mathlib.RingTheory.Ideal.Norm.RelNorm` `Mathlib.RingTheory.IntegralClosure.IntegralRestrict` `Mathlib.RingTheory.IntegralDomain` `Mathlib.RingTheory.Invariant` `Mathlib.RingTheory.Kaehler.Basic` `Mathlib.RingTheory.Kaehler.CotangentComplex` `Mathlib.RingTheory.Kaehler.JacobiZariski` `Mathlib.RingTheory.Kaehler.Polynomial` `Mathlib.RingTheory.Kaehler.TensorProduct` `Mathlib.RingTheory.LittleWedderburn` `Mathlib.RingTheory.LocalRing.Module` `Mathlib.RingTheory.Localization.NormTrace` `Mathlib.RingTheory.Norm.Basic` `Mathlib.RingTheory.NormTrace` `Mathlib.RingTheory.Polynomial.Cyclotomic.Basic` `Mathlib.RingTheory.Polynomial.Cyclotomic.Eval` `Mathlib.RingTheory.Polynomial.Cyclotomic.Expand` `Mathlib.RingTheory.Polynomial.Cyclotomic.Roots` `Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral` `Mathlib.RingTheory.Polynomial.Selmer` `Mathlib.RingTheory.Presentation` `Mathlib.RingTheory.Regular.IsSMulRegular` `Mathlib.RingTheory.Regular.RegularSequence` `Mathlib.RingTheory.RingHom.StandardSmooth` `Mathlib.RingTheory.RingHom.Unramified` `Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed` `Mathlib.RingTheory.RootsOfUnity.Basic` `Mathlib.RingTheory.RootsOfUnity.Complex` `Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity` `Mathlib.RingTheory.RootsOfUnity.Lemmas` `Mathlib.RingTheory.RootsOfUnity.Minpoly` `Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots` `Mathlib.RingTheory.Smooth.Basic` `Mathlib.RingTheory.Smooth.Kaehler` `Mathlib.RingTheory.Smooth.Local` `Mathlib.RingTheory.Smooth.Locus` `Mathlib.RingTheory.Smooth.Pi` `Mathlib.RingTheory.Smooth.StandardSmoothCotangent` `Mathlib.RingTheory.Smooth.StandardSmooth` `Mathlib.RingTheory.Spectrum.Prime.FreeLocus` `Mathlib.RingTheory.Trace.Basic` `Mathlib.RingTheory.Trace.Defs` `Mathlib.RingTheory.Trace.Quotient` `Mathlib.RingTheory.Unramified.Basic` `Mathlib.RingTheory.Unramified.Field` `Mathlib.RingTheory.Unramified.Finite` `Mathlib.RingTheory.Unramified.Locus` `Mathlib.RingTheory.Unramified.Pi` `Mathlib.RingTheory.WittVector.Basic` `Mathlib.RingTheory.WittVector.Compare` `Mathlib.RingTheory.WittVector.Complete` `Mathlib.RingTheory.WittVector.Defs` `Mathlib.RingTheory.WittVector.DiscreteValuationRing` `Mathlib.RingTheory.WittVector.Domain` `Mathlib.RingTheory.WittVector.FrobeniusFractionField` `Mathlib.RingTheory.WittVector.Frobenius` `Mathlib.RingTheory.WittVector.Identities` `Mathlib.RingTheory.WittVector.InitTail` `Mathlib.RingTheory.WittVector.IsPoly` `Mathlib.RingTheory.WittVector.Isocrystal` `Mathlib.RingTheory.WittVector.MulCoeff` `Mathlib.RingTheory.WittVector.MulP` `Mathlib.RingTheory.WittVector.StructurePolynomial` `Mathlib.RingTheory.WittVector.Teichmuller` `Mathlib.RingTheory.WittVector.Truncated` `Mathlib.RingTheory.WittVector.Verschiebung` `Mathlib.Tactic.NormNum.LegendreSymbol` `Mathlib.Tactic`	1
`Mathlib.Tactic.GroupExp` (new file)	504

Declarations diff

+ add_neg_cancel
+ neg_add_cancel

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.

Increase in tech debt: (relative, absolute) = (2.00, 0.02)

Current number	Change	Type
115	2	disabled simpNF lints

Current commit 371f00e4ee
Reference commit 13a19003b1

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

YaelDillies · 2025-02-06T18:25:56Z

Closing per Zulip

refactor: split the group tactic into group and group_exp

c129836

YaelDillies added the t-meta Tactics, attributes or user commands label Feb 3, 2025

fix tests

85805fb

YaelDillies mentioned this pull request Feb 3, 2025

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

Closed

YaelDillies added 3 commits February 3, 2025 07:32

fix

6e572a7

nolint

225e73e

noshake

371f00e

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 6, 2025

YaelDillies closed this Feb 6, 2025

YaelDillies deleted the group_exp branch February 6, 2025 18:26

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

refactor: split the `group` tactic into `group` and `group_exp` #21360

refactor: split the `group` tactic into `group` and `group_exp` #21360

YaelDillies commented Feb 3, 2025 •

edited

Loading

github-actions bot commented Feb 3, 2025 •

edited

Loading

Import changes for modified files

YaelDillies commented Feb 6, 2025

refactor: split the group tactic into group and group_exp #21360

refactor: split the group tactic into group and group_exp #21360

Conversation

YaelDillies commented Feb 3, 2025 • edited Loading

github-actions bot commented Feb 3, 2025 • edited Loading

PR summary 371f00e4ee

Import changes for modified files

Declarations diff

YaelDillies commented Feb 6, 2025

refactor: split the `group` tactic into `group` and `group_exp` #21360

refactor: split the `group` tactic into `group` and `group_exp` #21360

YaelDillies commented Feb 3, 2025 •

edited

Loading

github-actions bot commented Feb 3, 2025 •

edited

Loading