refactor(*): use `IsSelfInv` and `IsSelfNeg` by justus-springer · Pull Request #43774 · leanprover-community/mathlib4

justus-springer · 2026-09-13T13:15:15Z

Use the recently added IsSelfInv and IsSelfNeg to do some small refactors. In particular:

In Combinatorics/Additive/ApproximateSubgroup, use IsSelfInv/IsSelfNeg in the definition of approximate subgroups. Proofs get slightly shorter.
In Geometry/Group/Growth/QuotientInter, Topology/Algebra/Group/OpenMapping and Topology/Algebra/Group/Pointwise: Replace hypotheses of the form A⁻¹ = A and ∀ x ∈ s, x⁻¹ ∈ s by IsSelfInv. Mainly a cosmetic change.
Topology/Algebra/OpenSubgroup: Use IsSelfNeg in the definition of IsTopologicalAddGroup.addNegClosureNhd. This allows for a 5-line golf.

Generative AI was used to search Mathlib for possibilities of using IsSelfInv/IsSelfNeg and suggest refactors. I reviewed every line and did small tweaks.

depends on: feat(Algebra/Group/Pointwise/Set/SelfInv): a few more lemmas about self-inverse sets #43773

github-actions · 2026-09-13T13:16:18Z

PR summary 41e098532e

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Combinatorics.Additive.ApproximateSubgroup	1090	1092	+2 (+0.18%)

Import changes for all files

Files	Import difference
2159 files `Mathlib.Algebra.Category.Grp.EnoughInjectives` `Mathlib.Algebra.Category.Grp.LargeColimits` `Mathlib.Algebra.Category.Grp.Ulift` `Mathlib.Algebra.Category.ModuleCat.EnoughInjectives` `Mathlib.Algebra.Category.ModuleCat.Ext.Baer` `Mathlib.Algebra.Category.ModuleCat.InjectiveDimension` `Mathlib.Algebra.Category.ModuleCat.Topology.Basic` `Mathlib.Algebra.Category.ModuleCat.Topology.Homology` `Mathlib.Algebra.Lie.Basis.Base` `Mathlib.Algebra.Lie.Basis` `Mathlib.Algebra.Lie.Weights.IsSimple` `Mathlib.Algebra.Lie.Weights.RootSystem` `Mathlib.Algebra.Module.CharacterModule` `Mathlib.Algebra.Module.SpanRankOperations` `Mathlib.Algebra.Module.StablyFree.FreeOfInvertible` `Mathlib.Algebra.Module.Torsion.PrimaryComponent` `Mathlib.Algebra.Module.ZLattice.Basic` `Mathlib.Algebra.Module.ZLattice.Covolume` `Mathlib.Algebra.Module.ZLattice.Summable` `Mathlib.Algebra.Order.Archimedean.Real.Hom` `Mathlib.Algebra.Order.Ring.StandardPart` `Mathlib.Algebra.Order.Star.Real` `Mathlib.Algebra.Star.CHSH` `Mathlib.AlgebraicGeometry.AffineScheme` `Mathlib.AlgebraicGeometry.AffineSpace` `Mathlib.AlgebraicGeometry.AffineTransitionLimit` `Mathlib.AlgebraicGeometry.AlgClosed.Basic` `Mathlib.AlgebraicGeometry.AlgebraicCycle.Basic` `Mathlib.AlgebraicGeometry.Artinian` `Mathlib.AlgebraicGeometry.Birational.Birational` `Mathlib.AlgebraicGeometry.Birational.Composition` `Mathlib.AlgebraicGeometry.Birational.Dominant` `Mathlib.AlgebraicGeometry.Birational.RationalMap` `Mathlib.AlgebraicGeometry.ColimitsOver` `Mathlib.AlgebraicGeometry.Cover.Directed` `Mathlib.AlgebraicGeometry.Cover.Over` `Mathlib.AlgebraicGeometry.Cover.QuasiCompact` `Mathlib.AlgebraicGeometry.Cover.Sigma` `Mathlib.AlgebraicGeometry.EffectiveEpi` `Mathlib.AlgebraicGeometry.EllipticCurve.LFunction` `Mathlib.AlgebraicGeometry.EllipticCurve.Reduction` `Mathlib.AlgebraicGeometry.Fiber` `Mathlib.AlgebraicGeometry.FunctionField` `Mathlib.AlgebraicGeometry.Geometrically.Basic` `Mathlib.AlgebraicGeometry.Geometrically.Connected` `Mathlib.AlgebraicGeometry.Geometrically.Integral` `Mathlib.AlgebraicGeometry.Geometrically.Irreducible` `Mathlib.AlgebraicGeometry.Geometrically.Reduced` `Mathlib.AlgebraicGeometry.GluingOneHypercover` `Mathlib.AlgebraicGeometry.Group.Abelian` `Mathlib.AlgebraicGeometry.Group.Affine` `Mathlib.AlgebraicGeometry.Group.Smooth` `Mathlib.AlgebraicGeometry.IdealSheaf.Basic` `Mathlib.AlgebraicGeometry.IdealSheaf.Functorial` `Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent` `Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme` `Mathlib.AlgebraicGeometry.LimitsOver` `Mathlib.AlgebraicGeometry.Limits` `Mathlib.AlgebraicGeometry.Modules.Tilde` `Mathlib.AlgebraicGeometry.Morphisms.AffineAnd` `Mathlib.AlgebraicGeometry.Morphisms.Affine` `Mathlib.AlgebraicGeometry.Morphisms.Basic` `Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Constructors` `Mathlib.AlgebraicGeometry.Morphisms.Descent` `Mathlib.AlgebraicGeometry.Morphisms.Etale` `Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation` `Mathlib.AlgebraicGeometry.Morphisms.FiniteType` `Mathlib.AlgebraicGeometry.Morphisms.Finite` `Mathlib.AlgebraicGeometry.Morphisms.FlatDescent` `Mathlib.AlgebraicGeometry.Morphisms.FlatMono` `Mathlib.AlgebraicGeometry.Morphisms.FlatRank` `Mathlib.AlgebraicGeometry.Morphisms.Flat` `Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified` `Mathlib.AlgebraicGeometry.Morphisms.Immersion` `Mathlib.AlgebraicGeometry.Morphisms.Integral` `Mathlib.AlgebraicGeometry.Morphisms.IsIso` `Mathlib.AlgebraicGeometry.Morphisms.LocalClosure` `Mathlib.AlgebraicGeometry.Morphisms.LocalFlatDescent` `Mathlib.AlgebraicGeometry.Morphisms.LocalIso` `Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion` `Mathlib.AlgebraicGeometry.Morphisms.Preimmersion` `Mathlib.AlgebraicGeometry.Morphisms.Proper` `Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact` `Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite` `Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated` `Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties` `Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant` `Mathlib.AlgebraicGeometry.Morphisms.Separated` `Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber` `Mathlib.AlgebraicGeometry.Morphisms.Smooth` `Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks` `Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective` `Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen` `Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale` `Mathlib.AlgebraicGeometry.Noetherian` `Mathlib.AlgebraicGeometry.Normalization` `Mathlib.AlgebraicGeometry.OrderOfVanishing` `Mathlib.AlgebraicGeometry.PointsPi` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper` `Mathlib.AlgebraicGeometry.Properties` `Mathlib.AlgebraicGeometry.PullbackCarrier` `Mathlib.AlgebraicGeometry.Pullbacks` `Mathlib.AlgebraicGeometry.QuasiAffine` `Mathlib.AlgebraicGeometry.RelativeGluing` `Mathlib.AlgebraicGeometry.ResidueField` `Mathlib.AlgebraicGeometry.Sites.AffineEtale` `Mathlib.AlgebraicGeometry.Sites.Affine` `Mathlib.AlgebraicGeometry.Sites.BigZariski` `Mathlib.AlgebraicGeometry.Sites.ConstantSheaf` `Mathlib.AlgebraicGeometry.Sites.ElladicCohomology` `Mathlib.AlgebraicGeometry.Sites.EtalePoint` `Mathlib.AlgebraicGeometry.Sites.Etale` `Mathlib.AlgebraicGeometry.Sites.Fpqc` `Mathlib.AlgebraicGeometry.Sites.Pretopology` `Mathlib.AlgebraicGeometry.Sites.Proetale` `Mathlib.AlgebraicGeometry.Sites.QuasiCompact` `Mathlib.AlgebraicGeometry.Sites.Representability` `Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact` `Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski` `Mathlib.AlgebraicGeometry.Sites.Small` `Mathlib.AlgebraicGeometry.SpreadingOut` `Mathlib.AlgebraicGeometry.Stalk` `Mathlib.AlgebraicGeometry.ValuativeCriterion` `Mathlib.AlgebraicGeometry.ZariskisMainTheorem` `Mathlib.Analysis.AbsoluteValue.Equivalence` `Mathlib.Analysis.Analytic.Basic` `Mathlib.Analysis.Analytic.Binomial` `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.Polynomial` `Mathlib.Analysis.Analytic.RadiusLiminf` `Mathlib.Analysis.Analytic.Uniqueness` `Mathlib.Analysis.Analytic.WithLp` `Mathlib.Analysis.Analytic.Within` `Mathlib.Analysis.AperiodicOrder.Delone.Basic` `Mathlib.Analysis.Asymptotics.Arith` `Mathlib.Analysis.Asymptotics.AsymptoticEquivalent` `Mathlib.Analysis.Asymptotics.Completion` `Mathlib.Analysis.Asymptotics.ExpGrowth` `Mathlib.Analysis.Asymptotics.Lemmas` `Mathlib.Analysis.Asymptotics.LinearGrowth` `Mathlib.Analysis.Asymptotics.Ring` `Mathlib.Analysis.Asymptotics.SpecificAsymptotics` `Mathlib.Analysis.Asymptotics.SuperpolynomialDecay` `Mathlib.Analysis.Asymptotics.TVS` `Mathlib.Analysis.Asymptotics.Theta` `Mathlib.Analysis.BoundedVariation` `Mathlib.Analysis.BoxIntegral.Basic` `Mathlib.Analysis.BoxIntegral.Box.SubboxInduction` `Mathlib.Analysis.BoxIntegral.DivergenceTheorem` `Mathlib.Analysis.BoxIntegral.Integrability` `Mathlib.Analysis.BoxIntegral.Partition.Additive` `Mathlib.Analysis.BoxIntegral.Partition.Filter` `Mathlib.Analysis.BoxIntegral.Partition.Measure` `Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction` `Mathlib.Analysis.BoxIntegral.UnitPartition` `Mathlib.Analysis.CStarAlgebra.ApproximateUnit` `Mathlib.Analysis.CStarAlgebra.Basic` `Mathlib.Analysis.CStarAlgebra.CStarMatrix` `Mathlib.Analysis.CStarAlgebra.Classes` `Mathlib.Analysis.CStarAlgebra.Commutative.PosPart` `Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Pi` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Transfer` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary` `Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap` `Mathlib.Analysis.CStarAlgebra.ContinuousMap` `Mathlib.Analysis.CStarAlgebra.Exponential` `Mathlib.Analysis.CStarAlgebra.Extreme` `Mathlib.Analysis.CStarAlgebra.Fuglede` `Mathlib.Analysis.CStarAlgebra.GelfandDuality` `Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal` `Mathlib.Analysis.CStarAlgebra.Hom` `Mathlib.Analysis.CStarAlgebra.Matrix` `Mathlib.Analysis.CStarAlgebra.Module.Constructions` `Mathlib.Analysis.CStarAlgebra.Module.Defs` `Mathlib.Analysis.CStarAlgebra.Module.Synonym` `Mathlib.Analysis.CStarAlgebra.Multiplier` `Mathlib.Analysis.CStarAlgebra.PositiveLinearFunctional` `Mathlib.Analysis.CStarAlgebra.PositiveLinearMap` `Mathlib.Analysis.CStarAlgebra.Projection` `Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart` `Mathlib.Analysis.CStarAlgebra.Spectrum` `Mathlib.Analysis.CStarAlgebra.Unitary.Connected` `Mathlib.Analysis.CStarAlgebra.Unitary.Maps` `Mathlib.Analysis.CStarAlgebra.Unitary.Span` `Mathlib.Analysis.CStarAlgebra.Unitization` `Mathlib.Analysis.CStarAlgebra.lpSpace` `Mathlib.Analysis.Calculus.AbsolutelyMonotone` `Mathlib.Analysis.Calculus.AddTorsor.AffineMap` `Mathlib.Analysis.Calculus.AddTorsor.Coord` `Mathlib.Analysis.Calculus.BumpFunction.Basic` `Mathlib.Analysis.Calculus.BumpFunction.Convolution` `Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension` `Mathlib.Analysis.Calculus.BumpFunction.InnerProduct` `Mathlib.Analysis.Calculus.BumpFunction.Normed` `Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox` `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.Convolution` `Mathlib.Analysis.Calculus.ContDiff.Defs` `Mathlib.Analysis.Calculus.ContDiff.Deriv` `Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries` `Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno` `Mathlib.Analysis.Calculus.ContDiff.FiniteDimension` `Mathlib.Analysis.Calculus.ContDiff.Operations` `Mathlib.Analysis.Calculus.ContDiff.Polynomial` `Mathlib.Analysis.Calculus.ContDiff.RCLike` `Mathlib.Analysis.Calculus.ContDiff.RestrictScalars` `Mathlib.Analysis.Calculus.ContDiff.WithLp` `Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise` `Mathlib.Analysis.Calculus.DSlope` `Mathlib.Analysis.Calculus.Darboux` `Mathlib.Analysis.Calculus.Deriv.Abs` `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.DifferentialForm.Basic` `Mathlib.Analysis.Calculus.DifferentialForm.VectorField` `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.Measurable` `Mathlib.Analysis.Calculus.FDeriv.Mul` `Mathlib.Analysis.Calculus.FDeriv.Norm` `Mathlib.Analysis.Calculus.FDeriv.OfCompLeft` `Mathlib.Analysis.Calculus.FDeriv.Partial` `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.FDeriv.WithLp` `Mathlib.Analysis.Calculus.FormalMultilinearSeries` `Mathlib.Analysis.Calculus.Gradient.Basic` `Mathlib.Analysis.Calculus.ImplicitContDiff` `Mathlib.Analysis.Calculus.ImplicitFunction.Bivariate` `Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain` `Mathlib.Analysis.Calculus.Implicit` `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.InverseFunctionTheorem.FiniteDimensional` `Mathlib.Analysis.Calculus.IteratedDeriv.Analytic` `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.LineDeriv.IntegrationByParts` `Mathlib.Analysis.Calculus.LineDeriv.Measurable` `Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap` `Mathlib.Analysis.Calculus.LocalExtr.Basic` `Mathlib.Analysis.Calculus.LocalExtr.LineDeriv` `Mathlib.Analysis.Calculus.LocalExtr.Polynomial` `Mathlib.Analysis.Calculus.LocalExtr.Rolle` `Mathlib.Analysis.Calculus.LogDerivUniformlyOn` `Mathlib.Analysis.Calculus.LogDeriv` `Mathlib.Analysis.Calculus.MeanValue` `Mathlib.Analysis.Calculus.Monotone` `Mathlib.Analysis.Calculus.ParametricIntegral` `Mathlib.Analysis.Calculus.ParametricIntervalIntegral` `Mathlib.Analysis.Calculus.Rademacher` `Mathlib.Analysis.Calculus.SmoothSeries` `Mathlib.Analysis.Calculus.TangentCone.DimOne` `Mathlib.Analysis.Calculus.TangentCone.Pi` `Mathlib.Analysis.Calculus.TangentCone.ProperSpace` `Mathlib.Analysis.Calculus.TangentCone.Real` `Mathlib.Analysis.Calculus.TangentCone.Seq` `Mathlib.Analysis.Calculus.TaylorIntegral` `Mathlib.Analysis.Calculus.Taylor` `Mathlib.Analysis.Calculus.UniformLimitsDeriv` `Mathlib.Analysis.Calculus.VectorField` `Mathlib.Analysis.Complex.AbelLimit` `Mathlib.Analysis.Complex.AbsMax` `Mathlib.Analysis.Complex.Angle` `Mathlib.Analysis.Complex.Arg` `Mathlib.Analysis.Complex.Asymptotics` `Mathlib.Analysis.Complex.Basic` `Mathlib.Analysis.Complex.BorelCaratheodory` `Mathlib.Analysis.Complex.BranchLogRoot` `Mathlib.Analysis.Complex.CanonicalDecomposition` `Mathlib.Analysis.Complex.Cardinality` `Mathlib.Analysis.Complex.CauchyIntegral` `Mathlib.Analysis.Complex.Circle` `Mathlib.Analysis.Complex.Conformal` `Mathlib.Analysis.Complex.Convex` `Mathlib.Analysis.Complex.CoveringMap` `Mathlib.Analysis.Complex.ExponentialBounds` `Mathlib.Analysis.Complex.Exponential` `Mathlib.Analysis.Complex.Hadamard` `Mathlib.Analysis.Complex.HalfPlane` `Mathlib.Analysis.Complex.Harmonic.Analytic` `Mathlib.Analysis.Complex.Harmonic.Liouville` `Mathlib.Analysis.Complex.Harmonic.MeanValue` `Mathlib.Analysis.Complex.Harmonic.Poisson` `Mathlib.Analysis.Complex.HasPrimitives` `Mathlib.Analysis.Complex.IntegerCompl` `Mathlib.Analysis.Complex.Isometry` `Mathlib.Analysis.Complex.JensenFormula` `Mathlib.Analysis.Complex.Liouville` `Mathlib.Analysis.Complex.LocallyUniformLimit` `Mathlib.Analysis.Complex.MeanValue` `Mathlib.Analysis.Complex.Norm` `Mathlib.Analysis.Complex.OpenMapping` `Mathlib.Analysis.Complex.OperatorNorm` `Mathlib.Analysis.Complex.Order` `Mathlib.Analysis.Complex.Periodic` `Mathlib.Analysis.Complex.PhragmenLindelof` `Mathlib.Analysis.Complex.Poisson` `Mathlib.Analysis.Complex.Polynomial.Basic` `Mathlib.Analysis.Complex.Polynomial.GaussLucas` `Mathlib.Analysis.Complex.Polynomial.UnitTrinomial` `Mathlib.Analysis.Complex.Positivity` `Mathlib.Analysis.Complex.ReImTopology` `Mathlib.Analysis.Complex.RealDeriv` `Mathlib.Analysis.Complex.RemovableSingularity` `Mathlib.Analysis.Complex.RiemannMapping` `Mathlib.Analysis.Complex.Schwarz` `Mathlib.Analysis.Complex.Spectrum` `Mathlib.Analysis.Complex.SqrtDeriv` `Mathlib.Analysis.Complex.SummableUniformlyOn` `Mathlib.Analysis.Complex.TaylorSeries` `Mathlib.Analysis.Complex.Tietze` `Mathlib.Analysis.Complex.Trigonometric` `Mathlib.Analysis.Complex.UnitDisc.Basic` `Mathlib.Analysis.Complex.UpperHalfPlane.Basic` `Mathlib.Analysis.Complex.UpperHalfPlane.Exp` `Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints` `Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty` `Mathlib.Analysis.Complex.UpperHalfPlane.Manifold` `Mathlib.Analysis.Complex.UpperHalfPlane.Measure` `Mathlib.Analysis.Complex.UpperHalfPlane.Metric` `Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction` `Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction` `Mathlib.Analysis.Complex.UpperHalfPlane.Topology` `Mathlib.Analysis.Complex.ValueDistribution.Cartan` `Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction` `Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem` `Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic` `Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic` `Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic` `Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation` `Mathlib.Analysis.Complex.ValueDistribution.SecondMainTheorem` `Mathlib.Analysis.ConstantSpeed` `Mathlib.Analysis.Convex.AmpleSet` `Mathlib.Analysis.Convex.Approximation` `Mathlib.Analysis.Convex.Birkhoff` `Mathlib.Analysis.Convex.Body` `Mathlib.Analysis.Convex.Cone.Basic` `Mathlib.Analysis.Convex.Cone.Dual` `Mathlib.Analysis.Convex.Cone.InnerDual` `Mathlib.Analysis.Convex.Cone.TensorProduct` `Mathlib.Analysis.Convex.ContinuousLinearEquiv` `Mathlib.Analysis.Convex.Continuous` `Mathlib.Analysis.Convex.Deriv` `Mathlib.Analysis.Convex.DoublyStochasticMatrix` `Mathlib.Analysis.Convex.EGauge` `Mathlib.Analysis.Convex.Exposed` `Mathlib.Analysis.Convex.Extrema` `Mathlib.Analysis.Convex.GaugeRescale` `Mathlib.Analysis.Convex.Gauge` `Mathlib.Analysis.Convex.Integral` `Mathlib.Analysis.Convex.Intrinsic` `Mathlib.Analysis.Convex.KreinMilman` `Mathlib.Analysis.Convex.LinearIsometry` `Mathlib.Analysis.Convex.Measure` `Mathlib.Analysis.Convex.MetricSpace` `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.Strict.Extreme` `Mathlib.Analysis.Convex.StrictCombination` `Mathlib.Analysis.Convex.StrictConvexBetween` `Mathlib.Analysis.Convex.StrictConvexSpace` `Mathlib.Analysis.Convex.Strict` `Mathlib.Analysis.Convex.Strong` `Mathlib.Analysis.Convex.Topology` `Mathlib.Analysis.Convex.TotallyBounded` `Mathlib.Analysis.Convex.Uniform` `Mathlib.Analysis.Convex.Visible` `Mathlib.Analysis.Convolution` `Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff` `Mathlib.Analysis.Distribution.ContDiffMapSupportedIn` `Mathlib.Analysis.Distribution.DerivNotation` `Mathlib.Analysis.Distribution.Distribution` `Mathlib.Analysis.Distribution.FourierMultiplier` `Mathlib.Analysis.Distribution.SchwartzSpace.Basic` `Mathlib.Analysis.Distribution.SchwartzSpace.Deriv` `Mathlib.Analysis.Distribution.SchwartzSpace.Fourier` `Mathlib.Analysis.Distribution.Sobolev` `Mathlib.Analysis.Distribution.Support` `Mathlib.Analysis.Distribution.TemperateGrowth` `Mathlib.Analysis.Distribution.TemperedDistribution` `Mathlib.Analysis.Distribution.TestFunction` `Mathlib.Analysis.Fourier.AddCircleMulti` `Mathlib.Analysis.Fourier.AddCircle` `Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar` `Mathlib.Analysis.Fourier.Convolution` `Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality` `Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality` `Mathlib.Analysis.Fourier.FourierTransformDeriv` `Mathlib.Analysis.Fourier.FourierTransform` `Mathlib.Analysis.Fourier.Inversion` `Mathlib.Analysis.Fourier.LpSpace` `Mathlib.Analysis.Fourier.Notation` `Mathlib.Analysis.Fourier.PoissonSummation` `Mathlib.Analysis.Fourier.RiemannLebesgueLemma` `Mathlib.Analysis.Fourier.ZMod` `Mathlib.Analysis.FunctionalSpaces.BesselPotentialSpace` `Mathlib.Analysis.FunctionalSpaces.SobolevInequality` `Mathlib.Analysis.Hofer` `Mathlib.Analysis.InnerProductSpace.Adjoint` `Mathlib.Analysis.InnerProductSpace.Affine` `Mathlib.Analysis.InnerProductSpace.Basic` `Mathlib.Analysis.InnerProductSpace.Calculus` `Mathlib.Analysis.InnerProductSpace.CanonicalTensor` `Mathlib.Analysis.InnerProductSpace.Coalgebra` `Mathlib.Analysis.InnerProductSpace.Completion` `Mathlib.Analysis.InnerProductSpace.ConformalLinearMap` `Mathlib.Analysis.InnerProductSpace.Continuous` `Mathlib.Analysis.InnerProductSpace.Convex` `Mathlib.Analysis.InnerProductSpace.Defs` `Mathlib.Analysis.InnerProductSpace.Dual` `Mathlib.Analysis.InnerProductSpace.EuclideanDist` `Mathlib.Analysis.InnerProductSpace.ExteriorPower` `Mathlib.Analysis.InnerProductSpace.GramMatrix` `Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho` `Mathlib.Analysis.InnerProductSpace.Harmonic.Basic` `Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions` `Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl` `Mathlib.Analysis.InnerProductSpace.JointEigenspace` `Mathlib.Analysis.InnerProductSpace.Laplacian` `Mathlib.Analysis.InnerProductSpace.LaxMilgram` `Mathlib.Analysis.InnerProductSpace.LinearMap` `Mathlib.Analysis.InnerProductSpace.LinearPMap` `Mathlib.Analysis.InnerProductSpace.MeanErgodic` `Mathlib.Analysis.InnerProductSpace.MulOpposite` `Mathlib.Analysis.InnerProductSpace.NormDet` `Mathlib.Analysis.InnerProductSpace.NormPow` `Mathlib.Analysis.InnerProductSpace.OfNorm` `Mathlib.Analysis.InnerProductSpace.Orientation` `Mathlib.Analysis.InnerProductSpace.Orthogonal` `Mathlib.Analysis.InnerProductSpace.Orthonormal` `Mathlib.Analysis.InnerProductSpace.PiL2` `Mathlib.Analysis.InnerProductSpace.Positive` `Mathlib.Analysis.InnerProductSpace.ProdL2` `Mathlib.Analysis.InnerProductSpace.Projection.Basic` `Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional` `Mathlib.Analysis.InnerProductSpace.Projection.Minimal` `Mathlib.Analysis.InnerProductSpace.Projection.Reflection` `Mathlib.Analysis.InnerProductSpace.Projection.Submodule` `Mathlib.Analysis.InnerProductSpace.Rayleigh` `Mathlib.Analysis.InnerProductSpace.Reproducing.Operations` `Mathlib.Analysis.InnerProductSpace.Reproducing` `Mathlib.Analysis.InnerProductSpace.Semisimple` `Mathlib.Analysis.InnerProductSpace.SingularValues` `Mathlib.Analysis.InnerProductSpace.Spectrum` `Mathlib.Analysis.InnerProductSpace.StandardSubspace` `Mathlib.Analysis.InnerProductSpace.StarOrder` `Mathlib.Analysis.InnerProductSpace.Subspace` `Mathlib.Analysis.InnerProductSpace.Symmetric` `Mathlib.Analysis.InnerProductSpace.TensorProduct` `Mathlib.Analysis.InnerProductSpace.Trace` `Mathlib.Analysis.InnerProductSpace.TwoDim` `Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology` `Mathlib.Analysis.InnerProductSpace.l2Space` `Mathlib.Analysis.LConvolution` `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.HahnBanach` `Mathlib.Analysis.LocallyConvex.Montel` `Mathlib.Analysis.LocallyConvex.PointwiseConvergence` `Mathlib.Analysis.LocallyConvex.Polar` `Mathlib.Analysis.LocallyConvex.SeparatingDual` `Mathlib.Analysis.LocallyConvex.Separation` `Mathlib.Analysis.LocallyConvex.StrongTopology` `Mathlib.Analysis.LocallyConvex.WeakDual` `Mathlib.Analysis.LocallyConvex.WeakOperatorTopology` `Mathlib.Analysis.LocallyConvex.WeakSpace` `Mathlib.Analysis.LocallyConvex.WithSeminorms` `Mathlib.Analysis.Matrix.HermitianFunctionalCalculus` `Mathlib.Analysis.Matrix.Hermitian` `Mathlib.Analysis.Matrix.LDL` `Mathlib.Analysis.Matrix.MeasurableSpace` `Mathlib.Analysis.Matrix.Normed` `Mathlib.Analysis.Matrix.Order` `Mathlib.Analysis.Matrix.PosDef` `Mathlib.Analysis.Matrix.Spectrum` `Mathlib.Analysis.MeanInequalitiesPow` `Mathlib.Analysis.MeanInequalities` `Mathlib.Analysis.MellinInversion` `Mathlib.Analysis.MellinTransform` `Mathlib.Analysis.Meromorphic.Basic` `Mathlib.Analysis.Meromorphic.Complex` `Mathlib.Analysis.Meromorphic.Divisor` `Mathlib.Analysis.Meromorphic.FactorizedRational` `Mathlib.Analysis.Meromorphic.IsolatedZeros` `Mathlib.Analysis.Meromorphic.LogDeriv` `Mathlib.Analysis.Meromorphic.NormalForm` `Mathlib.Analysis.Meromorphic.Order` `Mathlib.Analysis.Meromorphic.RCLike` `Mathlib.Analysis.Meromorphic.TrailingCoefficient` `Mathlib.Analysis.Normed.Affine.AddTorsorBases` `Mathlib.Analysis.Normed.Affine.AddTorsor` `Mathlib.Analysis.Normed.Affine.AsymptoticCone` `Mathlib.Analysis.Normed.Affine.Ceva` `Mathlib.Analysis.Normed.Affine.ContinuousAffineMap` `Mathlib.Analysis.Normed.Affine.Convex` `Mathlib.Analysis.Normed.Affine.Isometry` `Mathlib.Analysis.Normed.Affine.MazurUlam` `Mathlib.Analysis.Normed.Affine.Simplex` `Mathlib.Analysis.Normed.Algebra.Basic` `Mathlib.Analysis.Normed.Algebra.DualNumber` `Mathlib.Analysis.Normed.Algebra.Exponential` `Mathlib.Analysis.Normed.Algebra.GelfandFormula` `Mathlib.Analysis.Normed.Algebra.GelfandMazur` `Mathlib.Analysis.Normed.Algebra.MatrixExponential` `Mathlib.Analysis.Normed.Algebra.QuaternionExponential` `Mathlib.Analysis.Normed.Algebra.Spectrum` `Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt` `Mathlib.Analysis.Normed.Algebra.Ultra` `Mathlib.Analysis.Normed.Algebra.UnitizationL1` `Mathlib.Analysis.Normed.Algebra.Unitization` `Mathlib.Analysis.Normed.Field.Approximation` `Mathlib.Analysis.Normed.Field.Basic` `Mathlib.Analysis.Normed.Field.Dense` `Mathlib.Analysis.Normed.Field.Instances` `Mathlib.Analysis.Normed.Field.Krasner` `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.Field.WithAbs` `Mathlib.Analysis.Normed.Group.AddCircle` `Mathlib.Analysis.Normed.Group.AddTorsor` `Mathlib.Analysis.Normed.Group.BallSphere` `Mathlib.Analysis.Normed.Group.Bounded` `Mathlib.Analysis.Normed.Group.Completeness` `Mathlib.Analysis.Normed.Group.Completion` `Mathlib.Analysis.Normed.Group.Continuity` `Mathlib.Analysis.Normed.Group.ControlledClosure` `Mathlib.Analysis.Normed.Group.FunctionSeries` `Mathlib.Analysis.Normed.Group.HomCompletion` `Mathlib.Analysis.Normed.Group.Hom` `Mathlib.Analysis.Normed.Group.InfiniteSum` `Mathlib.Analysis.Normed.Group.Lemmas` `Mathlib.Analysis.Normed.Group.NullSubmodule` `Mathlib.Analysis.Normed.Group.Pointwise` `Mathlib.Analysis.Normed.Group.Quotient` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels` `Mathlib.Analysis.Normed.Group.SemiNormedGrp` `Mathlib.Analysis.Normed.Group.SeparationQuotient` `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.Finsupp` `Mathlib.Analysis.Normed.Lp.LpEquiv` `Mathlib.Analysis.Normed.Lp.Matrix` `Mathlib.Analysis.Normed.Lp.MeasurableSpace` `Mathlib.Analysis.Normed.Lp.PiLp` `Mathlib.Analysis.Normed.Lp.ProdLp` `Mathlib.Analysis.Normed.Lp.SmoothApprox` `Mathlib.Analysis.Normed.Lp.lpHolder` `Mathlib.Analysis.Normed.Lp.lpSpace` `Mathlib.Analysis.Normed.Module.Alternating.Basic` `Mathlib.Analysis.Normed.Module.Alternating.Curry` `Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin` `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.Bases` `Mathlib.Analysis.Normed.Module.Basic` `Mathlib.Analysis.Normed.Module.Complemented` `Mathlib.Analysis.Normed.Module.Completion` `Mathlib.Analysis.Normed.Module.Connected` `Mathlib.Analysis.Normed.Module.ContinuousInverse` `Mathlib.Analysis.Normed.Module.Convex` `Mathlib.Analysis.Normed.Module.DoubleDual` `Mathlib.Analysis.Normed.Module.Dual` `Mathlib.Analysis.Normed.Module.Extr` `Mathlib.Analysis.Normed.Module.FiniteDimension` `Mathlib.Analysis.Normed.Module.HahnBanach` `Mathlib.Analysis.Normed.Module.Multilinear.Basic` `Mathlib.Analysis.Normed.Module.Multilinear.Curry` `Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn` `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.Seminorm.Basic` `Mathlib.Analysis.Normed.Module.Seminorm.Norm` `Mathlib.Analysis.Normed.Module.Shrink` `Mathlib.Analysis.Normed.Module.Span` `Mathlib.Analysis.Normed.Module.TransferInstance` `Mathlib.Analysis.Normed.Module.WeakDual` `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.Basic` `Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension` `Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative` `Mathlib.Analysis.Normed.Operator.Compact` `Mathlib.Analysis.Normed.Operator.CompleteCodomain` `Mathlib.Analysis.Normed.Operator.Completeness` `Mathlib.Analysis.Normed.Operator.Conformal` `Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv` `Mathlib.Analysis.Normed.Operator.ContinuousLinearMap` `Mathlib.Analysis.Normed.Operator.Extend` `Mathlib.Analysis.Normed.Operator.Fredholm.Basic` `Mathlib.Analysis.Normed.Operator.Fredholm.Open` `Mathlib.Analysis.Normed.Operator.FredholmAlternative` `Mathlib.Analysis.Normed.Operator.LinearIsometry` `Mathlib.Analysis.Normed.Operator.Mul` `Mathlib.Analysis.Normed.Operator.NNNorm` `Mathlib.Analysis.Normed.Operator.NormedSpace` `Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite` `Mathlib.Analysis.Normed.Operator.Prod` `Mathlib.Analysis.Normed.Order.Lattice` `Mathlib.Analysis.Normed.Order.UpperLower` `Mathlib.Analysis.Normed.Ring.Basic` `Mathlib.Analysis.Normed.Ring.Finite` `Mathlib.Analysis.Normed.Ring.InfiniteProd` `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.Normed.Unbundled.SpectralNorm` `Mathlib.Analysis.NormedSpace.FunctionSeries` `Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness` `Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm` `Mathlib.Analysis.NormedSpace.OperatorNorm.Prod` `Mathlib.Analysis.NormedSpace.RCLike` `Mathlib.Analysis.NormedSpace.Real` `Mathlib.Analysis.ODE.Basic` `Mathlib.Analysis.ODE.DiscreteGronwall` `Mathlib.Analysis.ODE.ExistUnique` `Mathlib.Analysis.ODE.Gronwall` `Mathlib.Analysis.ODE.PicardLindelof` `Mathlib.Analysis.ODE.Transform` `Mathlib.Analysis.PSeriesComplex` `Mathlib.Analysis.PSeries` `Mathlib.Analysis.Polynomial.Basic` `Mathlib.Analysis.Polynomial.CauchyBound` `Mathlib.Analysis.Polynomial.Factorization` `Mathlib.Analysis.Polynomial.Fourier` `Mathlib.Analysis.Polynomial.MahlerMeasure` `Mathlib.Analysis.Polynomial.Norm` `Mathlib.Analysis.Polynomial.Order` `Mathlib.Analysis.Quaternion` `Mathlib.Analysis.RCLike.Basic` `Mathlib.Analysis.RCLike.BoundedContinuous` `Mathlib.Analysis.RCLike.ContinuousMap` `Mathlib.Analysis.RCLike.Extend` `Mathlib.Analysis.RCLike.Inner` `Mathlib.Analysis.RCLike.Lemmas` `Mathlib.Analysis.RCLike.Sqrt` `Mathlib.Analysis.RCLike.TangentCone` `Mathlib.Analysis.Rat.NatSqrt.Real` `Mathlib.Analysis.Real.Cardinality` `Mathlib.Analysis.Real.Hyperreal` `Mathlib.Analysis.Real.OfDigits` `Mathlib.Analysis.Real.Pi.Bounds` `Mathlib.Analysis.Real.Pi.Chudnovsky` `Mathlib.Analysis.Real.Pi.Irrational` `Mathlib.Analysis.Real.Pi.Leibniz` `Mathlib.Analysis.Real.Pi.Wallis` `Mathlib.Analysis.Real.Spectrum` `Mathlib.Analysis.Real.Sqrt` `Mathlib.Analysis.Seminorm` `Mathlib.Analysis.SpecialFunctions.Arcosh` `Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean` `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.Analytic` `Mathlib.Analysis.SpecialFunctions.Complex.Arctan` `Mathlib.Analysis.SpecialFunctions.Complex.Arg` `Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar` `Mathlib.Analysis.SpecialFunctions.Complex.CircleMap` `Mathlib.Analysis.SpecialFunctions.Complex.Circle` `Mathlib.Analysis.SpecialFunctions.Complex.LogBounds` `Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv` `Mathlib.Analysis.SpecialFunctions.Complex.Log` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Isometric` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Measurable` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder` `Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass` `Mathlib.Analysis.SpecialFunctions.ExpDeriv` `Mathlib.Analysis.SpecialFunctions.Exp` `Mathlib.Analysis.SpecialFunctions.Exponential` `Mathlib.Analysis.SpecialFunctions.FrullaniIntegral` `Mathlib.Analysis.SpecialFunctions.Gamma.Basic` `Mathlib.Analysis.SpecialFunctions.Gamma.Beta` `Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup` `Mathlib.Analysis.SpecialFunctions.Gamma.Deligne` `Mathlib.Analysis.SpecialFunctions.Gamma.Deriv` `Mathlib.Analysis.SpecialFunctions.Gamma.Digamma` `Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform` `Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral` `Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation` `Mathlib.Analysis.SpecialFunctions.ImproperIntegrals` `Mathlib.Analysis.SpecialFunctions.Integrability.Basic` `Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic` `Mathlib.Analysis.SpecialFunctions.Integrals.Basic` `Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric` `Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage` `Mathlib.Analysis.SpecialFunctions.JapaneseBracket` `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.Log.Summable` `Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral` `Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq` `Mathlib.Analysis.SpecialFunctions.NonIntegrable` `Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric` `Mathlib.Analysis.SpecialFunctions.Pochhammer` `Mathlib.Analysis.SpecialFunctions.PolarCoord` `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.Integral` `Mathlib.Analysis.SpecialFunctions.Pow.NNReal` `Mathlib.Analysis.SpecialFunctions.Pow.Real` `Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric` `Mathlib.Analysis.SpecialFunctions.Sigmoid` `Mathlib.Analysis.SpecialFunctions.SmoothTransition` `Mathlib.Analysis.SpecialFunctions.Sqrt` `Mathlib.Analysis.SpecialFunctions.Stirling` `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.ChebyshevGauss` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema` `Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent` `Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd` `Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Series` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc` `Mathlib.Analysis.SpecificLimits.ArithmeticGeometric` `Mathlib.Analysis.SpecificLimits.Basic` `Mathlib.Analysis.SpecificLimits.Fibonacci` `Mathlib.Analysis.SpecificLimits.FloorPow` `Mathlib.Analysis.SpecificLimits.Normed` `Mathlib.Analysis.SpecificLimits.RCLike` `Mathlib.Analysis.SumIntegralComparisons` `Mathlib.Analysis.SumIntegralExpDecay` `Mathlib.Analysis.SumOverResidueClass` `Mathlib.Analysis.VonNeumannAlgebra.Basic` `Mathlib.CategoryTheory.Galois.ContAction` `Mathlib.CategoryTheory.Galois.Equivalence` `Mathlib.CategoryTheory.Galois.EssSurj` `Mathlib.CategoryTheory.Galois.IsFundamentalgroup` `Mathlib.Combinatorics.Additive.AP.Three.Behrend` `Mathlib.Combinatorics.Additive.Corner.Roth` `Mathlib.Combinatorics.Additive.Randomisation` `Mathlib.Combinatorics.Additive.VerySmallDoubling` `Mathlib.Combinatorics.Derangements.Exponential` `Mathlib.Combinatorics.Enumerative.Partition.GenFun` `Mathlib.Combinatorics.Enumerative.Partition.Glaisher` `Mathlib.Combinatorics.Enumerative.Pentagonal.EulerFunction` `Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries` `Mathlib.Combinatorics.Enumerative.Pentagonal.Ring` `Mathlib.Combinatorics.Extremal.RuzsaSzemeredi` `Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits` `Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity` `Mathlib.Combinatorics.SimpleGraph.LapMatrix` `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.Sequence` `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.Rat.NatSqrt.Real` `Mathlib.Data.Real.CompleteField` `Mathlib.Data.Real.Hom` `Mathlib.Data.Real.Sqrt` `Mathlib.Data.Real.StarOrdered` `Mathlib.Dynamics.BirkhoffSum.NormedSpace` `Mathlib.Dynamics.BirkhoffSum.QuasiMeasurePreserving` `Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber` `Mathlib.Dynamics.Ergodic.Action.Basic` `Mathlib.Dynamics.Ergodic.Action.OfMinimal` `Mathlib.Dynamics.Ergodic.Action.Regular` `Mathlib.Dynamics.Ergodic.AddCircleAdd` `Mathlib.Dynamics.Ergodic.AddCircle` `Mathlib.Dynamics.Ergodic.Conservative` `Mathlib.Dynamics.Ergodic.Ergodic` `Mathlib.Dynamics.Ergodic.Extreme` `Mathlib.Dynamics.Ergodic.Function` `Mathlib.Dynamics.Ergodic.MeasurePreserving` `Mathlib.Dynamics.Ergodic.RadonNikodym` `Mathlib.Dynamics.TopologicalEntropy.CoverEntropy` `Mathlib.Dynamics.TopologicalEntropy.NetEntropy` `Mathlib.Dynamics.TopologicalEntropy.Semiconj` `Mathlib.Dynamics.TopologicalEntropy.Subset` `Mathlib.FieldTheory.AbsoluteGaloisGroup` `Mathlib.FieldTheory.Galois.Abelian` `Mathlib.FieldTheory.Galois.Infinite` `Mathlib.FieldTheory.Galois.IsGaloisGroup` `Mathlib.FieldTheory.Galois.Profinite` `Mathlib.FieldTheory.KrullTopology` `Mathlib.FieldTheory.Laurent` `Mathlib.FieldTheory.RatFunc.AsPolynomial` `Mathlib.FieldTheory.RatFunc.Degree` `Mathlib.FieldTheory.RatFunc.IntermediateField` `Mathlib.FieldTheory.RatFunc.Luroth` `Mathlib.FieldTheory.RatFunc.Valuation` `Mathlib.Geometry.Diffeology.Basic` `Mathlib.Geometry.Euclidean.Altitude` `Mathlib.Geometry.Euclidean.Angle.Bisector` `Mathlib.Geometry.Euclidean.Angle.Incenter` `Mathlib.Geometry.Euclidean.Angle.Oriented.Affine` `Mathlib.Geometry.Euclidean.Angle.Oriented.Basic` `Mathlib.Geometry.Euclidean.Angle.Oriented.Projection` `Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle` `Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation` `Mathlib.Geometry.Euclidean.Angle.Sphere` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal` `Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection` `Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle` `Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality` `Mathlib.Geometry.Euclidean.Basic` `Mathlib.Geometry.Euclidean.BritishFlag` `Mathlib.Geometry.Euclidean.Circumcenter` `Mathlib.Geometry.Euclidean.Congruence` `Mathlib.Geometry.Euclidean.Incenter` `Mathlib.Geometry.Euclidean.Inversion.Basic` `Mathlib.Geometry.Euclidean.Inversion.Calculus` `Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane` `Mathlib.Geometry.Euclidean.MongePoint` `Mathlib.Geometry.Euclidean.NinePointCircle` `Mathlib.Geometry.Euclidean.PerpBisector` `Mathlib.Geometry.Euclidean.Projection` `Mathlib.Geometry.Euclidean.SignedDist` `Mathlib.Geometry.Euclidean.Similarity` `Mathlib.Geometry.Euclidean.Simplex` `Mathlib.Geometry.Euclidean.Sphere.Basic` `Mathlib.Geometry.Euclidean.Sphere.OrthRadius` `Mathlib.Geometry.Euclidean.Sphere.PolePolar` `Mathlib.Geometry.Euclidean.Sphere.Power` `Mathlib.Geometry.Euclidean.Sphere.Ptolemy` `Mathlib.Geometry.Euclidean.Sphere.SecondInter` `Mathlib.Geometry.Euclidean.Sphere.Tangent` `Mathlib.Geometry.Euclidean.Triangle` `Mathlib.Geometry.Euclidean.Volume.Measure` `Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation` `Mathlib.Geometry.Manifold.Algebra.LieGroup` `Mathlib.Geometry.Manifold.Algebra.Monoid` `Mathlib.Geometry.Manifold.Algebra.SMul` `Mathlib.Geometry.Manifold.Algebra.SmoothFunctions` `Mathlib.Geometry.Manifold.Algebra.Structures` `Mathlib.Geometry.Manifold.Bordism` `Mathlib.Geometry.Manifold.BumpFunction` `Mathlib.Geometry.Manifold.Category.MfldCat.OfModel` `Mathlib.Geometry.Manifold.Complex` `Mathlib.Geometry.Manifold.ConformalGroupoid` `Mathlib.Geometry.Manifold.ContMDiff.Atlas` `Mathlib.Geometry.Manifold.ContMDiff.Basic` `Mathlib.Geometry.Manifold.ContMDiff.Constructions` `Mathlib.Geometry.Manifold.ContMDiff.Defs` `Mathlib.Geometry.Manifold.ContMDiff.NormedSpace` `Mathlib.Geometry.Manifold.ContMDiffMFDeriv` `Mathlib.Geometry.Manifold.ContMDiffMap` `Mathlib.Geometry.Manifold.DerivationBundle` `Mathlib.Geometry.Manifold.Diffeomorph` `Mathlib.Geometry.Manifold.GroupLieAlgebra` `Mathlib.Geometry.Manifold.ImmersionDiff` `Mathlib.Geometry.Manifold.Immersion` `Mathlib.Geometry.Manifold.Instances.Icc` `Mathlib.Geometry.Manifold.Instances.Quotient` `Mathlib.Geometry.Manifold.Instances.Real` `Mathlib.Geometry.Manifold.Instances.Sphere` `Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra` `Mathlib.Geometry.Manifold.IntegralCurve.Basic` `Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique` `Mathlib.Geometry.Manifold.IntegralCurve.Transform` `Mathlib.Geometry.Manifold.IntegralCurve.UniformTime` `Mathlib.Geometry.Manifold.IsManifold.Basic` `Mathlib.Geometry.Manifold.IsManifold.ExtChartAt` `Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary` `Mathlib.Geometry.Manifold.LocalDiffeomorph` `Mathlib.Geometry.Manifold.LocalSourceTargetProperty` `Mathlib.Geometry.Manifold.MFDeriv.Atlas` `Mathlib.Geometry.Manifold.MFDeriv.Basic` `Mathlib.Geometry.Manifold.MFDeriv.Defs` `Mathlib.Geometry.Manifold.MFDeriv.FDeriv` `Mathlib.Geometry.Manifold.MFDeriv.NormedSpace` `Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions` `Mathlib.Geometry.Manifold.MFDeriv.Tangent` `Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential` `Mathlib.Geometry.Manifold.Metrizable` `Mathlib.Geometry.Manifold.Notation` `Mathlib.Geometry.Manifold.PartitionOfUnity` `Mathlib.Geometry.Manifold.PoincareConjecture` `Mathlib.Geometry.Manifold.Riemannian.Basic` `Mathlib.Geometry.Manifold.Riemannian.PathELength` `Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace` `Mathlib.Geometry.Manifold.Sheaf.Smooth` `Mathlib.Geometry.Manifold.SmoothApprox` `Mathlib.Geometry.Manifold.SmoothEmbedding` `Mathlib.Geometry.Manifold.Submersion` `Mathlib.Geometry.Manifold.VectorBundle.Basic` `Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection` `Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic` `Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.LeviCivita` `Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric` `Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion` `Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear` `Mathlib.Geometry.Manifold.VectorBundle.Hom` `Mathlib.Geometry.Manifold.VectorBundle.LocalFrame` `Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable` `Mathlib.Geometry.Manifold.VectorBundle.Pullback` `Mathlib.Geometry.Manifold.VectorBundle.Riemannian` `Mathlib.Geometry.Manifold.VectorBundle.SmoothSection` `Mathlib.Geometry.Manifold.VectorBundle.Tangent` `Mathlib.Geometry.Manifold.VectorBundle.Tensoriality` `Mathlib.Geometry.Manifold.VectorField.LieBracket` `Mathlib.Geometry.Manifold.VectorField.Pullback` `Mathlib.Geometry.Manifold.WhitneyEmbedding` `Mathlib.InformationTheory.Coding.KraftMcMillan` `Mathlib.InformationTheory.Coding.Kraft` `Mathlib.InformationTheory.KullbackLeibler.Basic` `Mathlib.InformationTheory.KullbackLeibler.ChainRule` `Mathlib.InformationTheory.KullbackLeibler.DataProcessing` `Mathlib.InformationTheory.KullbackLeibler.KLFun` `Mathlib.LinearAlgebra.Complex.FiniteDimensional` `Mathlib.LinearAlgebra.Eigenspace.ContinuousLinearMap` `Mathlib.LinearAlgebra.Matrix.Cartan.Realisation` `Mathlib.LinearAlgebra.Matrix.ElementaryRowOperations` `Mathlib.LinearAlgebra.Matrix.Gershgorin` `Mathlib.LinearAlgebra.Matrix.Permutation` `Mathlib.LinearAlgebra.Matrix.Stochastic` `Mathlib.LinearAlgebra.Matrix.Swap` `Mathlib.LinearAlgebra.QuadraticForm.Real` `Mathlib.LinearAlgebra.RootSystem.BaseChange` `Mathlib.LinearAlgebra.RootSystem.BaseExists` `Mathlib.LinearAlgebra.RootSystem.Base` `Mathlib.LinearAlgebra.RootSystem.Basic` `Mathlib.LinearAlgebra.RootSystem.CartanMatrix` `Mathlib.LinearAlgebra.RootSystem.Chain` `Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear` `Mathlib.LinearAlgebra.RootSystem.Finite.G2` `Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas` `Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations` `Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple` `Mathlib.LinearAlgebra.RootSystem.Hom` `Mathlib.LinearAlgebra.RootSystem.Irreducible` `Mathlib.LinearAlgebra.RootSystem.IsValuedIn` `Mathlib.LinearAlgebra.RootSystem.Reduced` `Mathlib.LinearAlgebra.RootSystem.RootPairingCat` `Mathlib.LinearAlgebra.RootSystem.RootPositive` `Mathlib.LinearAlgebra.RootSystem.WeylGroup` `Mathlib.MeasureTheory.Category.MeasCat` `Mathlib.MeasureTheory.Constructions.BorelSpace.Basic` `Mathlib.MeasureTheory.Constructions.BorelSpace.Complex` `Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap` `Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousMap` `Mathlib.MeasureTheory.Constructions.BorelSpace.Metric` `Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable` `Mathlib.MeasureTheory.Constructions.BorelSpace.Order` `Mathlib.MeasureTheory.Constructions.BorelSpace.Real` `Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop` `Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders` `Mathlib.MeasureTheory.Constructions.HaarToSphere` `Mathlib.MeasureTheory.Constructions.Pi` `Mathlib.MeasureTheory.Constructions.Polish.Basic` `Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal` `Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable` `Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent` `Mathlib.MeasureTheory.Constructions.Projective` `Mathlib.MeasureTheory.Constructions.UnitInterval` `Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace` `Mathlib.MeasureTheory.Covering.Besicovitch` `Mathlib.MeasureTheory.Covering.DensityTheorem` `Mathlib.MeasureTheory.Covering.Differentiation` `Mathlib.MeasureTheory.Covering.LiminfLimsup` `Mathlib.MeasureTheory.Covering.OneDim` `Mathlib.MeasureTheory.Covering.VitaliFamily` `Mathlib.MeasureTheory.Covering.Vitali` `Mathlib.MeasureTheory.Function.AEEqFun.DomAct` `Mathlib.MeasureTheory.Function.AEEqFun` `Mathlib.MeasureTheory.Function.AEEqOfIntegral` `Mathlib.MeasureTheory.Function.AEEqOfLIntegral` `Mathlib.MeasureTheory.Function.AEMeasurableOrder` `Mathlib.MeasureTheory.Function.AEMeasurableSequence` `Mathlib.MeasureTheory.Function.AbsolutelyContinuous` `Mathlib.MeasureTheory.Function.BorelGrowth` `Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic` `Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen` `Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1` `Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator` `Mathlib.MeasureTheory.Function.ConditionalExpectation.LebesgueBochner` `Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut` `Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Real` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique` `Mathlib.MeasureTheory.Function.ConditionalLExpectation` `Mathlib.MeasureTheory.Function.ContinuousMapDense` `Mathlib.MeasureTheory.Function.ConvergenceInDistribution` `Mathlib.MeasureTheory.Function.ConvergenceInMeasure` `Mathlib.MeasureTheory.Function.Egorov` `Mathlib.MeasureTheory.Function.EssSup` `Mathlib.MeasureTheory.Function.FactorsThrough` `Mathlib.MeasureTheory.Function.Floor` `Mathlib.MeasureTheory.Function.Holder` `Mathlib.MeasureTheory.Function.Intersectivity` `Mathlib.MeasureTheory.Function.JacobianOneDim` `Mathlib.MeasureTheory.Function.Jacobian` `Mathlib.MeasureTheory.Function.L1Space.AEEqFun` `Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral` `Mathlib.MeasureTheory.Function.L1Space.Integrable` `Mathlib.MeasureTheory.Function.L2Space` `Mathlib.MeasureTheory.Function.LocallyIntegrable` `Mathlib.MeasureTheory.Function.LpOrder` `Mathlib.MeasureTheory.Function.LpSeminorm.Basic` `Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov` `Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp` `Mathlib.MeasureTheory.Function.LpSeminorm.Count` `Mathlib.MeasureTheory.Function.LpSeminorm.Defs` `Mathlib.MeasureTheory.Function.LpSeminorm.Indicator` `Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm` `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.CompleteOfCompleteLp` `Mathlib.MeasureTheory.Function.LpSpace.Complete` `Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving` `Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions` `Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic` `Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous` `Mathlib.MeasureTheory.Function.LpSpace.Indicator` `Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum` `Mathlib.MeasureTheory.Function.Piecewise` `Mathlib.MeasureTheory.Function.SimpleFuncDenseLp` `Mathlib.MeasureTheory.Function.SimpleFuncDense` `Mathlib.MeasureTheory.Function.SimpleFunc` `Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan` `Mathlib.MeasureTheory.Function.SpecialFunctions.Basic` `Mathlib.MeasureTheory.Function.SpecialFunctions.Inner` `Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike` `Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc` `Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic` `Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp` `Mathlib.MeasureTheory.Function.UnifTight` `Mathlib.MeasureTheory.Function.UniformIntegrable` `Mathlib.MeasureTheory.Group.AEStabilizer` `Mathlib.MeasureTheory.Group.Action` `Mathlib.MeasureTheory.Group.AddCircle` `Mathlib.MeasureTheory.Group.Arithmetic` `Mathlib.MeasureTheory.Group.Circle` `Mathlib.MeasureTheory.Group.Convolution` `Mathlib.MeasureTheory.Group.Defs` `Mathlib.MeasureTheory.Group.FoelnerFilter` `Mathlib.MeasureTheory.Group.FundamentalDomain` `Mathlib.MeasureTheory.Group.GeometryOfNumbers` `Mathlib.MeasureTheory.Group.IntegralConvolution` `Mathlib.MeasureTheory.Group.Integral` `Mathlib.MeasureTheory.Group.LIntegral` `Mathlib.MeasureTheory.Group.MeasurableEquiv` `Mathlib.MeasureTheory.Group.Measure` `Mathlib.MeasureTheory.Group.ModularCharacter` `Mathlib.MeasureTheory.Group.Pointwise` `Mathlib.MeasureTheory.Group.Prod` `Mathlib.MeasureTheory.Integral.Asymptotics` `Mathlib.MeasureTheory.Integral.Average` `Mathlib.MeasureTheory.Integral.Bochner.Basic` `Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap` `Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus` `Mathlib.MeasureTheory.Integral.Bochner.L1` `Mathlib.MeasureTheory.Integral.Bochner.Set` `Mathlib.MeasureTheory.Integral.Bochner.SumMeasure` `Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory` `Mathlib.MeasureTheory.Integral.BoundedContinuousFunction` `Mathlib.MeasureTheory.Integral.CircleAverage` `Mathlib.MeasureTheory.Integral.CircleIntegral` `Mathlib.MeasureTheory.Integral.CircleTransform` `Mathlib.MeasureTheory.Integral.CompactlySupported` `Mathlib.MeasureTheory.Integral.CurveIntegral.Basic` `Mathlib.MeasureTheory.Integral.CurveIntegral.Poincare` `Mathlib.MeasureTheory.Integral.DivergenceTheorem` `Mathlib.MeasureTheory.Integral.DominatedConvergence` `Mathlib.MeasureTheory.Integral.ExpDecay` `Mathlib.MeasureTheory.Integral.FinMeasAdditive` `Mathlib.MeasureTheory.Integral.Gamma` `Mathlib.MeasureTheory.Integral.Indicator` `Mathlib.MeasureTheory.Integral.IntegrableOn` `Mathlib.MeasureTheory.Integral.IntegralEqImproper` `Mathlib.MeasureTheory.Integral.IntervalAverage` `Mathlib.MeasureTheory.Integral.IntervalIntegral.AbsolutelyContinuousFun` `Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic` `Mathlib.MeasureTheory.Integral.IntervalIntegral.ContDiff` `Mathlib.MeasureTheory.Integral.IntervalIntegral.DerivIntegrable` `Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral` `Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus` `Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts` `Mathlib.MeasureTheory.Integral.IntervalIntegral.LebesgueDifferentiationThm` `Mathlib.MeasureTheory.Integral.IntervalIntegral.MeanValue` `Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic` `Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope` `Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule` `Mathlib.MeasureTheory.Integral.Layercake` `Mathlib.MeasureTheory.Integral.Lebesgue.Add` `Mathlib.MeasureTheory.Integral.Lebesgue.Basic` `Mathlib.MeasureTheory.Integral.Lebesgue.Countable` `Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence` `Mathlib.MeasureTheory.Integral.Lebesgue.Map` `Mathlib.MeasureTheory.Integral.Lebesgue.Markov` `Mathlib.MeasureTheory.Integral.Lebesgue.Norm` `Mathlib.MeasureTheory.Integral.Lebesgue.Sub` `Mathlib.MeasureTheory.Integral.LebesgueNormedSpace` `Mathlib.MeasureTheory.Integral.Marginal` `Mathlib.MeasureTheory.Integral.MeanInequalities` `Mathlib.MeasureTheory.Integral.MeanValue` `Mathlib.MeasureTheory.Integral.PeakFunction` `Mathlib.MeasureTheory.Integral.Pi` `Mathlib.MeasureTheory.Integral.Prod` `Mathlib.MeasureTheory.Integral.Regular` `Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic` `Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal` `Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real` `Mathlib.MeasureTheory.Integral.SetToL1.ChangeMeasure` `Mathlib.MeasureTheory.Integral.SetToL1.DominatedConvergence` `Mathlib.MeasureTheory.Integral.SetToL1.Function` `Mathlib.MeasureTheory.Integral.SetToL1.L1` `Mathlib.MeasureTheory.Integral.SetToL1.SimpleFunc` `Mathlib.MeasureTheory.Integral.SetToL1` `Mathlib.MeasureTheory.Integral.TorusIntegral` `Mathlib.MeasureTheory.Measure.AEDisjoint` `Mathlib.MeasureTheory.Measure.AEMeasurable` `Mathlib.MeasureTheory.Measure.AbsolutelyContinuous` `Mathlib.MeasureTheory.Measure.AddContent` `Mathlib.MeasureTheory.Measure.Basic` `Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic` `Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion` `Mathlib.MeasureTheory.Measure.CharacteristicFunction` `Mathlib.MeasureTheory.Measure.Comap` `Mathlib.MeasureTheory.Measure.CompleteLattice` `Mathlib.MeasureTheory.Measure.Complex` `Mathlib.MeasureTheory.Measure.Content` `Mathlib.MeasureTheory.Measure.Continuity` `Mathlib.MeasureTheory.Measure.ContinuousPreimage` `Mathlib.MeasureTheory.Measure.Count` `Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion` `Mathlib.MeasureTheory.Measure.Decomposition.Hahn` `Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv` `Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue` `Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym` `Mathlib.MeasureTheory.Measure.Dirac.Basic` `Mathlib.MeasureTheory.Measure.Dirac.Def` `Mathlib.MeasureTheory.Measure.DiracProba` `Mathlib.MeasureTheory.Measure.Dirac` `Mathlib.MeasureTheory.Measure.Doubling` `Mathlib.MeasureTheory.Measure.EverywherePos` `Mathlib.MeasureTheory.Measure.Filter` `Mathlib.MeasureTheory.Measure.FiniteMeasureExt` `Mathlib.MeasureTheory.Measure.FiniteMeasurePi` `Mathlib.MeasureTheory.Measure.FiniteMeasureProd` `Mathlib.MeasureTheory.Measure.FiniteMeasure` `Mathlib.MeasureTheory.Measure.GiryMonad` `Mathlib.MeasureTheory.Measure.Haar.Basic` `Mathlib.MeasureTheory.Measure.Haar.Disintegration` `Mathlib.MeasureTheory.Measure.Haar.DistribChar` `Mathlib.MeasureTheory.Measure.Haar.Extension` `Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace` `Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar` `Mathlib.MeasureTheory.Measure.Haar.NormedSpace` `Mathlib.MeasureTheory.Measure.Haar.OfBasis` `Mathlib.MeasureTheory.Measure.Haar.Quotient` `Mathlib.MeasureTheory.Measure.Haar.Unique` `Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd` `Mathlib.MeasureTheory.Measure.HasOuterApproxClosed` `Mathlib.MeasureTheory.Measure.Hausdorff` `Mathlib.MeasureTheory.Measure.IntegralCharFun` `Mathlib.MeasureTheory.Measure.Interval` `Mathlib.MeasureTheory.Measure.Lebesgue.Basic` `Mathlib.MeasureTheory.Measure.Lebesgue.Complex` `Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar` `Mathlib.MeasureTheory.Measure.Lebesgue.Integral` `Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls` `Mathlib.MeasureTheory.Measure.LevyConvergence` `Mathlib.MeasureTheory.Measure.LevyProkhorovMetric` `Mathlib.MeasureTheory.Measure.LogLikelihoodRatio` `Mathlib.MeasureTheory.Measure.Map` `Mathlib.MeasureTheory.Measure.MeasureSpaceDef` `Mathlib.MeasureTheory.Measure.MeasureSpace` `Mathlib.MeasureTheory.Measure.MeasuredSets` `Mathlib.MeasureTheory.Measure.Module` `Mathlib.MeasureTheory.Measure.MutuallySingular` `Mathlib.MeasureTheory.Measure.NullMeasurable` `Mathlib.MeasureTheory.Measure.OpenPos` `Mathlib.MeasureTheory.Measure.OuterMeasure` `Mathlib.MeasureTheory.Measure.Portmanteau` `Mathlib.MeasureTheory.Measure.PreVariation` `Mathlib.MeasureTheory.Measure.ProbabilityMeasure` `Mathlib.MeasureTheory.Measure.Prod` `Mathlib.MeasureTheory.Measure.Prokhorov` `Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving` `Mathlib.MeasureTheory.Measure.Real` `Mathlib.MeasureTheory.Measure.Regular` `Mathlib.MeasureTheory.Measure.RegularityCompacts` `Mathlib.MeasureTheory.Measure.ResolventTransform` `Mathlib.MeasureTheory.Measure.Restrict` `Mathlib.MeasureTheory.Measure.SeparableMeasure` `Mathlib.MeasureTheory.Measure.Stieltjes` `Mathlib.MeasureTheory.Measure.SubFinite` `Mathlib.MeasureTheory.Measure.Sub` `Mathlib.MeasureTheory.Measure.Sum` `Mathlib.MeasureTheory.Measure.Support` `Mathlib.MeasureTheory.Measure.TightNormed` `Mathlib.MeasureTheory.Measure.Tight` `Mathlib.MeasureTheory.Measure.Tilted` `Mathlib.MeasureTheory.Measure.Trim` `Mathlib.MeasureTheory.Measure.Typeclasses.Finite` `Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass` `Mathlib.MeasureTheory.Measure.Typeclasses.Probability` `Mathlib.MeasureTheory.Measure.Typeclasses.SFinite` `Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne` `Mathlib.MeasureTheory.Measure.WithDensityFinite` `Mathlib.MeasureTheory.Measure.WithDensity` `Mathlib.MeasureTheory.Order.Group.Lattice` `Mathlib.MeasureTheory.Order.Lattice` `Mathlib.MeasureTheory.Order.UpperLower` `Mathlib.MeasureTheory.OuterMeasure.AE` `Mathlib.MeasureTheory.OuterMeasure.Basic` `Mathlib.MeasureTheory.OuterMeasure.BorelCantelli` `Mathlib.MeasureTheory.OuterMeasure.Caratheodory` `Mathlib.MeasureTheory.OuterMeasure.Induced` `Mathlib.MeasureTheory.OuterMeasure.OfAddContent` `Mathlib.MeasureTheory.OuterMeasure.OfFunction` `Mathlib.MeasureTheory.OuterMeasure.Operations` `Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero` `Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap` `Mathlib.MeasureTheory.SpecificCodomains.Pi` `Mathlib.MeasureTheory.SpecificCodomains.WithLp` `Mathlib.MeasureTheory.Topology` `Mathlib.MeasureTheory.VectorMeasure.AddContent` `Mathlib.MeasureTheory.VectorMeasure.Basic` `Mathlib.MeasureTheory.VectorMeasure.BoundedVariation` `Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn` `Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub` `Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan` `Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue` `Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym` `Mathlib.MeasureTheory.VectorMeasure.Integral` `Mathlib.MeasureTheory.VectorMeasure.IntegrationByParts` `Mathlib.MeasureTheory.VectorMeasure.Operations` `Mathlib.MeasureTheory.VectorMeasure.Order` `Mathlib.MeasureTheory.VectorMeasure.Prod` `Mathlib.MeasureTheory.VectorMeasure.Relations` `Mathlib.MeasureTheory.VectorMeasure.SetIntegral` `Mathlib.MeasureTheory.VectorMeasure.Variation.Basic` `Mathlib.MeasureTheory.VectorMeasure.Variation.Defs` `Mathlib.MeasureTheory.VectorMeasure.Variation.Semivariation` `Mathlib.MeasureTheory.VectorMeasure.Variation.SignedMeasure` `Mathlib.MeasureTheory.VectorMeasure.WithDensityVec` `Mathlib.MeasureTheory.VectorMeasure.WithDensity` `Mathlib.NumberTheory.AbelSummation` `Mathlib.NumberTheory.ArithmeticFunction.Carmichael` `Mathlib.NumberTheory.ArithmeticFunction.LFunction` `Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt` `Mathlib.NumberTheory.BernoulliPolynomials` `Mathlib.NumberTheory.Bernoulli` `Mathlib.NumberTheory.Bertrand` `Mathlib.NumberTheory.CarmichaelNumber` `Mathlib.NumberTheory.Chebyshev` `Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree` `Mathlib.NumberTheory.ClassNumber.Finite` `Mathlib.NumberTheory.ClassNumber.FunctionField` `Mathlib.NumberTheory.Cyclotomic.Basic` `Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter` `Mathlib.NumberTheory.Cyclotomic.Discriminant` `Mathlib.NumberTheory.Cyclotomic.Gal` `Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots` `Mathlib.NumberTheory.DiophantineApproximation.Basic` `Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions` `Mathlib.NumberTheory.DirichletCharacter.Bounds` `Mathlib.NumberTheory.DirichletCharacter.GaussSum` `Mathlib.NumberTheory.DirichletCharacter.Orthogonality` `Mathlib.NumberTheory.EulerProduct.Basic` `Mathlib.NumberTheory.EulerProduct.DirichletLSeries` `Mathlib.NumberTheory.EulerProduct.ExpLog` `Mathlib.NumberTheory.FLT.Three` `Mathlib.NumberTheory.Fermat` `Mathlib.NumberTheory.FunctionField` `Mathlib.NumberTheory.GaussSum` `Mathlib.NumberTheory.Harmonic.Bounds` `Mathlib.NumberTheory.Harmonic.EulerMascheroni` `Mathlib.NumberTheory.Harmonic.GammaDeriv` `Mathlib.NumberTheory.Harmonic.Int` `Mathlib.NumberTheory.Harmonic.ZetaAsymp` `Mathlib.NumberTheory.Height.Basic` `Mathlib.NumberTheory.Height.EllipticCurve` `Mathlib.NumberTheory.Height.MvPolynomial` `Mathlib.NumberTheory.Height.Northcott` `Mathlib.NumberTheory.Height.NumberField` `Mathlib.NumberTheory.Height.Projectivization` `Mathlib.NumberTheory.JacobiSum.Basic` `Mathlib.NumberTheory.LSeries.AbstractFuncEq` `Mathlib.NumberTheory.LSeries.Basic` `Mathlib.NumberTheory.LSeries.Convergence` `Mathlib.NumberTheory.LSeries.Convolution` `Mathlib.NumberTheory.LSeries.Deriv` `Mathlib.NumberTheory.LSeries.DirichletContinuation` `Mathlib.NumberTheory.LSeries.Dirichlet` `Mathlib.NumberTheory.LSeries.HurwitzZetaEven` `Mathlib.NumberTheory.LSeries.HurwitzZetaOdd` `Mathlib.NumberTheory.LSeries.HurwitzZetaValues` `Mathlib.NumberTheory.LSeries.HurwitzZeta` `Mathlib.NumberTheory.LSeries.Injectivity` `Mathlib.NumberTheory.LSeries.Linearity` `Mathlib.NumberTheory.LSeries.MellinEqDirichlet` `Mathlib.NumberTheory.LSeries.Nonvanishing` `Mathlib.NumberTheory.LSeries.Positivity` `Mathlib.NumberTheory.LSeries.PrimesInAP` `Mathlib.NumberTheory.LSeries.RiemannZetaLogDeriv` `Mathlib.NumberTheory.LSeries.RiemannZeta` `Mathlib.NumberTheory.LSeries.SumCoeff` `Mathlib.NumberTheory.LSeries.ZMod` `Mathlib.NumberTheory.LSeries.ZetaZeros` `Mathlib.NumberTheory.LegendreSymbol.AddCharacter` `Mathlib.NumberTheory.LegendreSymbol.Complex` `Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum` `Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity` `Mathlib.NumberTheory.LocalField.Basic` `Mathlib.NumberTheory.LucasLehmer` `Mathlib.NumberTheory.MahlerMeasure` `Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups` `Mathlib.NumberTheory.ModularForms.Basic` `Mathlib.NumberTheory.ModularForms.BoundedAtCusp` `Mathlib.NumberTheory.ModularForms.Bounds` `Mathlib.NumberTheory.ModularForms.CongruenceSubgroups` `Mathlib.NumberTheory.ModularForms.CuspFormSubmodule` `Mathlib.NumberTheory.ModularForms.Cusps` `Mathlib.NumberTheory.ModularForms.DedekindEta` `Mathlib.NumberTheory.ModularForms.Delta` `Mathlib.NumberTheory.ModularForms.Derivative` `Mathlib.NumberTheory.ModularForms.DimensionFormulas.LevelOne` `Mathlib.NumberTheory.ModularForms.Discriminant` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence` `Mathlib.NumberTheory.ModularForms.Identities` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold` `Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable` `Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable` `Mathlib.NumberTheory.ModularForms.LFunction` `Mathlib.NumberTheory.ModularForms.LevelOne.Basic` `Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula` `Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing` `Mathlib.NumberTheory.ModularForms.LevelOne` `Mathlib.NumberTheory.ModularForms.NormTrace` `Mathlib.NumberTheory.ModularForms.Petersson` `Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous` `Mathlib.NumberTheory.ModularForms.QExpansion` `Mathlib.NumberTheory.ModularForms.RamanujanFormula` `Mathlib.NumberTheory.ModularForms.SlashActions` `Mathlib.NumberTheory.ModularForms.SlashInvariantForms` `Mathlib.NumberTheory.Modular` `Mathlib.NumberTheory.MulChar.Duality` `Mathlib.NumberTheory.MulChar.Lemmas` `Mathlib.NumberTheory.Niven` `Mathlib.NumberTheory.NumberField.AdeleRing` `Mathlib.NumberTheory.NumberField.CMField` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord` `Mathlib.NumberTheory.NumberField.ClassNumber` `Mathlib.NumberTheory.NumberField.Completion.FinitePlace` `Mathlib.NumberTheory.NumberField.Completion.InfinitePlace` `Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances` `Mathlib.NumberTheory.NumberField.Completion.Ramification` `Mathlib.NumberTheory.NumberField.Cyclotomic.Basic` `Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings` `Mathlib.NumberTheory.NumberField.Cyclotomic.Galois` `Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal` `Mathlib.NumberTheory.NumberField.Cyclotomic.PID` `Mathlib.NumberTheory.NumberField.Cyclotomic.Three` `Mathlib.NumberTheory.NumberField.DedekindZeta` `Mathlib.NumberTheory.NumberField.DirichletDensity` `Mathlib.NumberTheory.NumberField.Discriminant.Basic` `Mathlib.NumberTheory.NumberField.Discriminant.Different` `Mathlib.NumberTheory.NumberField.EquivReindex` `Mathlib.NumberTheory.NumberField.ExistsRamified` `Mathlib.NumberTheory.NumberField.FiniteAdeleRing` `Mathlib.NumberTheory.NumberField.FinitePlaces` `Mathlib.NumberTheory.NumberField.House` `Mathlib.NumberTheory.NumberField.Ideal.Asymptotics` `Mathlib.NumberTheory.NumberField.Ideal.Basic` `Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind` `Mathlib.NumberTheory.NumberField.InfiniteAdeleRing` `Mathlib.NumberTheory.NumberField.InfinitePlace.Basic` `Mathlib.NumberTheory.NumberField.InfinitePlace.Completion` `Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings` `Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification` `Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex` `Mathlib.NumberTheory.NumberField.ProductFormula` `Mathlib.NumberTheory.NumberField.Units.Basic` `Mathlib.NumberTheory.NumberField.Units.DirichletTheorem` `Mathlib.NumberTheory.NumberField.Units.Regulator` `Mathlib.NumberTheory.Ostrowski` `Mathlib.NumberTheory.Padics.AddChar` `Mathlib.NumberTheory.Padics.Complex` `Mathlib.NumberTheory.Padics.HeightOneSpectrum` `Mathlib.NumberTheory.Padics.Hensel` `Mathlib.NumberTheory.Padics.LocalField` `Mathlib.NumberTheory.Padics.MahlerBasis` `Mathlib.NumberTheory.Padics.Measure.AmiceTransform` `Mathlib.NumberTheory.Padics.Measure.Basic` `Mathlib.NumberTheory.Padics.Measure.Topology` `Mathlib.NumberTheory.Padics.PadicIntegers` `Mathlib.NumberTheory.Padics.PadicNumbers` `Mathlib.NumberTheory.Padics.ProperSpace` `Mathlib.NumberTheory.Padics.RingHoms` `Mathlib.NumberTheory.Padics.ValuativeRel` `Mathlib.NumberTheory.Padics.WithVal` `Mathlib.NumberTheory.Pell` `Mathlib.NumberTheory.PrimesCongruentOne` `Mathlib.NumberTheory.RamificationInertia.Galois` `Mathlib.NumberTheory.RamificationInertia.HilbertTheory` `Mathlib.NumberTheory.RamificationInertia.Unramified` `Mathlib.NumberTheory.RamificationInertia.Valuation` `Mathlib.NumberTheory.RatFunc.Ostrowski` `Mathlib.NumberTheory.Rayleigh` `Mathlib.NumberTheory.Real.GoldenRatio` `Mathlib.NumberTheory.Real.Irrational` `Mathlib.NumberTheory.SiegelsLemma` `Mathlib.NumberTheory.SumPrimeReciprocals` `Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart` `Mathlib.NumberTheory.Transcendental.Liouville.Basic` `Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber` `Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith` `Mathlib.NumberTheory.Transcendental.Liouville.Measure` `Mathlib.NumberTheory.Transcendental.Liouville.Residual` `Mathlib.NumberTheory.TsumDivisorsAntidiagonal` `Mathlib.NumberTheory.WellApproximable` `Mathlib.NumberTheory.ZetaValues` `Mathlib.NumberTheory.Zsqrtd.ToReal` `Mathlib.Order.Filter.ZeroAndBoundedAtFilter` `Mathlib.Probability.BorelCantelli` `Mathlib.Probability.BrownianMotion.Basic` `Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily` `Mathlib.Probability.CDF` `Mathlib.Probability.CentralLimitTheorem` `Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs` `Mathlib.Probability.CondVar` `Mathlib.Probability.ConditionalExpectation` `Mathlib.Probability.ConditionalProbability` `Mathlib.Probability.CramerWold` `Mathlib.Probability.Decision.BayesEstimator` `Mathlib.Probability.Decision.Risk.Basic` `Mathlib.Probability.Decision.Risk.Countable` `Mathlib.Probability.Decision.Risk.Defs` `Mathlib.Probability.Decision.Risk.RiskIncrease` `Mathlib.Probability.Density` `Mathlib.Probability.Distributions.Bernoulli` `Mathlib.Probability.Distributions.Beta` `Mathlib.Probability.Distributions.Binomial` `Mathlib.Probability.Distributions.Cauchy` `Mathlib.Probability.Distributions.Exponential` `Mathlib.Probability.Distributions.Fernique` `Mathlib.Probability.Distributions.Gamma` `Mathlib.Probability.Distributions.Gaussian.Basic` `Mathlib.Probability.Distributions.Gaussian.CharFun` `Mathlib.Probability.Distributions.Gaussian.Fernique` `Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic` `Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Def` `Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence` `Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic` `Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Def` `Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence` `Mathlib.Probability.Distributions.Gaussian.Multivariate` `Mathlib.Probability.Distributions.Gaussian.Real` `Mathlib.Probability.Distributions.Geometric` `Mathlib.Probability.Distributions.Pareto` `Mathlib.Probability.Distributions.Poisson.Basic` `Mathlib.Probability.Distributions.Poisson.PoissonLimitThm` `Mathlib.Probability.Distributions.SetBernoulli` `Mathlib.Probability.Distributions.TwoValued` `Mathlib.Probability.Distributions.Uniform` `Mathlib.Probability.HasCondDistrib` `Mathlib.Probability.HasLawExists` `Mathlib.Probability.HasLaw` `Mathlib.Probability.IdentDistribIndep` `Mathlib.Probability.IdentDistrib` `Mathlib.Probability.Independence.Basic` `Mathlib.Probability.Independence.BoundedContinuousFunction` `Mathlib.Probability.Independence.CharacteristicFunction` `Mathlib.Probability.Independence.Conditional` `Mathlib.Probability.Independence.InfinitePi` `Mathlib.Probability.Independence.Integrable` `Mathlib.Probability.Independence.Integration` `Mathlib.Probability.Independence.Kernel.IndepFun` `Mathlib.Probability.Independence.Kernel.Indep` `Mathlib.Probability.Independence.Process.Basic` `Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic` `Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess` `Mathlib.Probability.Independence.Process.HasIndepIncrements` `Mathlib.Probability.Independence.ZeroOne` `Mathlib.Probability.Kernel.Basic` `Mathlib.Probability.Kernel.Category.SFinKer` `Mathlib.Probability.Kernel.Category.Stoch` `Mathlib.Probability.Kernel.CompProdEqIff` `Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous` `Mathlib.Probability.Kernel.Composition.CompMap` `Mathlib.Probability.Kernel.Composition.CompNotation` `Mathlib.Probability.Kernel.Composition.CompProd` `Mathlib.Probability.Kernel.Composition.Comp` `Mathlib.Probability.Kernel.Composition.IntegralCompProd` `Mathlib.Probability.Kernel.Composition.KernelLemmas` `Mathlib.Probability.Kernel.Composition.Lemmas` `Mathlib.Probability.Kernel.Composition.MapComap` `Mathlib.Probability.Kernel.Composition.MeasureCompProd` `Mathlib.Probability.Kernel.Composition.MeasureComp` `Mathlib.Probability.Kernel.Composition.ParallelComp` `Mathlib.Probability.Kernel.Composition.Prod` `Mathlib.Probability.Kernel.Composition.RadonNikodym` `Mathlib.Probability.Kernel.Composition.WithDensity` `Mathlib.Probability.Kernel.CondDistrib` `Mathlib.Probability.Kernel.Condexp` `Mathlib.Probability.Kernel.Defs` `Mathlib.Probability.Kernel.Deterministic` `Mathlib.Probability.Kernel.Disintegration.Basic` `Mathlib.Probability.Kernel.Disintegration.CDFToKernel` `Mathlib.Probability.Kernel.Disintegration.CondCDF` `Mathlib.Probability.Kernel.Disintegration.Density` `Mathlib.Probability.Kernel.Disintegration.Integral` `Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes` `Mathlib.Probability.Kernel.Disintegration.StandardBorel` `Mathlib.Probability.Kernel.Disintegration.Unique` `Mathlib.Probability.Kernel.Integral` `Mathlib.Probability.Kernel.Invariance` `Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj` `Mathlib.Probability.Kernel.IonescuTulcea.Traj` `Mathlib.Probability.Kernel.Irreducible` `Mathlib.Probability.Kernel.MeasurableIntegral` `Mathlib.Probability.Kernel.MeasurableLIntegral` `Mathlib.Probability.Kernel.Posterior` `Mathlib.Probability.Kernel.Proper` `Mathlib.Probability.Kernel.RadonNikodym` `Mathlib.Probability.Kernel.Representation` `Mathlib.Probability.Kernel.SetIntegral` `Mathlib.Probability.Kernel.WithDensity` `Mathlib.Probability.Martingale.Basic` `Mathlib.Probability.Martingale.BorelCantelli` `Mathlib.Probability.Martingale.Centering` `Mathlib.Probability.Martingale.Convergence` `Mathlib.Probability.Martingale.OptionalSampling` `Mathlib.Probability.Martingale.OptionalStopping` `Mathlib.Probability.Martingale.Upcrossing` `Mathlib.Probability.Moments.Basic` `Mathlib.Probability.Moments.ComplexMGF` `Mathlib.Probability.Moments.CovarianceBilinDual` `Mathlib.Probability.Moments.CovarianceBilin` `Mathlib.Probability.Moments.Covariance` `Mathlib.Probability.Moments.IntegrableExpMul` `Mathlib.Probability.Moments.MGFAnalytic` `Mathlib.Probability.Moments.SubGaussian` `Mathlib.Probability.Moments.Tilted` `Mathlib.Probability.Moments.Variance` `Mathlib.Probability.Notation` `Mathlib.Probability.ProbabilityMassFunction.Basic` `Mathlib.Probability.ProbabilityMassFunction.Binomial` `Mathlib.Probability.ProbabilityMassFunction.Constructions` `Mathlib.Probability.ProbabilityMassFunction.Integrals` `Mathlib.Probability.ProbabilityMassFunction.Monad` `Mathlib.Probability.Process.Adapted` `Mathlib.Probability.Process.Filtration` `Mathlib.Probability.Process.FiniteDimensionalLaws` `Mathlib.Probability.Process.HittingTime` `Mathlib.Probability.Process.Kolmogorov` `Mathlib.Probability.Process.LocalProperty` `Mathlib.Probability.Process.PartitionFiltration` `Mathlib.Probability.Process.Predictable` `Mathlib.Probability.Process.Stopping` `Mathlib.Probability.ProductMeasure` `Mathlib.Probability.StrongLaw` `Mathlib.Probability.UniformOn` `Mathlib.RepresentationTheory.Continuous.Basic` `Mathlib.RepresentationTheory.Continuous.TopRep` `Mathlib.RepresentationTheory.Homological.ContCohomology.Basic` `Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality` `Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree` `Mathlib.RingTheory.AdicCompletion.AsTensorProduct` `Mathlib.RingTheory.AdicCompletion.Completeness` `Mathlib.RingTheory.AdicCompletion.LocalRing` `Mathlib.RingTheory.AdicCompletion.Topology` `Mathlib.RingTheory.DedekindDomain.AdicValuation` `Mathlib.RingTheory.DedekindDomain.Different` `Mathlib.RingTheory.DedekindDomain.Factorization` `Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing` `Mathlib.RingTheory.DedekindDomain.GaussLemma` `Mathlib.RingTheory.DedekindDomain.LinearDisjoint` `Mathlib.RingTheory.DedekindDomain.SInteger` `Mathlib.RingTheory.DedekindDomain.SelmerGroup` `Mathlib.RingTheory.DividedPowers.Padic` `Mathlib.RingTheory.Etale.Descent` `Mathlib.RingTheory.Etale.Finite` `Mathlib.RingTheory.Etale.Locus` `Mathlib.RingTheory.Etale.QuasiFinite` `Mathlib.RingTheory.Etale.Weakly` `Mathlib.RingTheory.Flat.EquationalCriterion` `Mathlib.RingTheory.Flat.LocallyFree` `Mathlib.RingTheory.Flat.Rank` `Mathlib.RingTheory.Flat.Tensor` `Mathlib.RingTheory.Flat.TorsionFree` `Mathlib.RingTheory.FormalGroup.Basic` `Mathlib.RingTheory.Grassmannian` `Mathlib.RingTheory.HahnSeries.HahnEmbedding` `Mathlib.RingTheory.Ideal.Norm.RelNorm` `Mathlib.RingTheory.Ideal.Pure` `Mathlib.RingTheory.IdealFilter.Topology` `Mathlib.RingTheory.Invariant.Profinite` `Mathlib.RingTheory.KrullDimension.Regular` `Mathlib.RingTheory.LaurentSeries` `Mathlib.RingTheory.LittleWedderburn` `Mathlib.RingTheory.LocalProperties.InjectiveDimension` `Mathlib.RingTheory.LocalRing.Etale` `Mathlib.RingTheory.LocalRing.Module` `Mathlib.RingTheory.LocalRing.ResidueField.Polynomial` `Mathlib.RingTheory.Localization.AtPrime.Extension` `Mathlib.RingTheory.MvPowerSeries.Equiv` `Mathlib.RingTheory.MvPowerSeries.Evaluation` `Mathlib.RingTheory.MvPowerSeries.Expand` `Mathlib.RingTheory.MvPowerSeries.LinearTopology` `Mathlib.RingTheory.MvPowerSeries.PiTopology` `Mathlib.RingTheory.MvPowerSeries.Rename` `Mathlib.RingTheory.MvPowerSeries.Restricted` `Mathlib.RingTheory.MvPowerSeries.Substitution` `Mathlib.RingTheory.OrderOfVanishing.Noetherian` `Mathlib.RingTheory.Perfection` `Mathlib.RingTheory.Perfectoid.BDeRham` `Mathlib.RingTheory.Perfectoid.FontaineTheta` `Mathlib.RingTheory.Perfectoid.Untilt` `Mathlib.RingTheory.PicardGroup` `Mathlib.RingTheory.Polynomial.Cyclotomic.Basic` `Mathlib.RingTheory.Polynomial.Cyclotomic.Eval` `Mathlib.RingTheory.Polynomial.Cyclotomic.Expand` `Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization` `Mathlib.RingTheory.Polynomial.Cyclotomic.Roots` `Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral` `Mathlib.RingTheory.Polynomial.Hermite.Gaussian` `Mathlib.RingTheory.Polynomial.Selmer` `Mathlib.RingTheory.PowerSeries.Derivative` `Mathlib.RingTheory.PowerSeries.Evaluation` `Mathlib.RingTheory.PowerSeries.Exp` `Mathlib.RingTheory.PowerSeries.Expand` `Mathlib.RingTheory.PowerSeries.Log` `Mathlib.RingTheory.PowerSeries.PiTopology` `Mathlib.RingTheory.PowerSeries.Restricted` `Mathlib.RingTheory.PowerSeries.Substitution` `Mathlib.RingTheory.QuasiFinite.Polynomial` `Mathlib.RingTheory.RamificationInertia.Basic` `Mathlib.RingTheory.RamificationInertia.Ramification` `Mathlib.RingTheory.Regular.ProjectiveDimension` `Mathlib.RingTheory.RegularLocalRing.Defs` `Mathlib.RingTheory.RegularLocalRing.Polynomial` `Mathlib.RingTheory.RingHom.Etale` `Mathlib.RingTheory.RingHom.LocallyStandardSmooth` `Mathlib.RingTheory.RingHom.Smooth` `Mathlib.RingTheory.RingHom.StandardSmooth` `Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed` `Mathlib.RingTheory.RootsOfUnity.Complex` `Mathlib.RingTheory.Smooth.Fiber` `Mathlib.RingTheory.Smooth.Flat` `Mathlib.RingTheory.Smooth.IntegralClosure` `Mathlib.RingTheory.Smooth.Local` `Mathlib.RingTheory.Smooth.Locus` `Mathlib.RingTheory.Smooth.NoetherianDescent` `Mathlib.RingTheory.Smooth.Quotient` `Mathlib.RingTheory.Smooth.StandardSmoothOfFree` `Mathlib.RingTheory.Spectrum.Prime.FreeLocus` `Mathlib.RingTheory.Teichmuller` `Mathlib.RingTheory.TotallySplit` `Mathlib.RingTheory.Unramified.LocalRing` `Mathlib.RingTheory.Unramified.LocalStructure` `Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing` `Mathlib.RingTheory.Valuation.Discrete.RankOne` `Mathlib.RingTheory.Valuation.DiscreteValuativeRel` `Mathlib.RingTheory.Valuation.RankOne` `Mathlib.RingTheory.WittVector.Compare` `Mathlib.RingTheory.ZMod.UnitsCyclic` `Mathlib.RingTheory.ZariskisMainTheorem` `Mathlib.Tactic.ComputeAsymptotics.Lemmas` `Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic` `Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis` `Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion` `Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs` `Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized` `Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic` `Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming` `Mathlib.Tactic.NormNum.Irrational` `Mathlib.Tactic.NormNum.LegendreSymbol` `Mathlib.Tactic.NormNum.RealSqrt` `Mathlib.Tactic` `Mathlib.Topology.Algebra.AffineSubspace` `Mathlib.Topology.Algebra.Affine` `Mathlib.Topology.Algebra.Algebra.Equiv` `Mathlib.Topology.Algebra.Algebra` `Mathlib.Topology.Algebra.AsymptoticCone` `Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic` `Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion` `Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits` `Mathlib.Topology.Algebra.ClopenNhdofOne` `Mathlib.Topology.Algebra.ContinuousAffineEquiv` `Mathlib.Topology.Algebra.ContinuousAffineMap.Topology` `Mathlib.Topology.Algebra.ContinuousAffineMap` `Mathlib.Topology.Algebra.FilterBasis` `Mathlib.Topology.Algebra.Group.AddTorsor` `Mathlib.Topology.Algebra.Group.ClosedSubgroup` `Mathlib.Topology.Algebra.Group.CompactOpen` `Mathlib.Topology.Algebra.Group.Compact` `Mathlib.Topology.Algebra.Group.Extension` `Mathlib.Topology.Algebra.Group.Matrix` `Mathlib.Topology.Algebra.Group.OpenMapping` `Mathlib.Topology.Algebra.Group.Pointwise` `Mathlib.Topology.Algebra.Group.Quotient` `Mathlib.Topology.Algebra.Group.Torsor` `Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt` `Mathlib.Topology.Algebra.InfiniteSum.Constructions` `Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution` `Mathlib.Topology.Algebra.InfiniteSum.ENNReal` `Mathlib.Topology.Algebra.InfiniteSum.Field` `Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion` `Mathlib.Topology.Algebra.InfiniteSum.Group` `Mathlib.Topology.Algebra.InfiniteSum.Module` `Mathlib.Topology.Algebra.InfiniteSum.NatInt` `Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean` `Mathlib.Topology.Algebra.InfiniteSum.Order` `Mathlib.Topology.Algebra.InfiniteSum.Real` `Mathlib.Topology.Algebra.InfiniteSum.Ring` `Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn` `Mathlib.Topology.Algebra.IsOpenUnits` `Mathlib.Topology.Algebra.IsUniformGroup.Basic` `Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup` `Mathlib.Topology.Algebra.LinearMapCompletion` `Mathlib.Topology.Algebra.LinearTopology` `Mathlib.Topology.Algebra.Module.Alternating.Basic` `Mathlib.Topology.Algebra.Module.Alternating.Topology` `Mathlib.Topology.Algebra.Module.Basic` `Mathlib.Topology.Algebra.Module.Cardinality` `Mathlib.Topology.Algebra.Module.ClosedSubmodule` `Mathlib.Topology.Algebra.Module.Complement` `Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic` `Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Extend` `Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent` `Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Invertible` `Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd` `Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Positive` `Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient` `Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars` `Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict` `Mathlib.Topology.Algebra.Module.Determinant` `Mathlib.Topology.Algebra.Module.EmbeddingOfLocal` `Mathlib.Topology.Algebra.Module.Equiv` `Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear` `Mathlib.Topology.Algebra.Module.FiniteDimension` `Mathlib.Topology.Algebra.Module.IsWeak` `Mathlib.Topology.Algebra.Module.LinearMapPiProd` `Mathlib.Topology.Algebra.Module.LinearMap` `Mathlib.Topology.Algebra.Module.LinearPMap` `Mathlib.Topology.Algebra.Module.LocallyConvex` `Mathlib.Topology.Algebra.Module.ModuleTopology` `Mathlib.Topology.Algebra.Module.Multilinear.Basic` `Mathlib.Topology.Algebra.Module.Multilinear.Bounded` `Mathlib.Topology.Algebra.Module.Multilinear.Topology` `Mathlib.Topology.Algebra.Module.PerfectPairing` `Mathlib.Topology.Algebra.Module.PerfectSpace` `Mathlib.Topology.Algebra.Module.Simple` `Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace` `Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM` `Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap` `Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM` `Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM` `Mathlib.Topology.Algebra.Module.Spaces.WeakBilin` `Mathlib.Topology.Algebra.Module.Spaces.WeakDual` `Mathlib.Topology.Algebra.Module.Star` `Mathlib.Topology.Algebra.Module.StrongTopology` `Mathlib.Topology.Algebra.Module.TopDualPairing` `Mathlib.Topology.Algebra.Module.TransferInstance` `Mathlib.Topology.Algebra.Module.UniformConvergence` `Mathlib.Topology.Algebra.NonUnitalAlgebra` `Mathlib.Topology.Algebra.NonUnitalStarAlgebra` `Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology` `Mathlib.Topology.Algebra.Nonarchimedean.Bases` `Mathlib.Topology.Algebra.Nonarchimedean.Basic` `Mathlib.Topology.Algebra.Nonarchimedean.Completion` `Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected` `Mathlib.Topology.Algebra.OpenSubgroup` `Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete` `Mathlib.Topology.Algebra.Order.UpperLower` `Mathlib.Topology.Algebra.Polynomial` `Mathlib.Topology.Algebra.PontryaginDual` `Mathlib.Topology.Algebra.ProperAction.AddTorsor` `Mathlib.Topology.Algebra.ProperAction.Basic` `Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated` `Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous` `Mathlib.Topology.Algebra.ProperAction.Torsor` `Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace` `Mathlib.Topology.Algebra.Ring.Compact` `Mathlib.Topology.Algebra.Ring.Ideal` `Mathlib.Topology.Algebra.SeparationQuotient.Basic` `Mathlib.Topology.Algebra.SeparationQuotient.FiniteDimensional` `Mathlib.Topology.Algebra.SeparationQuotient.Hom` `Mathlib.Topology.Algebra.SeparationQuotient.Section` `Mathlib.Topology.Algebra.Star.LinearMap` `Mathlib.Topology.Algebra.StarSubalgebra` `Mathlib.Topology.Algebra.TopologicallyNilpotent` `Mathlib.Topology.Algebra.UniformField` `Mathlib.Topology.Algebra.UniformFilterBasis` `Mathlib.Topology.Algebra.UniformRing` `Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology` `Mathlib.Topology.Algebra.Valued.LocallyCompact` `Mathlib.Topology.Algebra.Valued.NormedValued` `Mathlib.Topology.Algebra.Valued.ValuationTopology` `Mathlib.Topology.Algebra.Valued.ValuativeRel` `Mathlib.Topology.Algebra.Valued.ValuedField` `Mathlib.Topology.Algebra.Valued.WithVal` `Mathlib.Topology.Algebra.Valued.WithZeroMulInt` `Mathlib.Topology.Baire.BaireMeasurable` `Mathlib.Topology.Baire.CompleteMetrizable` `Mathlib.Topology.Bornology.BoundedOperation` `Mathlib.Topology.CWComplex.Abstract.Basic` `Mathlib.Topology.CWComplex.Classical.Basic` `Mathlib.Topology.CWComplex.Classical.Finite` `Mathlib.Topology.CWComplex.Classical.Graph` `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.Category.TopCat.Sphere` `Mathlib.Topology.Compactification.OnePoint.Sphere` `Mathlib.Topology.Compactness.CompactlyGeneratedSpace` `Mathlib.Topology.Compactness.DeltaGeneratedSpace` `Mathlib.Topology.Connected.PathComponentOne` `Mathlib.Topology.ContinuousMap.Algebra` `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.Lattice` `Mathlib.Topology.ContinuousMap.LocallyConstant` `Mathlib.Topology.ContinuousMap.LocallyConvex` `Mathlib.Topology.ContinuousMap.Periodic` `Mathlib.Topology.ContinuousMap.Polynomial` `Mathlib.Topology.ContinuousMap.StarOrdered` `Mathlib.Topology.ContinuousMap.Star` `Mathlib.Topology.ContinuousMap.StoneWeierstrass` `Mathlib.Topology.ContinuousMap.Units` `Mathlib.Topology.ContinuousMap.Weierstrass` `Mathlib.Topology.ContinuousMap.ZeroAtInftyUnitization` `Mathlib.Topology.ContinuousMap.ZeroAtInfty` `Mathlib.Topology.Covering.AddCircle` `Mathlib.Topology.Covering.Quotient` `Mathlib.Topology.EMetricSpace.BoundedVariation` `Mathlib.Topology.EMetricSpace.PairReduction` `Mathlib.Topology.EMetricSpace.VariationOnFromTo` `Mathlib.Topology.Homotopy.Lifting` `Mathlib.Topology.Instances.AddCircle.Defs` `Mathlib.Topology.Instances.AddCircle.DenseSubgroup` `Mathlib.Topology.Instances.AddCircle.Real` `Mathlib.Topology.Instances.CantorSet` `Mathlib.Topology.Instances.Complex` `Mathlib.Topology.Instances.ENNReal.ENatENNReal` `Mathlib.Topology.Instances.ENNReal.Lemmas` `Mathlib.Topology.Instances.EReal.Lemmas` `Mathlib.Topology.Instances.Irrational` `Mathlib.Topology.Instances.NNReal.Lemmas` `Mathlib.Topology.Instances.RatLemmas` `Mathlib.Topology.Instances.Real.Lemmas` `Mathlib.Topology.Instances.RealVectorSpace` `Mathlib.Topology.Instances.TrivSqZeroExt` `Mathlib.Topology.Instances.ZMultiples` `Mathlib.Topology.Maps.Strict.Group` `Mathlib.Topology.Maps.Strict.Module` `Mathlib.Topology.MetricSpace.Algebra` `Mathlib.Topology.MetricSpace.CantorScheme` `Mathlib.Topology.MetricSpace.CauSeqFilter` `Mathlib.Topology.MetricSpace.Closeds` `Mathlib.Topology.MetricSpace.Completion` `Mathlib.Topology.MetricSpace.Contracting` `Mathlib.Topology.MetricSpace.Cover` `Mathlib.Topology.MetricSpace.CoveringExponent` `Mathlib.Topology.MetricSpace.CoveringNumbers` `Mathlib.Topology.MetricSpace.GromovHausdorffRealized` `Mathlib.Topology.MetricSpace.GromovHausdorff` `Mathlib.Topology.MetricSpace.HausdorffAlexandroff` `Mathlib.Topology.MetricSpace.HausdorffDimension` `Mathlib.Topology.MetricSpace.HausdorffDistance` `Mathlib.Topology.MetricSpace.HolderNorm` `Mathlib.Topology.MetricSpace.Holder` `Mathlib.Topology.MetricSpace.Kuratowski` `Mathlib.Topology.MetricSpace.PartitionOfUnity` `Mathlib.Topology.MetricSpace.Perfect` `Mathlib.Topology.MetricSpace.PiNat` `Mathlib.Topology.MetricSpace.Polish` `Mathlib.Topology.MetricSpace.Snowflaking` `Mathlib.Topology.MetricSpace.ThickenedIndicator` `Mathlib.Topology.MetricSpace.Thickening` `Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps` `Mathlib.Topology.MetricSpace.UniformConvergence` `Mathlib.Topology.Metrizable.Urysohn` `Mathlib.Topology.Order.Cadlag` `Mathlib.Topology.Order.Category.FrameAdjunction` `Mathlib.Topology.PartitionOfUnity` `Mathlib.Topology.Semicontinuity.Basic` `Mathlib.Topology.Semicontinuity.Lindelof` `Mathlib.Topology.Semicontinuity.Michael` `Mathlib.Topology.Separation.CompletelyRegular` `Mathlib.Topology.Separation.Lemmas` `Mathlib.Topology.Separation.PerfectlyNormal` `Mathlib.Topology.Sheaves.CommRingCat` `Mathlib.Topology.Sion` `Mathlib.Topology.TietzeExtension` `Mathlib.Topology.UniformSpace.Dini` `Mathlib.Topology.UniformSpace.ProdApproximation` `Mathlib.Topology.UniformSpace.Uniformizable` `Mathlib.Topology.UrysohnsBounded` `Mathlib.Topology.UrysohnsLemma` `Mathlib.Topology.VectorBundle.Basic` `Mathlib.Topology.VectorBundle.Constructions` `Mathlib.Topology.VectorBundle.ContinuousAlternatingMap` `Mathlib.Topology.VectorBundle.FiniteDimensional` `Mathlib.Topology.VectorBundle.Hom` `Mathlib.Topology.VectorBundle.Riemannian`	1
`Mathlib.Combinatorics.Additive.ApproximateSubgroup`	2
`Mathlib.Algebra.Group.Pointwise.Finset.SelfInv` (new file)	686

Declarations diff (regex)

+ IsSelfInv.image
+ IsTopologicalGroup.mulInvClosureNhd.inv
+ closure_subset_mul_left_of_mem_nhds_one_of_isSelfInv
+ closure_subset_mul_right_of_mem_nhds_one_of_isSelfInv
+ closure_subset_of_mem_nhds_one_of_isSelfInv_mul_left_subset
+ closure_subset_of_mem_nhds_one_of_isSelfInv_mul_right_subset
+ exists_closed_nhds_one_isSelfInv_eq_mul_subset
+ inv_eq_self
+ isSelfInv_coe_iff
+ isSelfInv_iff_forall_inv_mem
+ isSelfInv_inter_inv
+ isSelfInv_union_inv

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 41e0985).

+24 new declarations
−0 removed declarations

+Finset.isSelfInv_coe_iff
+Finset.isSelfInv_iff_forall_inv_mem
+Finset.isSelfNeg_coe_iff
+Finset.isSelfNeg_iff_forall_neg_mem
+IsApproximateAddSubgroup.isSelfNeg
+IsApproximateSubgroup.isSelfInv
+IsSelfInv.image
+IsSelfNeg.image
+IsTopologicalAddGroup.addNegClosureNhd.isSelfNeg
+IsTopologicalGroup.mulInvClosureNhd.isSelfInv
+closure_subset_add_left_of_mem_nhds_zero_of_isSelfNeg
+closure_subset_add_right_of_mem_nhds_zero_of_isSelfNeg
+closure_subset_mul_left_of_mem_nhds_one_of_isSelfInv
+closure_subset_mul_right_of_mem_nhds_one_of_isSelfInv
+closure_subset_of_mem_nhds_one_of_isSelfInv_mul_left_subset
+closure_subset_of_mem_nhds_one_of_isSelfInv_mul_right_subset
+closure_subset_of_mem_nhds_zero_of_isSelfNeg_add_left_subset
+closure_subset_of_mem_nhds_zero_of_isSelfNeg_add_right_subset
+exists_closed_nhds_one_isSelfInv_eq_mul_subset
+exists_closed_nhds_zero_isSelfNeg_eq_add_subset
+isSelfInv_inter_inv
+isSelfInv_union_inv
+isSelfNeg_inter_neg
+isSelfNeg_union_neg

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (weak)
exposed public sections	5068	1

Current commit 41e098532e
Reference commit 3a33b9d429

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py 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-dependent-issues · 2026-09-13T13:20:51Z

This PR/issue depends on:

feat(Algebra/Group/Pointwise/Set/SelfInv): a few more lemmas about self-inverse sets #43773
By Dependent Issues (🤖). Happy coding!

eric-wieser · 2026-09-13T17:24:58Z

+
+@[to_additive]
+lemma isSelfInv_iff_forall_inv_mem : IsSelfInv s ↔ ∀ ⦃x⦄, x ∈ s → x⁻¹ ∈ s := by
+  simp only [← isSelfInv_coe_iff, _root_.isSelfInv_iff_forall_inv_mem, mem_coe]


Shouldn't isSelfInv_iff_forall_inv_mem be in the Set namespace?

I agree, opened #43792

refactor

81b2785

justus-springer mentioned this pull request Sep 13, 2026

feat(Algebra/Group/Pointwise/Set/SelfInv): a few more lemmas about self-inverse sets #43773

Open

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 Sep 13, 2026

eric-wieser reviewed Sep 13, 2026

View reviewed changes

justus-springer added the LLM-generated PRs with substantial input from LLMs - review accordingly label Sep 14, 2026

justus-springer added 2 commits September 14, 2026 09:53

Merge branch 'master' into justus/use-isSelfInv

84b7e7b

fix, add deprecations

41e0985

This was referenced Sep 14, 2026

chore(Algebra/Group/Pointwise/Set/SelfInv): put into lemmas into Set namespace #43792

Open

doc(Algebra/Group/SelfInv): extend module docstring #43793

Open

Navigation Menu

refactor(*): use `IsSelfInv` and `IsSelfNeg` - #43774

refactor(*): use `IsSelfInv` and `IsSelfNeg`#43774
justus-springer wants to merge 3 commits into
leanprover-community:masterfrom
justus-springer:justus/use-isSelfInv

justus-springer commented Sep 13, 2026

Uh oh!

github-actions Bot commented Sep 13, 2026 •

edited

Loading

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

mathlib-dependent-issues Bot commented Sep 13, 2026

Uh oh!

eric-wieser Sep 13, 2026

Uh oh!

justus-springer Sep 14, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

justus-springer commented Sep 13, 2026

Uh oh!

github-actions Bot commented Sep 13, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 41e098532e

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

mathlib-dependent-issues Bot commented Sep 13, 2026

Uh oh!

eric-wieser Sep 13, 2026

Choose a reason for hiding this comment

Uh oh!

justus-springer Sep 14, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

github-actions Bot commented Sep 13, 2026 •

edited

Loading