feat(GroupTheory/Subgroup): basic API for set normalizers by SnirBroshi · Pull Request #36760 · leanprover-community/mathlib4

SnirBroshi · 2026-03-17T07:23:20Z

Since @[to_additive] doesn't work on MulAut (because AddAut wants to use multiplicative syntax) I've had to translate 2 theorems manually.

~~FWIW I think that setNormalizer should replace normalizer, as this old TODO says:~~

mathlib4/Mathlib/Algebra/Group/Subgroup/Defs.lean

Line 674 in 34ad346

-- TODO should this replace `normalizer`?

~~This will join Subgroup.centralizer which is already defined on sets rather than subgroups (and subgroups can use it thanks to their SetLike).~~
~~If you agree I'll create a separate PR that does it. Though it shouldn't block this PR.~~

depends on: [Merged by Bors] - feat(Algebra/Group/Subgroup/Defs): merge setNormalizer into normalizer #36852

github-actions · 2026-03-17T07:24:37Z

PR summary 36653f0972

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.GroupTheory.Subgroup.Centralizer	433	435	+2 (+0.46%)
Mathlib.Algebra.Group.Subgroup.Pointwise	652	654	+2 (+0.31%)

Import changes for all files

Files	Import difference
554 files `Mathlib.Algebra.Algebra.Epi` `Mathlib.Algebra.Algebra.Operations` `Mathlib.Algebra.Algebra.Spectrum.Basic` `Mathlib.Algebra.Algebra.Spectrum.Pi` `Mathlib.Algebra.Algebra.Spectrum.Quasispectrum` `Mathlib.Algebra.Algebra.StrictPositivity` `Mathlib.Algebra.Algebra.Subalgebra.Directed` `Mathlib.Algebra.Algebra.Subalgebra.Lattice` `Mathlib.Algebra.Algebra.Subalgebra.MulOpposite` `Mathlib.Algebra.Algebra.Subalgebra.Operations` `Mathlib.Algebra.Algebra.Subalgebra.Pi` `Mathlib.Algebra.Algebra.Subalgebra.Pointwise` `Mathlib.Algebra.Algebra.Subalgebra.Prod` `Mathlib.Algebra.Algebra.Subalgebra.Tower` `Mathlib.Algebra.Algebra.Subalgebra.Unitization` `Mathlib.Algebra.ArithmeticGeometric` `Mathlib.Algebra.Category.AlgCat.Basic` `Mathlib.Algebra.Category.AlgCat.Limits` `Mathlib.Algebra.Category.AlgCat.Monoidal` `Mathlib.Algebra.Category.AlgCat.Symmetric` `Mathlib.Algebra.Category.BialgCat.Basic` `Mathlib.Algebra.Category.BialgCat.Monoidal` `Mathlib.Algebra.Category.CoalgCat.Basic` `Mathlib.Algebra.Category.CoalgCat.ComonEquivalence` `Mathlib.Algebra.Category.CoalgCat.Monoidal` `Mathlib.Algebra.Category.Grp.AB` `Mathlib.Algebra.Category.Grp.Abelian` `Mathlib.Algebra.Category.Grp.Images` `Mathlib.Algebra.Category.Grp.Injective` `Mathlib.Algebra.Category.Grp.IsFinite` `Mathlib.Algebra.Category.Grp.Subobject` `Mathlib.Algebra.Category.HopfAlgCat.Basic` `Mathlib.Algebra.Category.HopfAlgCat.Monoidal` `Mathlib.Algebra.Category.ModuleCat.AB` `Mathlib.Algebra.Category.ModuleCat.Abelian` `Mathlib.Algebra.Category.ModuleCat.Biproducts` `Mathlib.Algebra.Category.ModuleCat.ChangeOfRings` `Mathlib.Algebra.Category.ModuleCat.EpiMono` `Mathlib.Algebra.Category.ModuleCat.Images` `Mathlib.Algebra.Category.ModuleCat.Injective` `Mathlib.Algebra.Category.ModuleCat.Kernels` `Mathlib.Algebra.Category.ModuleCat.LeftResolution` `Mathlib.Algebra.Category.ModuleCat.Localization` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian` `Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits` `Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Free` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback` `Mathlib.Algebra.Category.ModuleCat.Presheaf.PushforwardZeroMonoidal` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify` `Mathlib.Algebra.Category.ModuleCat.Presheaf` `Mathlib.Algebra.Category.ModuleCat.Pseudofunctor` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian` `Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Free` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization` `Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous` `Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree` `Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent` `Mathlib.Algebra.Category.ModuleCat.Sheaf` `Mathlib.Algebra.Category.ModuleCat.Stalk` `Mathlib.Algebra.Category.ModuleCat.Subobject` `Mathlib.Algebra.Category.Ring.Adjunctions` `Mathlib.Algebra.Category.Ring.Epi` `Mathlib.Algebra.Central.Basic` `Mathlib.Algebra.Central.Defs` `Mathlib.Algebra.Central.End` `Mathlib.Algebra.Central.Matrix` `Mathlib.Algebra.CharP.Algebra` `Mathlib.Algebra.CharP.IntermediateField` `Mathlib.Algebra.CharP.LocalRing` `Mathlib.Algebra.CharP.MixedCharZero` `Mathlib.Algebra.CharP.Subring` `Mathlib.Algebra.Colimit.Finiteness` `Mathlib.Algebra.Colimit.TensorProduct` `Mathlib.Algebra.CubicDiscriminant` `Mathlib.Algebra.DirectSum.Idempotents` `Mathlib.Algebra.DirectSum.Internal` `Mathlib.Algebra.DualNumber` `Mathlib.Algebra.Exact` `Mathlib.Algebra.FiveLemma` `Mathlib.Algebra.FreeAlgebra` `Mathlib.Algebra.Group.UniqueProds.VectorSpace` `Mathlib.Algebra.Homology.ConcreteCategory` `Mathlib.Algebra.Homology.ShortComplex.Ab` `Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory` `Mathlib.Algebra.Homology.ShortComplex.ModuleCat` `Mathlib.Algebra.Module.Bimodule` `Mathlib.Algebra.Module.GradedModule` `Mathlib.Algebra.Module.Injective` `Mathlib.Algebra.Module.LocalizedModule.Exact` `Mathlib.Algebra.Module.LocalizedModule.Int` `Mathlib.Algebra.Module.LocalizedModule.Submodule` `Mathlib.Algebra.Module.Presentation.Basic` `Mathlib.Algebra.Module.Presentation.Cokernel` `Mathlib.Algebra.Module.Presentation.DirectSum` `Mathlib.Algebra.Module.Presentation.RestrictScalars` `Mathlib.Algebra.Module.Presentation.Tautological` `Mathlib.Algebra.Module.Presentation.Tensor` `Mathlib.Algebra.Module.SnakeLemma` `Mathlib.Algebra.Module.Submodule.Pointwise` `Mathlib.Algebra.MonoidAlgebra.Grading` `Mathlib.Algebra.MvPolynomial.Basic` `Mathlib.Algebra.MvPolynomial.Cardinal` `Mathlib.Algebra.MvPolynomial.Comap` `Mathlib.Algebra.MvPolynomial.CommRing` `Mathlib.Algebra.MvPolynomial.Counit` `Mathlib.Algebra.MvPolynomial.Degrees` `Mathlib.Algebra.MvPolynomial.Derivation` `Mathlib.Algebra.MvPolynomial.Division` `Mathlib.Algebra.MvPolynomial.Equiv` `Mathlib.Algebra.MvPolynomial.Eval` `Mathlib.Algebra.MvPolynomial.Funext` `Mathlib.Algebra.MvPolynomial.Invertible` `Mathlib.Algebra.MvPolynomial.Monad` `Mathlib.Algebra.MvPolynomial.NoZeroDivisors` `Mathlib.Algebra.MvPolynomial.PDeriv` `Mathlib.Algebra.MvPolynomial.Polynomial` `Mathlib.Algebra.MvPolynomial.Rename` `Mathlib.Algebra.MvPolynomial.SchwartzZippel` `Mathlib.Algebra.MvPolynomial.Supported` `Mathlib.Algebra.MvPolynomial.Variables` `Mathlib.Algebra.Order.Module.HahnEmbedding` `Mathlib.Algebra.Order.Ring.Archimedean` `Mathlib.Algebra.Polynomial.AlgebraMap` `Mathlib.Algebra.Polynomial.CoeffMem` `Mathlib.Algebra.Polynomial.Degree.CardPowDegree` `Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree` `Mathlib.Algebra.Polynomial.Derivation` `Mathlib.Algebra.Polynomial.FieldDivision` `Mathlib.Algebra.Polynomial.Homogenize` `Mathlib.Algebra.Polynomial.Laurent` `Mathlib.Algebra.Polynomial.Lifts` `Mathlib.Algebra.Polynomial.Module.AEval` `Mathlib.Algebra.Polynomial.Module.Basic` `Mathlib.Algebra.Polynomial.Module.TensorProduct` `Mathlib.Algebra.Polynomial.RingDivision` `Mathlib.Algebra.Polynomial.Roots` `Mathlib.Algebra.Polynomial.RuleOfSigns` `Mathlib.Algebra.Polynomial.Smeval` `Mathlib.Algebra.Polynomial.SpecificDegree` `Mathlib.Algebra.Polynomial.Splits` `Mathlib.Algebra.Polynomial.SumIteratedDerivative` `Mathlib.Algebra.Polynomial.Taylor` `Mathlib.Algebra.Ring.Subring.IntPolynomial` `Mathlib.Algebra.Ring.Subring.Pointwise` `Mathlib.Algebra.Star.CHSH` `Mathlib.Algebra.Star.Free` `Mathlib.Algebra.Star.Subalgebra` `Mathlib.Algebra.Star.UnitaryStarAlgAut` `Mathlib.Algebra.Star.Unitary` `Mathlib.Algebra.TrivSqZeroExt.Basic` `Mathlib.Algebra.TrivSqZeroExt.Ideal` `Mathlib.Algebra.Vertex.HVertexOperator` `Mathlib.Algebra.Vertex.VertexOperator` `Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ` `Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms` `Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange` `Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology` `Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic` `Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup` `Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps` `Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit` `Mathlib.AlgebraicTopology.FundamentalGroupoid.Product` `Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected` `Mathlib.AlgebraicTopology.SimplicialComplex.Basic` `Mathlib.AlgebraicTopology.SingularHomology.Basic` `Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance` `Mathlib.AlgebraicTopology.SingularSet` `Mathlib.AlgebraicTopology.TopologicalSimplex` `Mathlib.Analysis.Calculus.TangentCone.Basic` `Mathlib.Analysis.Calculus.TangentCone.Prod` `Mathlib.Analysis.Complex.Exponential` `Mathlib.Analysis.Complex.Norm` `Mathlib.Analysis.Complex.Order` `Mathlib.Analysis.Complex.Trigonometric` `Mathlib.Analysis.Convex.Caratheodory` `Mathlib.Analysis.Convex.Combination` `Mathlib.Analysis.Convex.Cone.Closure` `Mathlib.Analysis.Convex.Contractible` `Mathlib.Analysis.Convex.Independent` `Mathlib.Analysis.Convex.Jensen` `Mathlib.Analysis.Convex.PathConnected` `Mathlib.Analysis.Convex.Quasiconvex` `Mathlib.Analysis.Convex.SimplicialComplex.Basic` `Mathlib.Analysis.Convex.StdSimplex` `Mathlib.Analysis.Convex.StoneSeparation` `Mathlib.Analysis.Convex.Strict` `Mathlib.Analysis.Normed.Affine.Simplex` `Mathlib.Analysis.Normed.Group.Bounded` `Mathlib.Analysis.Normed.Group.Continuity` `Mathlib.Analysis.Normed.Group.Rat` `Mathlib.Analysis.Normed.Lp.WithLp` `Mathlib.Analysis.Normed.Ring.WithAbs` `Mathlib.Analysis.NormedSpace.Alternating.Basic` `Mathlib.Analysis.NormedSpace.Alternating.Curry` `Mathlib.Analysis.NormedSpace.Alternating.Uncurry.Fin` `Mathlib.Analysis.NormedSpace.Connected` `Mathlib.Analysis.NormedSpace.Extend` `Mathlib.Analysis.NormedSpace.Multilinear.Basic` `Mathlib.Analysis.NormedSpace.Multilinear.Curry` `Mathlib.Analysis.NormedSpace.Normalize` `Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm` `Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm` `Mathlib.Analysis.NormedSpace.RieszLemma` `Mathlib.Analysis.Real.Spectrum` `Mathlib.Analysis.SpecialFunctions.Log.ERealExp` `Mathlib.Analysis.Subadditive` `Mathlib.CategoryTheory.Abelian.Ext` `Mathlib.CategoryTheory.Abelian.FreydMitchell` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite` `Mathlib.CategoryTheory.Abelian.Injective.Basic` `Mathlib.CategoryTheory.Abelian.Projective.Basic` `Mathlib.CategoryTheory.Abelian.Pseudoelements` `Mathlib.CategoryTheory.Abelian.Yoneda` `Mathlib.CategoryTheory.Galois.Topology` `Mathlib.CategoryTheory.Monoidal.Internal.Module` `Mathlib.CategoryTheory.Preadditive.Yoneda.Injective` `Mathlib.CategoryTheory.Preadditive.Yoneda.Limits` `Mathlib.CategoryTheory.Preadditive.Yoneda.Projective` `Mathlib.Combinatorics.Additive.ApproximateSubgroup` `Mathlib.Combinatorics.Nullstellensatz` `Mathlib.Data.Matrix.DualNumber` `Mathlib.Data.Rat.NatSqrt.Real` `Mathlib.Data.Real.CompleteField` `Mathlib.Data.Real.Hom` `Mathlib.Data.Real.Irrational` `Mathlib.Data.Real.Sqrt` `Mathlib.Data.Real.StarOrdered` `Mathlib.FieldTheory.IntermediateField.Adjoin.Defs` `Mathlib.FieldTheory.IntermediateField.Basic` `Mathlib.Geometry.Convex.Cone.Dual` `Mathlib.Geometry.Convex.Cone.Pointed` `Mathlib.Geometry.Convex.Cone.Simplicial` `Mathlib.Geometry.Manifold.ChartedSpace` `Mathlib.Geometry.Manifold.HasGroupoid` `Mathlib.Geometry.Manifold.LocalInvariantProperties` `Mathlib.Geometry.Manifold.Sheaf.Basic` `Mathlib.GroupTheory.Coxeter.Basic` `Mathlib.GroupTheory.Divisible` `Mathlib.GroupTheory.QuotientGroup.Basic` `Mathlib.GroupTheory.QuotientGroup.Finite` `Mathlib.GroupTheory.Rank` `Mathlib.LinearAlgebra.AffineSpace.Basis` `Mathlib.LinearAlgebra.AffineSpace.Ceva` `Mathlib.LinearAlgebra.AffineSpace.Independent` `Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic` `Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid` `Mathlib.LinearAlgebra.Basis.Exact` `Mathlib.LinearAlgebra.Basis.VectorSpace` `Mathlib.LinearAlgebra.DirectSum.Finite` `Mathlib.LinearAlgebra.Finsupp.Span` `Mathlib.LinearAlgebra.FreeProduct.Basic` `Mathlib.LinearAlgebra.Goursat` `Mathlib.LinearAlgebra.Isomorphisms` `Mathlib.LinearAlgebra.LeftExact` `Mathlib.LinearAlgebra.Matrix.Ideal` `Mathlib.LinearAlgebra.Projection` `Mathlib.LinearAlgebra.Quotient.Basic` `Mathlib.LinearAlgebra.Quotient.Bilinear` `Mathlib.LinearAlgebra.Quotient.Pi` `Mathlib.LinearAlgebra.SModEq.Pointwise` `Mathlib.LinearAlgebra.SModEq.Pow` `Mathlib.LinearAlgebra.SymmetricAlgebra.Basic` `Mathlib.LinearAlgebra.TensorAlgebra.Basic` `Mathlib.LinearAlgebra.TensorAlgebra.Grading` `Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower` `Mathlib.LinearAlgebra.TensorProduct.Finiteness` `Mathlib.LinearAlgebra.TensorProduct.Opposite` `Mathlib.LinearAlgebra.TensorProduct.Quotient` `Mathlib.LinearAlgebra.TensorProduct.RightExactness` `Mathlib.LinearAlgebra.TensorProduct.Subalgebra` `Mathlib.LinearAlgebra.TensorProduct.Submodule` `Mathlib.LinearAlgebra.TensorProduct.Vanishing` `Mathlib.MeasureTheory.OuterMeasure.AE` `Mathlib.MeasureTheory.OuterMeasure.Basic` `Mathlib.MeasureTheory.OuterMeasure.BorelCantelli` `Mathlib.MeasureTheory.OuterMeasure.Operations` `Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs` `Mathlib.NumberTheory.Dioph` `Mathlib.NumberTheory.FLT.Basic` `Mathlib.NumberTheory.FLT.MasonStothers` `Mathlib.NumberTheory.PellMatiyasevic` `Mathlib.NumberTheory.TsumDivsorsAntidiagonal` `Mathlib.NumberTheory.Zsqrtd.Basic` `Mathlib.NumberTheory.Zsqrtd.GaussianInt` `Mathlib.NumberTheory.Zsqrtd.ToReal` `Mathlib.RingTheory.AdicCompletion.Basic` `Mathlib.RingTheory.AdicCompletion.LocalRing` `Mathlib.RingTheory.Adjoin.Basic` `Mathlib.RingTheory.Adjoin.Polynomial.Basic` `Mathlib.RingTheory.Adjoin.Polynomial` `Mathlib.RingTheory.Adjoin.Singleton` `Mathlib.RingTheory.Algebraic.Cardinality` `Mathlib.RingTheory.Algebraic.Defs` `Mathlib.RingTheory.Algebraic.LinearIndependent` `Mathlib.RingTheory.Algebraic.Pi` `Mathlib.RingTheory.AlgebraicIndependent.Defs` `Mathlib.RingTheory.Bezout` `Mathlib.RingTheory.Bialgebra.Basic` `Mathlib.RingTheory.Bialgebra.Equiv` `Mathlib.RingTheory.Bialgebra.Hom` `Mathlib.RingTheory.Bialgebra.MonoidAlgebra` `Mathlib.RingTheory.Bialgebra.TensorProduct` `Mathlib.RingTheory.Coalgebra.Basic` `Mathlib.RingTheory.Coalgebra.Convolution` `Mathlib.RingTheory.Coalgebra.Equiv` `Mathlib.RingTheory.Coalgebra.Hom` `Mathlib.RingTheory.Coalgebra.MonoidAlgebra` `Mathlib.RingTheory.Coalgebra.MulOpposite` `Mathlib.RingTheory.Coalgebra.TensorProduct` `Mathlib.RingTheory.Congruence.Hom` `Mathlib.RingTheory.Coprime.Ideal` `Mathlib.RingTheory.Derivation.Basic` `Mathlib.RingTheory.Derivation.DifferentialRing` `Mathlib.RingTheory.Derivation.ToSquareZero` `Mathlib.RingTheory.DividedPowers.Basic` `Mathlib.RingTheory.DividedPowers.DPMorphism` `Mathlib.RingTheory.DividedPowers.RatAlgebra` `Mathlib.RingTheory.DividedPowers.SubDPIdeal` `Mathlib.RingTheory.DualNumber` `Mathlib.RingTheory.EuclideanDomain` `Mathlib.RingTheory.Finiteness.Basic` `Mathlib.RingTheory.Finiteness.Bilinear` `Mathlib.RingTheory.Finiteness.Defs` `Mathlib.RingTheory.Finiteness.Lattice` `Mathlib.RingTheory.Finiteness.Nakayama` `Mathlib.RingTheory.Finiteness.Prod` `Mathlib.RingTheory.Finiteness.Subalgebra` `Mathlib.RingTheory.GradedAlgebra.AlgHom` `Mathlib.RingTheory.GradedAlgebra.Basic` `Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal` `Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps` `Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule` `Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring` `Mathlib.RingTheory.GradedAlgebra.Radical` `Mathlib.RingTheory.GradedAlgebra.RingHom` `Mathlib.RingTheory.GradedAlgebra.TensorProduct` `Mathlib.RingTheory.HahnSeries.Cardinal` `Mathlib.RingTheory.HahnSeries.HEval` `Mathlib.RingTheory.HahnSeries.Lex` `Mathlib.RingTheory.HahnSeries.Multiplication` `Mathlib.RingTheory.HahnSeries.PowerSeries` `Mathlib.RingTheory.HahnSeries.Summable` `Mathlib.RingTheory.HahnSeries.Valuation` `Mathlib.RingTheory.HopfAlgebra.Basic` `Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra` `Mathlib.RingTheory.HopfAlgebra.TensorProduct` `Mathlib.RingTheory.Ideal.Colon` `Mathlib.RingTheory.Ideal.IdempotentFG` `Mathlib.RingTheory.Ideal.IsPrimary` `Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient` `Mathlib.RingTheory.Ideal.IsPrincipal` `Mathlib.RingTheory.Ideal.Maps` `Mathlib.RingTheory.Ideal.MinimalPrime.Basic` `Mathlib.RingTheory.Ideal.MinimalPrime.Localization` `Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian` `Mathlib.RingTheory.Ideal.Oka` `Mathlib.RingTheory.Ideal.Operations` `Mathlib.RingTheory.Ideal.Over` `Mathlib.RingTheory.Ideal.Pointwise` `Mathlib.RingTheory.Ideal.Prod` `Mathlib.RingTheory.Ideal.Quotient.Basic` `Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder` `Mathlib.RingTheory.Ideal.Quotient.Operations` `Mathlib.RingTheory.Ideal.Quotient.PowTransition` `Mathlib.RingTheory.IdealFilter.Basic` `Mathlib.RingTheory.Idempotents` `Mathlib.RingTheory.Int.Basic` `Mathlib.RingTheory.IsPrimary` `Mathlib.RingTheory.IsTensorProduct` `Mathlib.RingTheory.Jacobson.Ideal` `Mathlib.RingTheory.Jacobson.Radical` `Mathlib.RingTheory.Jacobson.Semiprimary` `Mathlib.RingTheory.LocalProperties.Exactness` `Mathlib.RingTheory.LocalProperties.Submodule` `Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic` `Mathlib.RingTheory.LocalRing.NonLocalRing` `Mathlib.RingTheory.LocalRing.ResidueField.Defs` `Mathlib.RingTheory.Localization.Algebra` `Mathlib.RingTheory.Localization.AsSubring` `Mathlib.RingTheory.Localization.AtPrime.Basic` `Mathlib.RingTheory.Localization.Away.Basic` `Mathlib.RingTheory.Localization.BaseChange` `Mathlib.RingTheory.Localization.Finiteness` `Mathlib.RingTheory.Localization.Ideal` `Mathlib.RingTheory.Localization.LocalizationLocalization` `Mathlib.RingTheory.Localization.Rat` `Mathlib.RingTheory.Morita.Basic` `Mathlib.RingTheory.Morita.Matrix` `Mathlib.RingTheory.MvPolynomial.EulerIdentity` `Mathlib.RingTheory.MvPolynomial.Groebner` `Mathlib.RingTheory.MvPolynomial.Homogeneous` `Mathlib.RingTheory.MvPolynomial.Localization` `Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex` `Mathlib.RingTheory.MvPolynomial.MonomialOrder` `Mathlib.RingTheory.MvPolynomial.Symmetric.Defs` `Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem` `Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities` `Mathlib.RingTheory.MvPolynomial.Tower` `Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous` `Mathlib.RingTheory.MvPowerSeries.Basic` `Mathlib.RingTheory.MvPowerSeries.Inverse` `Mathlib.RingTheory.MvPowerSeries.LexOrder` `Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors` `Mathlib.RingTheory.MvPowerSeries.Order` `Mathlib.RingTheory.MvPowerSeries.Rename` `Mathlib.RingTheory.MvPowerSeries.Trunc` `Mathlib.RingTheory.Nakayama` `Mathlib.RingTheory.Nilpotent.Exp` `Mathlib.RingTheory.Noetherian.Defs` `Mathlib.RingTheory.Noetherian.Filter` `Mathlib.RingTheory.Noetherian.OfPrime` `Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain` `Mathlib.RingTheory.Polynomial.Bernstein` `Mathlib.RingTheory.Polynomial.ContentIdeal` `Mathlib.RingTheory.Polynomial.Content` `Mathlib.RingTheory.Polynomial.Eisenstein.Basic` `Mathlib.RingTheory.Polynomial.Eisenstein.Criterion` `Mathlib.RingTheory.Polynomial.Eisenstein.Distinguished` `Mathlib.RingTheory.Polynomial.GaussNorm` `Mathlib.RingTheory.Polynomial.HilbertPoly` `Mathlib.RingTheory.Polynomial.Ideal` `Mathlib.RingTheory.Polynomial.IntegralNormalization` `Mathlib.RingTheory.Polynomial.Morse` `Mathlib.RingTheory.Polynomial.Radical` `Mathlib.RingTheory.Polynomial.ScaleRoots` `Mathlib.RingTheory.Polynomial.ShiftedLegendre` `Mathlib.RingTheory.Polynomial.SmallDegreeVieta` `Mathlib.RingTheory.Polynomial.Tower` `Mathlib.RingTheory.Polynomial.Vieta` `Mathlib.RingTheory.Polynomial.Wronskian` `Mathlib.RingTheory.PolynomialAlgebra` `Mathlib.RingTheory.PowerSeries.Basic` `Mathlib.RingTheory.PowerSeries.Catalan` `Mathlib.RingTheory.PowerSeries.CoeffMulMem` `Mathlib.RingTheory.PowerSeries.GaussNorm` `Mathlib.RingTheory.PowerSeries.NoZeroDivisors` `Mathlib.RingTheory.PowerSeries.Order` `Mathlib.RingTheory.PowerSeries.Schroder` `Mathlib.RingTheory.PowerSeries.Trunc` `Mathlib.RingTheory.PowerSeries.WellKnown` `Mathlib.RingTheory.PrincipalIdealDomainOfPrime` `Mathlib.RingTheory.PrincipalIdealDomain` `Mathlib.RingTheory.QuotSMulTop` `Mathlib.RingTheory.Radical.NatInt` `Mathlib.RingTheory.Radical` `Mathlib.RingTheory.Regular.Category` `Mathlib.RingTheory.SimpleModule.Basic` `Mathlib.RingTheory.SimpleModule.Isotypic` `Mathlib.RingTheory.SimpleRing.Matrix` `Mathlib.RingTheory.SimpleRing.Principal` `Mathlib.RingTheory.SurjectiveOnStalks` `Mathlib.RingTheory.TensorProduct.Basic` `Mathlib.RingTheory.TensorProduct.Finite` `Mathlib.RingTheory.TensorProduct.IsBaseChangeFree` `Mathlib.RingTheory.TensorProduct.IsBaseChangePi` `Mathlib.RingTheory.TensorProduct.Maps` `Mathlib.RingTheory.TensorProduct.MonoidAlgebra` `Mathlib.RingTheory.TensorProduct.MvPolynomial` `Mathlib.RingTheory.TensorProduct.Pi` `Mathlib.RingTheory.TensorProduct.Quotient` `Mathlib.RingTheory.UniqueFactorizationDomain.Ideal` `Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky` `Mathlib.RingTheory.Valuation.Basic` `Mathlib.RingTheory.Valuation.ExtendToLocalization` `Mathlib.RingTheory.Valuation.Integers` `Mathlib.RingTheory.Valuation.PrimeMultiplicity` `Mathlib.RingTheory.Valuation.Quotient` `Mathlib.RingTheory.Valuation.ValuationRing` `Mathlib.RingTheory.Valuation.ValuativeRel.Basic` `Mathlib.RingTheory.Valuation.ValuativeRel.Trivial` `Mathlib.Tactic.NormNum.RealSqrt` `Mathlib.Topology.Algebra.Equicontinuity` `Mathlib.Topology.Algebra.Field` `Mathlib.Topology.Algebra.Group.Basic` `Mathlib.Topology.Algebra.Group.Compact` `Mathlib.Topology.Algebra.Group.GroupTopology` `Mathlib.Topology.Algebra.Group.OpenMapping` `Mathlib.Topology.Algebra.Group.Pointwise` `Mathlib.Topology.Algebra.Group.SubmonoidClosure` `Mathlib.Topology.Algebra.GroupCompletion` `Mathlib.Topology.Algebra.InfiniteSum.Constructions` `Mathlib.Topology.Algebra.InfiniteSum.ENNReal` `Mathlib.Topology.Algebra.InfiniteSum.Field` `Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion` `Mathlib.Topology.Algebra.InfiniteSum.Group` `Mathlib.Topology.Algebra.InfiniteSum.NatInt` `Mathlib.Topology.Algebra.InfiniteSum.Order` `Mathlib.Topology.Algebra.InfiniteSum.Real` `Mathlib.Topology.Algebra.InfiniteSum.Ring` `Mathlib.Topology.Algebra.InfiniteSum.UniformOn` `Mathlib.Topology.Algebra.IntermediateField` `Mathlib.Topology.Algebra.IsUniformGroup.Constructions` `Mathlib.Topology.Algebra.IsUniformGroup.Defs` `Mathlib.Topology.Algebra.IsUniformGroup.Order` `Mathlib.Topology.Algebra.Localization` `Mathlib.Topology.Algebra.MetricSpace.Lipschitz` `Mathlib.Topology.Algebra.Module.Compact` `Mathlib.Topology.Algebra.MvPolynomial` `Mathlib.Topology.Algebra.Order.Field` `Mathlib.Topology.Algebra.Order.LiminfLimsup` `Mathlib.Topology.Algebra.Order.UpperLower` `Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace` `Mathlib.Topology.Algebra.Ring.Basic` `Mathlib.Topology.Algebra.Ring.Real` `Mathlib.Topology.Algebra.Star.Unitary` `Mathlib.Topology.Algebra.UniformConvergence` `Mathlib.Topology.Algebra.UniformMulAction` `Mathlib.Topology.Category.TopCat.Monoidal` `Mathlib.Topology.Category.TopCommRingCat` `Mathlib.Topology.Compactness.HilbertCubeEmbedding` `Mathlib.Topology.Connected.LocPathConnected` `Mathlib.Topology.Connected.PathConnected` `Mathlib.Topology.EMetricSpace.BoundedVariation` `Mathlib.Topology.Homotopy.Affine` `Mathlib.Topology.Homotopy.Basic` `Mathlib.Topology.Homotopy.Contractible` `Mathlib.Topology.Homotopy.Equiv` `Mathlib.Topology.Homotopy.HSpaces` `Mathlib.Topology.Homotopy.HomotopyGroup` `Mathlib.Topology.Homotopy.Lifting` `Mathlib.Topology.Homotopy.LocallyContractible` `Mathlib.Topology.Homotopy.Path` `Mathlib.Topology.Homotopy.Product` `Mathlib.Topology.Instances.ENNReal.Lemmas` `Mathlib.Topology.Instances.EReal.Lemmas` `Mathlib.Topology.Instances.NNReal.Lemmas` `Mathlib.Topology.Instances.Rat` `Mathlib.Topology.Path` `Mathlib.Topology.Semicontinuity.Basic` `Mathlib.Topology.Semicontinuity.Lindelof` `Mathlib.Topology.Semicontinuous` `Mathlib.Topology.Sheaves.Abelian` `Mathlib.Topology.Sheaves.AddCommGrpCat` `Mathlib.Topology.Sheaves.Flasque` `Mathlib.Topology.Subpath` `Mathlib.Topology.UniformSpace.CompareReals` `Mathlib.Topology.UniformSpace.Matrix` `Mathlib.Topology.UniformSpace.Path` `Mathlib.Topology.UnitInterval`	1
18 files `Mathlib.Algebra.AffineMonoid.Basic` `Mathlib.Algebra.AffineMonoid.Irreducible` `Mathlib.Algebra.Field.Action.ConjAct` `Mathlib.Algebra.Group.Irreducible.Indecomposable` `Mathlib.Algebra.Group.Subgroup.Pointwise` `Mathlib.Algebra.Group.Submonoid.Support` `Mathlib.Algebra.GroupWithZero.Action.ConjAct` `Mathlib.Algebra.GroupWithZero.Range` `Mathlib.Algebra.GroupWithZero.Subgroup` `Mathlib.Algebra.Order.GroupWithZero.Range` `Mathlib.Algebra.Ring.Action.ConjAct` `Mathlib.Algebra.Ring.Subgroup` `Mathlib.Geometry.Group.Growth.LinearLowerBound` `Mathlib.GroupTheory.DoubleCoset` `Mathlib.GroupTheory.Finiteness` `Mathlib.GroupTheory.GroupAction.ConjAct` `Mathlib.GroupTheory.MonoidLocalization.Finite` `Mathlib.GroupTheory.Subgroup.Centralizer`	2

Declarations diff

+ _root_.AddSubgroup.mem_normalizer_iff_conj_image_eq
+ _root_.AddSubgroup.normalizer_le_normalizer_closure
+ _root_.CommGroup.normalizer_eq_top
+ centralizer_le_normalizer
+ maximal_normal_subgroupOf_normalizer
+ mem_centralizer_iff_commutator_eq_one'
+ mem_normalizer_iff_conj_image_eq
+ normal_subgroupOf_centralizer_normalizer
+ normal_subgroupOf_closure_normalizer
+ normalizer_empty
+ normalizer_le_normalizer_closure
+ normalizer_singleton

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

Mathlib/Algebra/Group/Subgroup/Basic.lean

Mathlib/GroupTheory/Subgroup/Centralizer.lean

tb65536 · 2026-03-18T11:54:17Z

I would probably recommend going ahead with the larger normalizer refactor that you mention.

tb65536 · 2026-03-21T10:04:55Z

I'm marking this as blocked by #36852

mathlib-dependent-issues · 2026-03-23T09:48:53Z

This PR/issue depends on:

~~[Merged by Bors] - feat(Algebra/Group/Subgroup/Defs): merge setNormalizer into normalizer #36852~~
By Dependent Issues (🤖). Happy coding!

Mathlib/GroupTheory/Subgroup/Centralizer.lean

feat(GroupTheory/Subgroup): basic API for set normalizers

880ea50

github-actions bot added the t-group-theory Group theory label Mar 17, 2026

mathlib-triage bot assigned tb65536 Mar 18, 2026

tb65536 reviewed Mar 18, 2026

View reviewed changes

Mathlib/Algebra/Group/Subgroup/Basic.lean Outdated Show resolved Hide resolved

tb65536 reviewed Mar 18, 2026

View reviewed changes

Mathlib/Algebra/Group/Subgroup/Basic.lean Outdated Show resolved Hide resolved

tb65536 reviewed Mar 18, 2026

View reviewed changes

Mathlib/GroupTheory/Subgroup/Centralizer.lean Outdated Show resolved Hide resolved

remove normalizer_{bot,top}

84a8848

SnirBroshi mentioned this pull request Mar 19, 2026

[Merged by Bors] - feat(Algebra/Group/Subgroup/Defs): merge setNormalizer into normalizer #36852

Closed

use commutator notation

b5eba09

SnirBroshi requested a review from tb65536 March 19, 2026 12:21

mathlib-dependent-issues bot added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Mar 21, 2026

SnirBroshi added 4 commits March 23, 2026 14:30

Merge branch 'master' into feature/group/normalizer-basics

1ff38e2

setNormalizer was replaced

396057a

rename theorems with setNormalizer

0858434

to_additive is magic

a0ba713

SnirBroshi added the WIP Work in progress label Mar 23, 2026

fix mem_normalizer_iff usages

62fb1d4

SnirBroshi removed the WIP Work in progress label Mar 23, 2026

SnirBroshi added 2 commits March 23, 2026 15:57

fix Nilpotent.lean

5f3d818

Merge branch 'master' into feature/group/normalizer-basics

8cd1064

tb65536 reviewed Mar 25, 2026

View reviewed changes

Mathlib/GroupTheory/Subgroup/Centralizer.lean Outdated Show resolved Hide resolved

commutators are now additivized :)

bbb00fa

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(GroupTheory/Subgroup): basic API for set normalizers#36760

feat(GroupTheory/Subgroup): basic API for set normalizers#36760
SnirBroshi wants to merge 11 commits intoleanprover-community:masterfrom
SnirBroshi:feature/group/normalizer-basics

SnirBroshi commented Mar 17, 2026 •

edited

Loading

Uh oh!

github-actions bot commented Mar 17, 2026 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

tb65536 commented Mar 18, 2026

Uh oh!

tb65536 commented Mar 21, 2026

Uh oh!

mathlib-dependent-issues bot commented Mar 23, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

SnirBroshi commented Mar 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Mar 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 36653f0972

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

tb65536 commented Mar 18, 2026

Uh oh!

tb65536 commented Mar 21, 2026

Uh oh!

mathlib-dependent-issues bot commented Mar 23, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

SnirBroshi commented Mar 17, 2026 •

edited

Loading

github-actions bot commented Mar 17, 2026 •

edited

Loading