refactor: change definition of distance in normed group by sgouezel · Pull Request #35037 · leanprover-community/mathlib4

sgouezel · 2026-02-09T17:16:14Z

The current definition of the distance in a normed group is dist x y = ||x / y||. With this definition, the distance is right-invariant. This does not correspond to the convention in geometric group theory where the distance is given by ||x^{-1} * y|| to make sure it is left-invariant -- this corresponds to the fact that, in a Cayley graph, we put an edge between x and xs and declare these to be at distance one.

We refactor the definition to make sure it follows the standard convention. A pain point is that, in additive commutative groups, which is arguably the most important case, it becomes ||-x + y|| instead of ||x - y|| (which is propositionally the same, but not definitionally). To minimize the hassle, we keep all the lemmas that use ||x - y||, with their current names, and add new versions in terms of ||-x + y|| when useful.

github-actions · 2026-02-09T17:17:27Z

PR summary 4d984d0bb1

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Normed.Group.Defs	994	997	+3 (+0.30%)
Mathlib.Analysis.Normed.Group.Basic	1083	1086	+3 (+0.28%)
Mathlib.Analysis.Normed.Group.Real	1084	1087	+3 (+0.28%)
Mathlib.Analysis.Normed.Order.Hom.Basic	1084	1087	+3 (+0.28%)
Mathlib.InformationTheory.Hamming	1084	1087	+3 (+0.28%)
Mathlib.Analysis.Normed.Group.Constructions	1086	1089	+3 (+0.28%)
Mathlib.Analysis.Normed.Order.Hom.Ultra	1086	1089	+3 (+0.28%)
Mathlib.Analysis.Normed.Group.Int	1111	1114	+3 (+0.27%)
Mathlib.Analysis.Normed.Group.Continuity	1208	1211	+3 (+0.25%)
Mathlib.Analysis.Normed.Group.Bounded	1209	1212	+3 (+0.25%)
Mathlib.Analysis.Normed.Group.Rat	1213	1216	+3 (+0.25%)
Mathlib.Analysis.Normed.Ring.Basic	1213	1216	+3 (+0.25%)
Mathlib.Analysis.Normed.Field.Basic	1217	1220	+3 (+0.25%)
Mathlib.Analysis.Complex.Norm	1283	1286	+3 (+0.23%)
Mathlib.Analysis.Normed.MulAction	1327	1330	+3 (+0.23%)
Mathlib.Analysis.Normed.Group.Uniform	1342	1345	+3 (+0.22%)
Mathlib.Analysis.Normed.Group.Completion	1352	1355	+3 (+0.22%)
Mathlib.Analysis.Normed.Field.Lemmas	1378	1381	+3 (+0.22%)
Mathlib.Analysis.Normed.Group.Ultra	1383	1386	+3 (+0.22%)
Mathlib.Analysis.Normed.Module.Basic	1383	1386	+3 (+0.22%)
Mathlib.Analysis.LocallyConvex.BalancedCoreHull	1426	1429	+3 (+0.21%)
Mathlib.Analysis.Seminorm	1429	1432	+3 (+0.21%)
Mathlib.Topology.Algebra.Module.Multilinear.Bounded	1441	1444	+3 (+0.21%)
Mathlib.Analysis.Asymptotics.Lemmas	1443	1446	+3 (+0.21%)
Mathlib.Analysis.Normed.Group.Pointwise	1473	1476	+3 (+0.20%)
Mathlib.NumberTheory.Padics.PadicNumbers	1477	1480	+3 (+0.20%)
Mathlib.Analysis.LocallyConvex.WithSeminorms	1539	1542	+3 (+0.19%)
Mathlib.Analysis.Normed.Group.Quotient	1542	1545	+3 (+0.19%)
Mathlib.Analysis.Normed.Group.ControlledClosure	1552	1555	+3 (+0.19%)
Mathlib.NumberTheory.Padics.PadicIntegers	1594	1597	+3 (+0.19%)
Mathlib.Analysis.Normed.Operator.Basic	1628	1631	+3 (+0.18%)
Mathlib.Analysis.Complex.Basic	1631	1634	+3 (+0.18%)
Mathlib.Analysis.Normed.Operator.Completeness	1631	1634	+3 (+0.18%)
Mathlib.Topology.ContinuousMap.Bounded.Normed	1638	1641	+3 (+0.18%)
Mathlib.Analysis.Normed.Module.Multilinear.Basic	1640	1643	+3 (+0.18%)
Mathlib.Topology.ContinuousMap.Compact	1684	1687	+3 (+0.18%)
Mathlib.Analysis.SpecialFunctions.Exp	1704	1707	+3 (+0.18%)
Mathlib.Analysis.Normed.Lp.ProdLp	1795	1798	+3 (+0.17%)
Mathlib.Analysis.Normed.Lp.lpSpace	1796	1799	+3 (+0.17%)
Mathlib.Analysis.Normed.Algebra.UnitizationL1	1799	1802	+3 (+0.17%)
Mathlib.Analysis.CStarAlgebra.lpSpace	1801	1804	+3 (+0.17%)
Mathlib.Topology.MetricSpace.Kuratowski	1801	1804	+3 (+0.17%)
Mathlib.Analysis.Calculus.FDeriv.Extend	1840	1843	+3 (+0.16%)
Mathlib.Analysis.Calculus.UniformLimitsDeriv	1841	1844	+3 (+0.16%)
Mathlib.Topology.Algebra.Valued.NormedValued	1855	1858	+3 (+0.16%)
Mathlib.Analysis.InnerProductSpace.Subspace	1865	1868	+3 (+0.16%)
Mathlib.MeasureTheory.Function.LpSpace.Basic	1930	1933	+3 (+0.16%)
Mathlib.NumberTheory.Padics.MahlerBasis	1932	1935	+3 (+0.16%)
Mathlib.MeasureTheory.Function.ConvergenceInMeasure	1935	1938	+3 (+0.16%)

Import changes for all files

Files	Import difference
716 files `Mathlib.Analysis.Analytic.Basic` `Mathlib.Analysis.Analytic.CPolynomialDef` `Mathlib.Analysis.Analytic.CPolynomial` `Mathlib.Analysis.Analytic.ChangeOrigin` `Mathlib.Analysis.Analytic.Composition` `Mathlib.Analysis.Analytic.Constructions` `Mathlib.Analysis.Analytic.ConvergenceRadius` `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.Completion` `Mathlib.Analysis.Asymptotics.Defs` `Mathlib.Analysis.Asymptotics.ExpGrowth` `Mathlib.Analysis.Asymptotics.Lemmas` `Mathlib.Analysis.Asymptotics.SpecificAsymptotics` `Mathlib.Analysis.Asymptotics.SuperpolynomialDecay` `Mathlib.Analysis.Asymptotics.TVS` `Mathlib.Analysis.Asymptotics.Theta` `Mathlib.Analysis.BoxIntegral.Partition.Additive` `Mathlib.Analysis.CStarAlgebra.Basic` `Mathlib.Analysis.CStarAlgebra.Classes` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary` `Mathlib.Analysis.CStarAlgebra.ContinuousMap` `Mathlib.Analysis.CStarAlgebra.Exponential` `Mathlib.Analysis.CStarAlgebra.Multiplier` `Mathlib.Analysis.CStarAlgebra.Unitization` `Mathlib.Analysis.CStarAlgebra.lpSpace` `Mathlib.Analysis.Calculus.AddTorsor.AffineMap` `Mathlib.Analysis.Calculus.Conformal.InnerProduct` `Mathlib.Analysis.Calculus.Conformal.NormedSpace` `Mathlib.Analysis.Calculus.ContDiff.Basic` `Mathlib.Analysis.Calculus.ContDiff.Bounds` `Mathlib.Analysis.Calculus.ContDiff.CPolynomial` `Mathlib.Analysis.Calculus.ContDiff.Comp` `Mathlib.Analysis.Calculus.ContDiff.Defs` `Mathlib.Analysis.Calculus.ContDiff.Deriv` `Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries` `Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno` `Mathlib.Analysis.Calculus.ContDiff.Operations` `Mathlib.Analysis.Calculus.ContDiff.Polynomial` `Mathlib.Analysis.Calculus.ContDiff.RCLike` `Mathlib.Analysis.Calculus.ContDiff.RestrictScalars` `Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise` `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.CompMul` `Mathlib.Analysis.Calculus.Deriv.Comp` `Mathlib.Analysis.Calculus.Deriv.Inv` `Mathlib.Analysis.Calculus.Deriv.Inverse` `Mathlib.Analysis.Calculus.Deriv.Linear` `Mathlib.Analysis.Calculus.Deriv.MeanValue` `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.DerivativeTest` `Mathlib.Analysis.Calculus.DiffContOnCl` `Mathlib.Analysis.Calculus.FDeriv.Add` `Mathlib.Analysis.Calculus.FDeriv.Affine` `Mathlib.Analysis.Calculus.FDeriv.Analytic` `Mathlib.Analysis.Calculus.FDeriv.Basic` `Mathlib.Analysis.Calculus.FDeriv.Bilinear` `Mathlib.Analysis.Calculus.FDeriv.CompCLM` `Mathlib.Analysis.Calculus.FDeriv.Comp` `Mathlib.Analysis.Calculus.FDeriv.Congr` `Mathlib.Analysis.Calculus.FDeriv.Const` `Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap` `Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap` `Mathlib.Analysis.Calculus.FDeriv.Defs` `Mathlib.Analysis.Calculus.FDeriv.Equiv` `Mathlib.Analysis.Calculus.FDeriv.Extend` `Mathlib.Analysis.Calculus.FDeriv.Linear` `Mathlib.Analysis.Calculus.FDeriv.Mul` `Mathlib.Analysis.Calculus.FDeriv.Pi` `Mathlib.Analysis.Calculus.FDeriv.Pow` `Mathlib.Analysis.Calculus.FDeriv.Prod` `Mathlib.Analysis.Calculus.FDeriv.RestrictScalars` `Mathlib.Analysis.Calculus.FDeriv.Star` `Mathlib.Analysis.Calculus.FDeriv.Symmetric` `Mathlib.Analysis.Calculus.FormalMultilinearSeries` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv` `Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall` `Mathlib.Analysis.Calculus.IteratedDeriv.Defs` `Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno` `Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas` `Mathlib.Analysis.Calculus.IteratedDeriv.WithinZpow` `Mathlib.Analysis.Calculus.LHopital` `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.MeanValue` `Mathlib.Analysis.Calculus.SmoothSeries` `Mathlib.Analysis.Calculus.TangentCone.Basic` `Mathlib.Analysis.Calculus.TangentCone.Defs` `Mathlib.Analysis.Calculus.TangentCone.DimOne` `Mathlib.Analysis.Calculus.TangentCone.Pi` `Mathlib.Analysis.Calculus.TangentCone.Prod` `Mathlib.Analysis.Calculus.TangentCone.ProperSpace` `Mathlib.Analysis.Calculus.TangentCone.Real` `Mathlib.Analysis.Calculus.TangentCone.Seq` `Mathlib.Analysis.Calculus.TangentCone` `Mathlib.Analysis.Calculus.Taylor` `Mathlib.Analysis.Calculus.UniformLimitsDeriv` `Mathlib.Analysis.Calculus.VectorField` `Mathlib.Analysis.Complex.AbelLimit` `Mathlib.Analysis.Complex.Angle` `Mathlib.Analysis.Complex.Arg` `Mathlib.Analysis.Complex.Asymptotics` `Mathlib.Analysis.Complex.Basic` `Mathlib.Analysis.Complex.Circle` `Mathlib.Analysis.Complex.Convex` `Mathlib.Analysis.Complex.ExponentialBounds` `Mathlib.Analysis.Complex.Exponential` `Mathlib.Analysis.Complex.HalfPlane` `Mathlib.Analysis.Complex.IntegerCompl` `Mathlib.Analysis.Complex.Norm` `Mathlib.Analysis.Complex.Order` `Mathlib.Analysis.Complex.ReImTopology` `Mathlib.Analysis.Complex.RealDeriv` `Mathlib.Analysis.Complex.Spectrum` `Mathlib.Analysis.Complex.Trigonometric` `Mathlib.Analysis.Complex.UnitDisc.Basic` `Mathlib.Analysis.Complex.UpperHalfPlane.Basic` `Mathlib.Analysis.ConstantSpeed` `Mathlib.Analysis.Convex.AmpleSet` `Mathlib.Analysis.Convex.Body` `Mathlib.Analysis.Convex.Deriv` `Mathlib.Analysis.Convex.EGauge` `Mathlib.Analysis.Convex.GaugeRescale` `Mathlib.Analysis.Convex.Gauge` `Mathlib.Analysis.Convex.LinearIsometry` `Mathlib.Analysis.Convex.PartitionOfUnity` `Mathlib.Analysis.Convex.Side` `Mathlib.Analysis.Convex.SpecificFunctions.Basic` `Mathlib.Analysis.Convex.SpecificFunctions.Deriv` `Mathlib.Analysis.Convex.SpecificFunctions.Pow` `Mathlib.Analysis.Convex.StrictCombination` `Mathlib.Analysis.Convex.StrictConvexBetween` `Mathlib.Analysis.Convex.StrictConvexSpace` `Mathlib.Analysis.Convex.Strong` `Mathlib.Analysis.Convex.Uniform` `Mathlib.Analysis.Distribution.ContDiffMapSupportedIn` `Mathlib.Analysis.Distribution.Distribution` `Mathlib.Analysis.Distribution.TestFunction` `Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar` `Mathlib.Analysis.InnerProductSpace.Affine` `Mathlib.Analysis.InnerProductSpace.Basic` `Mathlib.Analysis.InnerProductSpace.Completion` `Mathlib.Analysis.InnerProductSpace.ConformalLinearMap` `Mathlib.Analysis.InnerProductSpace.Continuous` `Mathlib.Analysis.InnerProductSpace.Convex` `Mathlib.Analysis.InnerProductSpace.Defs` `Mathlib.Analysis.InnerProductSpace.LinearMap` `Mathlib.Analysis.InnerProductSpace.OfNorm` `Mathlib.Analysis.InnerProductSpace.Orthogonal` `Mathlib.Analysis.InnerProductSpace.Orthonormal` `Mathlib.Analysis.InnerProductSpace.Projection.Minimal` `Mathlib.Analysis.InnerProductSpace.Subspace` `Mathlib.Analysis.InnerProductSpace.Symmetric` `Mathlib.Analysis.LocallyConvex.AbsConvexOpen` `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.PointwiseConvergence` `Mathlib.Analysis.LocallyConvex.Polar` `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.Divisor` `Mathlib.Analysis.Meromorphic.FactorizedRational` `Mathlib.Analysis.Meromorphic.IsolatedZeros` `Mathlib.Analysis.Meromorphic.NormalForm` `Mathlib.Analysis.Meromorphic.Order` `Mathlib.Analysis.Meromorphic.TrailingCoefficient` `Mathlib.Analysis.Normed.Affine.AddTorsor` `Mathlib.Analysis.Normed.Affine.Ceva` `Mathlib.Analysis.Normed.Affine.ContinuousAffineMap` `Mathlib.Analysis.Normed.Affine.Isometry` `Mathlib.Analysis.Normed.Affine.MazurUlam` `Mathlib.Analysis.Normed.Affine.Simplex` `Mathlib.Analysis.Normed.Algebra.DualNumber` `Mathlib.Analysis.Normed.Algebra.Exponential` `Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt` `Mathlib.Analysis.Normed.Algebra.Ultra` `Mathlib.Analysis.Normed.Algebra.UnitizationL1` `Mathlib.Analysis.Normed.Algebra.Unitization` `Mathlib.Analysis.Normed.Field.Basic` `Mathlib.Analysis.Normed.Field.Instances` `Mathlib.Analysis.Normed.Field.Lemmas` `Mathlib.Analysis.Normed.Field.ProperSpace` `Mathlib.Analysis.Normed.Field.TransferInstance` `Mathlib.Analysis.Normed.Field.Ultra` `Mathlib.Analysis.Normed.Field.UnitBall` `Mathlib.Analysis.Normed.Group.AddCircle` `Mathlib.Analysis.Normed.Group.AddTorsor` `Mathlib.Analysis.Normed.Group.BallSphere` `Mathlib.Analysis.Normed.Group.Basic` `Mathlib.Analysis.Normed.Group.Bounded` `Mathlib.Analysis.Normed.Group.CocompactMap` `Mathlib.Analysis.Normed.Group.Completeness` `Mathlib.Analysis.Normed.Group.Completion` `Mathlib.Analysis.Normed.Group.Constructions` `Mathlib.Analysis.Normed.Group.Continuity` `Mathlib.Analysis.Normed.Group.ControlledClosure` `Mathlib.Analysis.Normed.Group.Defs` `Mathlib.Analysis.Normed.Group.FunctionSeries` `Mathlib.Analysis.Normed.Group.HomCompletion` `Mathlib.Analysis.Normed.Group.Hom` `Mathlib.Analysis.Normed.Group.Indicator` `Mathlib.Analysis.Normed.Group.InfiniteSum` `Mathlib.Analysis.Normed.Group.Int` `Mathlib.Analysis.Normed.Group.Lemmas` `Mathlib.Analysis.Normed.Group.NullSubmodule` `Mathlib.Analysis.Normed.Group.Pointwise` `Mathlib.Analysis.Normed.Group.Quotient` `Mathlib.Analysis.Normed.Group.Rat` `Mathlib.Analysis.Normed.Group.Real` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels` `Mathlib.Analysis.Normed.Group.SemiNormedGrp` `Mathlib.Analysis.Normed.Group.SeparationQuotient` `Mathlib.Analysis.Normed.Group.Subgroup` `Mathlib.Analysis.Normed.Group.Submodule` `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.Alternating.Basic` `Mathlib.Analysis.Normed.Module.Alternating.Curry` `Mathlib.Analysis.Normed.Module.Ball.Action` `Mathlib.Analysis.Normed.Module.Ball.Homeomorph` `Mathlib.Analysis.Normed.Module.Ball.Pointwise` `Mathlib.Analysis.Normed.Module.Ball.RadialEquiv` `Mathlib.Analysis.Normed.Module.Basic` `Mathlib.Analysis.Normed.Module.Completion` `Mathlib.Analysis.Normed.Module.Connected` `Mathlib.Analysis.Normed.Module.Convex` `Mathlib.Analysis.Normed.Module.ENormedSpace` `Mathlib.Analysis.Normed.Module.Extr` `Mathlib.Analysis.Normed.Module.MStructure` `Mathlib.Analysis.Normed.Module.Multilinear.Basic` `Mathlib.Analysis.Normed.Module.Multilinear.Curry` `Mathlib.Analysis.Normed.Module.Normalize` `Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm` `Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm` `Mathlib.Analysis.Normed.Module.RCLike.Basic` `Mathlib.Analysis.Normed.Module.RCLike.Extend` `Mathlib.Analysis.Normed.Module.RCLike.Real` `Mathlib.Analysis.Normed.Module.Ray` `Mathlib.Analysis.Normed.Module.RieszLemma` `Mathlib.Analysis.Normed.Module.Shrink` `Mathlib.Analysis.Normed.Module.Span` `Mathlib.Analysis.Normed.Module.TransferInstance` `Mathlib.Analysis.Normed.MulAction` `Mathlib.Analysis.Normed.Operator.Asymptotics` `Mathlib.Analysis.Normed.Operator.BanachSteinhaus` `Mathlib.Analysis.Normed.Operator.Banach` `Mathlib.Analysis.Normed.Operator.Basic` `Mathlib.Analysis.Normed.Operator.Bilinear` `Mathlib.Analysis.Normed.Operator.BoundedLinearMaps` `Mathlib.Analysis.Normed.Operator.Compact` `Mathlib.Analysis.Normed.Operator.Completeness` `Mathlib.Analysis.Normed.Operator.Conformal` `Mathlib.Analysis.Normed.Operator.ContinuousLinearMap` `Mathlib.Analysis.Normed.Operator.Extend` `Mathlib.Analysis.Normed.Operator.LinearIsometry` `Mathlib.Analysis.Normed.Operator.Mul` `Mathlib.Analysis.Normed.Operator.NNNorm` `Mathlib.Analysis.Normed.Operator.NormedSpace` `Mathlib.Analysis.Normed.Operator.Prod` `Mathlib.Analysis.Normed.Order.Basic` `Mathlib.Analysis.Normed.Order.Hom.Basic` `Mathlib.Analysis.Normed.Order.Hom.Ultra` `Mathlib.Analysis.Normed.Order.Lattice` `Mathlib.Analysis.Normed.Order.UpperLower` `Mathlib.Analysis.Normed.Ring.Basic` `Mathlib.Analysis.Normed.Ring.Finite` `Mathlib.Analysis.Normed.Ring.InfiniteSum` `Mathlib.Analysis.Normed.Ring.Int` `Mathlib.Analysis.Normed.Ring.Lemmas` `Mathlib.Analysis.Normed.Ring.TransferInstance` `Mathlib.Analysis.Normed.Ring.Ultra` `Mathlib.Analysis.Normed.Ring.Units` `Mathlib.Analysis.Normed.Ring.WithAbs` `Mathlib.Analysis.Normed.Unbundled.AlgebraNorm` `Mathlib.Analysis.Normed.Unbundled.FiniteExtension` `Mathlib.Analysis.Normed.Unbundled.InvariantExtension` `Mathlib.Analysis.Normed.Unbundled.IsPowMulFaithful` `Mathlib.Analysis.Normed.Unbundled.RingSeminorm` `Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded` `Mathlib.Analysis.Normed.Unbundled.SeminormFromConst` `Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm` `Mathlib.Analysis.NormedSpace.Alternating.Basic` `Mathlib.Analysis.NormedSpace.Alternating.Curry` `Mathlib.Analysis.NormedSpace.Alternating.Uncurry.Fin` `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.HahnBanach.Extension` `Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual` `Mathlib.Analysis.NormedSpace.HahnBanach.Separation` `Mathlib.Analysis.NormedSpace.HomeomorphBall` `Mathlib.Analysis.NormedSpace.IndicatorFunction` `Mathlib.Analysis.NormedSpace.Int` `Mathlib.Analysis.NormedSpace.MStructure` `Mathlib.Analysis.NormedSpace.Multilinear.Basic` `Mathlib.Analysis.NormedSpace.Multilinear.Curry` `Mathlib.Analysis.NormedSpace.Normalize` `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.ODE.Gronwall` `Mathlib.Analysis.PSeries` `Mathlib.Analysis.Polynomial.Basic` `Mathlib.Analysis.Polynomial.CauchyBound` `Mathlib.Analysis.Polynomial.Norm` `Mathlib.Analysis.RCLike.Basic` `Mathlib.Analysis.RCLike.BoundedContinuous` `Mathlib.Analysis.RCLike.Extend` `Mathlib.Analysis.RCLike.Sqrt` `Mathlib.Analysis.RCLike.TangentCone` `Mathlib.Analysis.Real.OfDigits` `Mathlib.Analysis.Real.Pi.Bounds` `Mathlib.Analysis.Seminorm` `Mathlib.Analysis.SpecialFunctions.Arcosh` `Mathlib.Analysis.SpecialFunctions.Arsinh` `Mathlib.Analysis.SpecialFunctions.Artanh` `Mathlib.Analysis.SpecialFunctions.Bernstein` `Mathlib.Analysis.SpecialFunctions.BinaryEntropy` `Mathlib.Analysis.SpecialFunctions.Choose` `Mathlib.Analysis.SpecialFunctions.CompareExp` `Mathlib.Analysis.SpecialFunctions.Complex.Arg` `Mathlib.Analysis.SpecialFunctions.Complex.CircleMap` `Mathlib.Analysis.SpecialFunctions.Complex.Circle` `Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv` `Mathlib.Analysis.SpecialFunctions.Complex.Log` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic` `Mathlib.Analysis.SpecialFunctions.ExpDeriv` `Mathlib.Analysis.SpecialFunctions.Exp` `Mathlib.Analysis.SpecialFunctions.Exponential` `Mathlib.Analysis.SpecialFunctions.Log.Base` `Mathlib.Analysis.SpecialFunctions.Log.Basic` `Mathlib.Analysis.SpecialFunctions.Log.Deriv` `Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp` `Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog` `Mathlib.Analysis.SpecialFunctions.Log.ERealExp` `Mathlib.Analysis.SpecialFunctions.Log.InvLog` `Mathlib.Analysis.SpecialFunctions.Log.Monotone` `Mathlib.Analysis.SpecialFunctions.Log.NegMulLog` `Mathlib.Analysis.SpecialFunctions.Log.PosLog` `Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto` `Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq` `Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric` `Mathlib.Analysis.SpecialFunctions.Pochhammer` `Mathlib.Analysis.SpecialFunctions.PolynomialExp` `Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics` `Mathlib.Analysis.SpecialFunctions.Pow.Complex` `Mathlib.Analysis.SpecialFunctions.Pow.Continuity` `Mathlib.Analysis.SpecialFunctions.Pow.Deriv` `Mathlib.Analysis.SpecialFunctions.Pow.NNReal` `Mathlib.Analysis.SpecialFunctions.Pow.Real` `Mathlib.Analysis.SpecialFunctions.Sigmoid` `Mathlib.Analysis.SpecialFunctions.SmoothTransition` `Mathlib.Analysis.SpecialFunctions.Sqrt` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle` `Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev` `Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex` `Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Series` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc` `Mathlib.Analysis.SpecificLimits.Fibonacci` `Mathlib.Analysis.SpecificLimits.FloorPow` `Mathlib.Analysis.SpecificLimits.Normed` `Mathlib.Analysis.SpecificLimits.RCLike` `Mathlib.Analysis.SumOverResidueClass` `Mathlib.Combinatorics.Additive.Corner.Roth` `Mathlib.Combinatorics.Derangements.Exponential` `Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity` `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.AkraBazzi` `Mathlib.Computability.AkraBazzi.GrowsPolynomially` `Mathlib.Computability.AkraBazzi.SumTransform` `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.EffectiveEpi` `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.EffectiveEpi` `Mathlib.Condensed.Light.Epi` `Mathlib.Condensed.Light.Explicit` `Mathlib.Condensed.Light.Functors` `Mathlib.Condensed.Light.Instances` `Mathlib.Condensed.Light.InternallyProjective` `Mathlib.Condensed.Light.Limits` `Mathlib.Condensed.Light.Module` `Mathlib.Condensed.Light.Monoidal` `Mathlib.Condensed.Light.Small` `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.ExponentialBounds` `Mathlib.Data.Complex.Exponential` `Mathlib.Data.Complex.Norm` `Mathlib.Data.Complex.Order` `Mathlib.Data.Complex.Trigonometric` `Mathlib.Data.Real.Pi.Bounds` `Mathlib.Dynamics.BirkhoffSum.NormedSpace` `Mathlib.Dynamics.Ergodic.Function` `Mathlib.Dynamics.TopologicalEntropy.CoverEntropy` `Mathlib.Dynamics.TopologicalEntropy.NetEntropy` `Mathlib.Dynamics.TopologicalEntropy.Semiconj` `Mathlib.Dynamics.TopologicalEntropy.Subset` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal` `Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle` `Mathlib.Geometry.Euclidean.Basic` `Mathlib.Geometry.Euclidean.Inversion.Basic` `Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane` `Mathlib.Geometry.Euclidean.PerpBisector` `Mathlib.Geometry.Euclidean.Simplex` `Mathlib.Geometry.Manifold.ConformalGroupoid` `Mathlib.Geometry.Manifold.IsManifold.Basic` `Mathlib.Geometry.Manifold.LocalSourceTargetProperty` `Mathlib.InformationTheory.Hamming` `Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus` `Mathlib.LinearAlgebra.Matrix.LDL` `Mathlib.MeasureTheory.Constructions.BorelSpace.Complex` `Mathlib.MeasureTheory.Constructions.BorelSpace.Metric` `Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable` `Mathlib.MeasureTheory.Constructions.Polish.Basic` `Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal` `Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable` `Mathlib.MeasureTheory.Function.AEEqFun` `Mathlib.MeasureTheory.Function.AEEqOfLIntegral` `Mathlib.MeasureTheory.Function.ConvergenceInMeasure` `Mathlib.MeasureTheory.Function.Egorov` `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.Defs` `Mathlib.MeasureTheory.Function.LpSeminorm.Indicator` `Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity` `Mathlib.MeasureTheory.Function.LpSeminorm.Prod` `Mathlib.MeasureTheory.Function.LpSeminorm.SMul` `Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality` `Mathlib.MeasureTheory.Function.LpSeminorm.Trim` `Mathlib.MeasureTheory.Function.LpSpace.Basic` `Mathlib.MeasureTheory.Function.LpSpace.Complete` `Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions` `Mathlib.MeasureTheory.Function.LpSpace.Indicator` `Mathlib.MeasureTheory.Function.Piecewise` `Mathlib.MeasureTheory.Function.SimpleFuncDense` `Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan` `Mathlib.MeasureTheory.Function.SpecialFunctions.Basic` `Mathlib.MeasureTheory.Function.SpecialFunctions.Inner` `Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic` `Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner` `Mathlib.MeasureTheory.Integral.Indicator` `Mathlib.MeasureTheory.Integral.Lebesgue.Norm` `Mathlib.MeasureTheory.Integral.LebesgueNormedSpace` `Mathlib.MeasureTheory.Integral.MeanInequalities` `Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic` `Mathlib.MeasureTheory.Measure.Complex` `Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue` `Mathlib.MeasureTheory.Measure.PreVariation` `Mathlib.MeasureTheory.Measure.RegularityCompacts` `Mathlib.MeasureTheory.Measure.SubFinite` `Mathlib.MeasureTheory.VectorMeasure.AddContent` `Mathlib.MeasureTheory.VectorMeasure.Variation.Defs` `Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt` `Mathlib.NumberTheory.ArithmeticFunction` `Mathlib.NumberTheory.Bertrand` `Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree` `Mathlib.NumberTheory.EulerProduct.Basic` `Mathlib.NumberTheory.Harmonic.EulerMascheroni` `Mathlib.NumberTheory.Harmonic.Int` `Mathlib.NumberTheory.Height.Basic` `Mathlib.NumberTheory.Padics.AddChar` `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.Padics.ValuativeRel` `Mathlib.NumberTheory.SumPrimeReciprocals` `Mathlib.NumberTheory.Transcendental.Liouville.Basic` `Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber` `Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith` `Mathlib.NumberTheory.Transcendental.Liouville.Residual` `Mathlib.NumberTheory.TsumDivisorsAntidiagonal` `Mathlib.NumberTheory.TsumDivsorsAntidiagonal` `Mathlib.NumberTheory.VonMangoldt` `Mathlib.Order.Filter.ZeroAndBoundedAtFilter` `Mathlib.Probability.Decision.Risk.Basic` `Mathlib.Probability.Distributions.Geometric` `Mathlib.Probability.Distributions.Poisson` `Mathlib.Probability.Independence.Basic` `Mathlib.Probability.Independence.Kernel.IndepFun` `Mathlib.Probability.Independence.Kernel.Indep` `Mathlib.Probability.Independence.Kernel` `Mathlib.Probability.Independence.Process` `Mathlib.Probability.Kernel.Composition.Lemmas` `Mathlib.Probability.Kernel.Composition.MeasureCompProd` `Mathlib.Probability.Kernel.Composition.MeasureComp` `Mathlib.Probability.Kernel.Disintegration.Basic` `Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes` `Mathlib.Probability.Kernel.Invariance` `Mathlib.Probability.Process.Kolmogorov` `Mathlib.RingTheory.DividedPowers.Padic` `Mathlib.RingTheory.HahnSeries.HahnEmbedding` `Mathlib.RingTheory.Polynomial.Hermite.Gaussian` `Mathlib.RingTheory.PowerSeries.Restricted` `Mathlib.RingTheory.Valuation.RankOne` `Mathlib.Tactic.ComputeAsymptotics.Lemmas` `Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis` `Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion` `Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized` `Mathlib.Tactic.NormNum.Irrational` `Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic` `Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion` `Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits` `Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt` `Mathlib.Topology.Algebra.InfiniteSum.Field` `Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn` `Mathlib.Topology.Algebra.Module.Alternating.Topology` `Mathlib.Topology.Algebra.Module.Cardinality` `Mathlib.Topology.Algebra.Module.Multilinear.Bounded` `Mathlib.Topology.Algebra.Module.Multilinear.Topology` `Mathlib.Topology.Algebra.Module.PerfectSpace` `Mathlib.Topology.Algebra.Module.PointwiseConvergence` `Mathlib.Topology.Algebra.Module.StrongDual` `Mathlib.Topology.Algebra.Module.StrongTopology` `Mathlib.Topology.Algebra.Module.TransferInstance` `Mathlib.Topology.Algebra.Module.UniformConvergence` `Mathlib.Topology.Algebra.Polynomial` `Mathlib.Topology.Algebra.PontryaginDual` `Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous` `Mathlib.Topology.Algebra.Valued.NormedValued` `Mathlib.Topology.Bornology.BoundedOperation` `Mathlib.Topology.CWComplex.Classical.Basic` `Mathlib.Topology.CWComplex.Classical.Finite` `Mathlib.Topology.CWComplex.Classical.Subcomplex` `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.Cartesian` `Mathlib.Topology.Category.LightProfinite.EffectiveEpi` `Mathlib.Topology.Category.LightProfinite.Extend` `Mathlib.Topology.Category.LightProfinite.Injective` `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.Basic` `Mathlib.Topology.Category.Profinite.Nobeling.Induction` `Mathlib.Topology.Category.Profinite.Nobeling.Span` `Mathlib.Topology.Category.Profinite.Nobeling.Successor` `Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit` `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.Compactness.HilbertCubeEmbedding` `Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli` `Mathlib.Topology.ContinuousMap.Bounded.Basic` `Mathlib.Topology.ContinuousMap.Bounded.Normed` `Mathlib.Topology.ContinuousMap.Bounded.Star` `Mathlib.Topology.ContinuousMap.BoundedCompactlySupported` `Mathlib.Topology.ContinuousMap.Compact` `Mathlib.Topology.ContinuousMap.CompactlySupported` `Mathlib.Topology.ContinuousMap.ContinuousMapZero` `Mathlib.Topology.ContinuousMap.ContinuousSqrt` `Mathlib.Topology.ContinuousMap.Ideals` `Mathlib.Topology.ContinuousMap.Polynomial` `Mathlib.Topology.ContinuousMap.StarOrdered` `Mathlib.Topology.ContinuousMap.StoneWeierstrass` `Mathlib.Topology.ContinuousMap.Units` `Mathlib.Topology.ContinuousMap.Weierstrass` `Mathlib.Topology.ContinuousMap.ZeroAtInfty` `Mathlib.Topology.EMetricSpace.PairReduction` `Mathlib.Topology.Instances.CantorSet` `Mathlib.Topology.Instances.Complex` `Mathlib.Topology.MetricSpace.CantorScheme` `Mathlib.Topology.MetricSpace.CauSeqFilter` `Mathlib.Topology.MetricSpace.GromovHausdorffRealized` `Mathlib.Topology.MetricSpace.GromovHausdorff` `Mathlib.Topology.MetricSpace.HausdorffAlexandroff` `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.Snowflaking` `Mathlib.Topology.MetricSpace.ThickenedIndicator` `Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps` `Mathlib.Topology.MetricSpace.UniformConvergence` `Mathlib.Topology.Metrizable.Urysohn` `Mathlib.Topology.Order.Category.FrameAdjunction` `Mathlib.Topology.PartitionOfUnity` `Mathlib.Topology.Separation.CompletelyRegular` `Mathlib.Topology.Separation.Lemmas` `Mathlib.Topology.TietzeExtension` `Mathlib.Topology.UniformSpace.Dini` `Mathlib.Topology.UniformSpace.Uniformizable` `Mathlib.Topology.UrysohnsBounded` `Mathlib.Topology.UrysohnsLemma` `Mathlib.Topology.VectorBundle.Basic` `Mathlib.Topology.VectorBundle.Constructions` `Mathlib.Topology.VectorBundle.Hom` `Mathlib.Topology.VectorBundle.Riemannian`	3

Declarations diff

+ LipschitzOnWith.norm_inv_mul_le
+ LipschitzOnWith.norm_inv_mul_le_of_le
+ LipschitzWith.norm_inv_mul_le
+ LipschitzWith.norm_inv_mul_le_of_le
+ NormedAddCommGroup.nhds_zero_basis_norm_lt
+ NormedAddCommGroup.tendsto_nhds_zero
+ NormedGroup.nhds_basis_norm_lt
+ NormedGroup.nhds_one_basis_norm_lt
+ NormedGroup.tendsto_nhds_nhds
+ NormedGroup.tendsto_nhds_one
+ NormedGroup.to_isIsometricSMul
+ NormedGroup.uniformity_basis_dist
+ SeminormedGroup.mem_closure_iff
+ abs_norm_sub_norm_le_norm_inv_mul
+ ball_eq_metric
+ ball_eq_norm_inv_mul_lt
+ closedBall_eq_metric
+ dist_eq_eLpNorm_neg_add
+ dist_eq_norm_inv_mul
+ dist_eq_norm_inv_mul'
+ dist_norm_norm_le_norm_inv_mul
+ edist_eq_eLpNorm_neg_add
+ edist_eq_enorm_inv_mul
+ lipschitzOnWith_iff_norm_inv_mul_le
+ lipschitzWith_iff_norm_inv_mul_le
+ map_inv_mul
+ mem_ball_iff_norm_inv_mul_lt
+ mem_ball_iff_norm_inv_mul_lt'
+ mem_closedBall_iff_norm_inv_mul_le
+ mem_closedBall_iff_norm_inv_mul_le'
+ mem_sphere_iff_norm_inv_mul_eq
+ nndist_eq_nnnorm_inv_mul
+ nndist_nnnorm_nnnorm_le_nnnorm_inv_mul
+ norm_inv_mul
+ norm_le_norm_add_norm_inv_mul
+ norm_sub_norm_le_norm_inv_mul
+ opNorm_neg
+ tendsto_iff_norm_inv_mul_tendsto_zero
+ tendsto_norm_inv_mul_self
+ tendsto_norm_inv_mul_self_nhdsGE
+ tendsto_norm_inv_mul_self_nhdsNE
- NormedGroup.to_isIsometricSMul_right

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

Mathlib/Analysis/Normed/Group/Defs.lean

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>

mathlib-merge-conflicts · 2026-02-13T15:52:17Z

This pull request has conflicts, please merge master and resolve them.

We have currently a specific definition of the right uniformity of a topological group, but not of the left uniformity. We introduce it in the current PR, for two reasons. First, there is no reason to favor one over the other. Second, it is needed in #35037, which changes the formula for the distance in a normed group to make it left-invariant following standard conventions. We also prove that a group is complete for its left-uniformity iff it is complete for its right-uniformity, by showing that inversion is a uniform equivalence between the two uniformities. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

mathlib-dependent-issues · 2026-02-16T22:06:14Z

This PR/issue depends on:

~~[Merged by Bors] - feat: the left uniformity in a group #35252~~
~~[Merged by Bors] - feat: inv lemmas for uniform convergence, missing to_fun attributes #35384~~
By Dependent Issues (🤖). Happy coding!

YaelDillies

Thanks!

maintainer delegate

YaelDillies · 2026-02-17T16:45:14Z

Mathlib/Analysis/Normed/Group/Defs.lean

 public import Mathlib.Topology.Order.Real
 public import Mathlib.Algebra.Order.BigOperators.Ring.Finset
 public import Mathlib.Algebra.Order.Module.Field
+public import Mathlib.Tactic.Group


Should this be private instead?

Otherwise, it doesn't make the tactic available in downstream files, right? In an earlier version the import was not public, and it broke other files.

YaelDillies · 2026-02-17T16:46:34Z

Mathlib/Analysis/Normed/Group/Ultra.lean

+    have : x⁻¹ * y * (y⁻¹ * z) = x⁻¹ * z := by
+      rw [mul_assoc, ← mul_assoc y, mul_inv_cancel, one_mul]


Do you still need this given the lemma you added?

YaelDillies · 2026-02-17T16:46:48Z

Mathlib/Analysis/Normed/Group/Uniform.lean

+    have : b⁻¹ * a⁻¹ * (a * c) = b⁻¹ * c := by
+      rw [mul_assoc, ← mul_assoc a⁻¹, inv_mul_cancel, one_mul]


YaelDillies · 2026-02-17T16:47:08Z

Mathlib/Analysis/Normed/Group/Uniform.lean

 @[to_additive]
-instance NormedGroup.to_isIsometricSMul_left : IsIsometricSMul E E :=
-  ⟨fun a => Isometry.of_dist_eq fun b c => by simp [dist_eq_norm_div]⟩
+instance NormedGroup.to_isIsometricSMul_left : IsIsometricSMul Eᵐᵒᵖ E :=


github-actions · 2026-02-17T16:49:49Z

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

start

c49fd58

sgouezel marked this pull request as draft February 9, 2026 17:16

sgouezel changed the title ~~chore: change definition of distance in normed group~~ refactor: change definition of distance in normed group Feb 9, 2026

github-actions bot added the t-analysis Analysis (normed *, calculus) label Feb 9, 2026

fix

83ea9c6

themathqueen reviewed Feb 9, 2026

View reviewed changes

Mathlib/Analysis/Normed/Group/Defs.lean Outdated Show resolved Hide resolved

themathqueen reviewed Feb 9, 2026

View reviewed changes

Mathlib/Analysis/Normed/Group/Defs.lean Outdated Show resolved Hide resolved

sgouezel and others added 16 commits February 10, 2026 09:10

better

f1a01ed

Update Mathlib/Analysis/Normed/Group/Defs.lean

6bebe1a

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>

cleanup

f32f451

fix

a035bde

start fixing

7b074b1

progress

a83d7b4

fix name

2ea00d7

oops

f8a8643

better

cf2813f

progress

379d152

better

81f6318

save

cb30d0e

fix

3f52079

better

4d6cf1e

better

db253a1

fix

2a54ce3

github-actions bot 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 11, 2026

sgouezel added 5 commits February 11, 2026 15:02

fix

64a0674

fix

631efc8

fix

704bae2

more

4032665

fix lipschitz

28ddca2

sgouezel added 6 commits February 11, 2026 17:00

better

b954b49

more

e677cff

more fixes

f59c79d

fix

3bdb840

fix

8386204

merge master

78ae7d9

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 12, 2026

sgouezel added 3 commits February 12, 2026 13:08

fix

118b71b

hint test file

4bf7dd3

start cleaning up

e83b387

sgouezel mentioned this pull request Feb 12, 2026

refactor(Normed/Group/Quotient): generalise to non-abelian groups #21342

Open

2 tasks

YaelDillies self-assigned this Feb 13, 2026

mathlib-merge-conflicts bot 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 13, 2026

sgouezel mentioned this pull request Feb 15, 2026

[Merged by Bors] - feat: the left uniformity in a group #35252

Closed

mathlib-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 15, 2026

mathlib-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 16, 2026

merge master

51c7519

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 17, 2026

sgouezel added 3 commits February 17, 2026 11:42

missing import

750e43d

fix

4f77eb5

fix test

f86fc76

sgouezel marked this pull request as ready for review February 17, 2026 12:44

missing deprecation

7f6abf6

YaelDillies approved these changes Feb 17, 2026

View reviewed changes

mathlib-triage bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Feb 17, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

refactor: change definition of distance in normed group#35037

refactor: change definition of distance in normed group#35037
sgouezel wants to merge 37 commits intoleanprover-community:masterfrom
sgouezel:SG_normedGroup

sgouezel commented Feb 9, 2026 •

edited

Loading

Uh oh!

github-actions bot commented Feb 9, 2026 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

mathlib-merge-conflicts bot commented Feb 13, 2026

Uh oh!

mathlib-dependent-issues bot commented Feb 16, 2026

Uh oh!

YaelDillies left a comment

Uh oh!

YaelDillies Feb 17, 2026

Uh oh!

sgouezel Feb 17, 2026

Uh oh!

YaelDillies Feb 17, 2026

Uh oh!

YaelDillies Feb 17, 2026

Uh oh!

YaelDillies Feb 17, 2026

Uh oh!

github-actions bot commented Feb 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

		have : x⁻¹ * y * (y⁻¹ * z) = x⁻¹ * z := by
		rw [mul_assoc, ← mul_assoc y, mul_inv_cancel, one_mul]

		have : b⁻¹ * a⁻¹ * (a * c) = b⁻¹ * c := by
		rw [mul_assoc, ← mul_assoc a⁻¹, inv_mul_cancel, one_mul]

Conversation

sgouezel commented Feb 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary 4d984d0bb1

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

mathlib-merge-conflicts bot commented Feb 13, 2026

Uh oh!

mathlib-dependent-issues bot commented Feb 16, 2026

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

YaelDillies Feb 17, 2026

Choose a reason for hiding this comment

Uh oh!

sgouezel Feb 17, 2026

Choose a reason for hiding this comment

Uh oh!

YaelDillies Feb 17, 2026

Choose a reason for hiding this comment

Uh oh!

YaelDillies Feb 17, 2026

Choose a reason for hiding this comment

Uh oh!

YaelDillies Feb 17, 2026

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Feb 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

sgouezel commented Feb 9, 2026 •

edited

Loading

github-actions bot commented Feb 9, 2026 •

edited

Loading