chore(Data/Real): encapsulate real numbers by jcommelin · Pull Request #38702 · leanprover-community/mathlib4

jcommelin · 2026-04-29T09:53:16Z

This PR:

hides the definition of the real numbers
preserves defeqs when casting Nat, Int, Rat, into the reals
preserves the defeq x - y = x + (-y) for x y : Real
removes a bunch of technical debt
adjusts imports in the library, where files relied on getting access to Cauchy sequences transitively via importing the reals.

github-actions · 2026-04-29T09:54:25Z

PR summary 1804a9da0a

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.UniformSpace.Real	1019	1021	+2 (+0.20%)
Mathlib.Topology.Algebra.Ring.Real	1191	1193	+2 (+0.17%)
Mathlib.Topology.UniformSpace.CompareReals	1204	1206	+2 (+0.17%)
Mathlib.Analysis.Complex.Norm	1305	1307	+2 (+0.15%)
Mathlib.Topology.Instances.Real.Lemmas	1336	1338	+2 (+0.15%)
Mathlib.Analysis.Real.Cardinality	1477	1479	+2 (+0.14%)
Mathlib.NumberTheory.Padics.PadicNumbers	1501	1503	+2 (+0.13%)
Mathlib.Analysis.RCLike.Basic	1591	1593	+2 (+0.13%)
Mathlib.NumberTheory.Padics.PadicIntegers	1617	1619	+2 (+0.12%)

Import changes for all files

Files	Import difference
168 files `Mathlib.Algebra.Order.Floor.Extended` `Mathlib.AlgebraicGeometry.EllipticCurve.Reduction` `Mathlib.AlgebraicGeometry.Group.Abelian` `Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite` `Mathlib.AlgebraicGeometry.Normalization` `Mathlib.AlgebraicGeometry.ZariskisMainTheorem` `Mathlib.Analysis.Asymptotics.Defs` `Mathlib.Analysis.BoxIntegral.Box.Basic` `Mathlib.Analysis.BoxIntegral.Partition.Basic` `Mathlib.Analysis.BoxIntegral.Partition.Split` `Mathlib.Analysis.BoxIntegral.Partition.Tagged` `Mathlib.Analysis.Calculus.TangentCone.Basic` `Mathlib.Analysis.Calculus.TangentCone.Defs` `Mathlib.Analysis.Calculus.TangentCone.Pi` `Mathlib.Analysis.Calculus.TangentCone.Prod` `Mathlib.Analysis.Convex.Cone.Extension` `Mathlib.Analysis.Convex.Extrema` `Mathlib.Analysis.Convex.NNReal` `Mathlib.Analysis.Convex.Visible` `Mathlib.Analysis.Normed.Affine.Simplex` `Mathlib.Analysis.Normed.Field.Basic` `Mathlib.Analysis.Normed.Field.TransferInstance` `Mathlib.Analysis.Normed.Group.AddTorsor` `Mathlib.Analysis.Normed.Group.Basic` `Mathlib.Analysis.Normed.Group.CocompactMap` `Mathlib.Analysis.Normed.Group.Constructions` `Mathlib.Analysis.Normed.Group.Defs` `Mathlib.Analysis.Normed.Group.Indicator` `Mathlib.Analysis.Normed.Group.Int` `Mathlib.Analysis.Normed.Group.Real` `Mathlib.Analysis.Normed.Group.Seminorm` `Mathlib.Analysis.Normed.Group.Subgroup` `Mathlib.Analysis.Normed.Group.Submodule` `Mathlib.Analysis.Normed.Lp.WithLp` `Mathlib.Analysis.Normed.Module.ENormedSpace` `Mathlib.Analysis.Normed.Module.MStructure` `Mathlib.Analysis.Normed.MulAction` `Mathlib.Analysis.Normed.Order.Basic` `Mathlib.Analysis.Normed.Order.Hom.Basic` `Mathlib.Analysis.Normed.Order.Hom.Ultra` `Mathlib.Analysis.Normed.Ring.Basic` `Mathlib.Analysis.Normed.Ring.Finite` `Mathlib.Analysis.Normed.Ring.TransferInstance` `Mathlib.Analysis.Normed.Ring.WithAbs` `Mathlib.Analysis.NormedSpace.Connected` `Mathlib.Analysis.NormedSpace.ENormedSpace` `Mathlib.Analysis.NormedSpace.Extr` `Mathlib.Analysis.NormedSpace.MStructure` `Mathlib.Analysis.NormedSpace.RieszLemma` `Mathlib.Analysis.Oscillation` `Mathlib.Analysis.Polynomial.CauchyBound` `Mathlib.Combinatorics.Schnirelmann` `Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic` `Mathlib.Data.ENNReal.Action` `Mathlib.Data.ENNReal.Basic` `Mathlib.Data.ENNReal.BigOperators` `Mathlib.Data.ENNReal.Holder` `Mathlib.Data.ENNReal.Inv` `Mathlib.Data.ENNReal.Lemmas` `Mathlib.Data.ENNReal.Operations` `Mathlib.Data.ENNReal.Real` `Mathlib.Data.EReal.Basic` `Mathlib.Data.EReal.Inv` `Mathlib.Data.EReal.Operations` `Mathlib.Data.Int.WithZero` `Mathlib.Data.NNReal.Basic` `Mathlib.Data.NNReal.Defs` `Mathlib.Data.NNReal.Star` `Mathlib.Data.Real.Archimedean` `Mathlib.Data.Real.ConjExponents` `Mathlib.Data.Real.ENatENNReal` `Mathlib.Data.Real.Embedding` `Mathlib.Data.Real.Pointwise` `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.Manifold.StructureGroupoid` `Mathlib.InformationTheory.Hamming` `Mathlib.LinearAlgebra.Matrix.Gershgorin` `Mathlib.MeasureTheory.OuterMeasure.Defs` `Mathlib.NumberTheory.ClassNumber.AdmissibleAbs` `Mathlib.NumberTheory.DirichletCharacter.Bounds` `Mathlib.NumberTheory.FunctionField` `Mathlib.NumberTheory.RatFunc.Ostrowski` `Mathlib.NumberTheory.SumTwoSquares` `Mathlib.NumberTheory.TsumDivsorsAntidiagonal` `Mathlib.NumberTheory.Zsqrtd.GaussianInt` `Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity` `Mathlib.Order.Filter.ENNReal` `Mathlib.RingTheory.DedekindDomain.AdicValuation` `Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing` `Mathlib.RingTheory.DedekindDomain.GaussLemma` `Mathlib.RingTheory.DedekindDomain.SInteger` `Mathlib.RingTheory.DedekindDomain.SelmerGroup` `Mathlib.RingTheory.Etale.QuasiFinite` `Mathlib.RingTheory.LaurentSeries` `Mathlib.RingTheory.LocalRing.ResidueField.Polynomial` `Mathlib.RingTheory.MvPowerSeries.GaussNorm` `Mathlib.RingTheory.OrderOfVanishing.Noetherian` `Mathlib.RingTheory.Polynomial.GaussNorm` `Mathlib.RingTheory.PowerSeries.GaussNorm` `Mathlib.RingTheory.QuasiFinite.Polynomial` `Mathlib.RingTheory.Smooth.IntegralClosure` `Mathlib.RingTheory.Unramified.LocalStructure` `Mathlib.RingTheory.Valuation.Discrete.Basic` `Mathlib.RingTheory.Valuation.ValuativeRel.Basic` `Mathlib.RingTheory.Valuation.ValuativeRel.Trivial` `Mathlib.RingTheory.ZariskisMainTheorem` `Mathlib.Topology.Algebra.MetricSpace.Lipschitz` `Mathlib.Topology.Algebra.Module.TransferInstance` `Mathlib.Topology.Algebra.Order.LiminfLimsup` `Mathlib.Topology.Algebra.Star.Real` `Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology` `Mathlib.Topology.Algebra.Valued.ValuativeRel` `Mathlib.Topology.Algebra.Valued.WithVal` `Mathlib.Topology.Bornology.Real` `Mathlib.Topology.Compactness.HilbertCubeEmbedding` `Mathlib.Topology.EMetricSpace.Basic` `Mathlib.Topology.EMetricSpace.Defs` `Mathlib.Topology.EMetricSpace.Diam` `Mathlib.Topology.EMetricSpace.Lipschitz` `Mathlib.Topology.EMetricSpace.Paracompact` `Mathlib.Topology.EMetricSpace.Pi` `Mathlib.Topology.Instances.Int` `Mathlib.Topology.Instances.Nat` `Mathlib.Topology.Instances.PNat` `Mathlib.Topology.MetricSpace.Algebra` `Mathlib.Topology.MetricSpace.Antilipschitz` `Mathlib.Topology.MetricSpace.Basic` `Mathlib.Topology.MetricSpace.Bilipschitz` `Mathlib.Topology.MetricSpace.Bounded` `Mathlib.Topology.MetricSpace.CauSeqFilter` `Mathlib.Topology.MetricSpace.Cauchy` `Mathlib.Topology.MetricSpace.Congruence` `Mathlib.Topology.MetricSpace.Defs` `Mathlib.Topology.MetricSpace.DilationEquiv` `Mathlib.Topology.MetricSpace.Dilation` `Mathlib.Topology.MetricSpace.Equicontinuity` `Mathlib.Topology.MetricSpace.Gluing` `Mathlib.Topology.MetricSpace.Infsep` `Mathlib.Topology.MetricSpace.IsometricSMul` `Mathlib.Topology.MetricSpace.Isometry` `Mathlib.Topology.MetricSpace.Lipschitz` `Mathlib.Topology.MetricSpace.MetricSeparated` `Mathlib.Topology.MetricSpace.ProperSpace.Lemmas` `Mathlib.Topology.MetricSpace.ProperSpace` `Mathlib.Topology.MetricSpace.Pseudo.Basic` `Mathlib.Topology.MetricSpace.Pseudo.Constructions` `Mathlib.Topology.MetricSpace.Pseudo.Defs` `Mathlib.Topology.MetricSpace.Pseudo.Lemmas` `Mathlib.Topology.MetricSpace.Pseudo.Pi` `Mathlib.Topology.MetricSpace.Pseudo.Real` `Mathlib.Topology.MetricSpace.Sequences` `Mathlib.Topology.MetricSpace.ShrinkingLemma` `Mathlib.Topology.MetricSpace.Similarity` `Mathlib.Topology.MetricSpace.TransferInstance` `Mathlib.Topology.MetricSpace.Ultra.Basic` `Mathlib.Topology.MetricSpace.Ultra.Pi` `Mathlib.Topology.MetricSpace.Ultra.TotallySeparated` `Mathlib.Topology.Metrizable.CompletelyMetrizable` `Mathlib.Topology.Metrizable.ContinuousMap` `Mathlib.Topology.Metrizable.Real` `Mathlib.Topology.Metrizable.Uniformity` `Mathlib.Topology.Order.Real` `Mathlib.Topology.Semicontinuous`	1
1708 files `Mathlib.Algebra.Module.ZLattice.Basic` `Mathlib.Algebra.Module.ZLattice.Covolume` `Mathlib.Algebra.Module.ZLattice.Summable` `Mathlib.Algebra.Order.Ring.StandardPart` `Mathlib.Algebra.Star.CHSH` `Mathlib.AlgebraicGeometry.EllipticCurve.LFunction` `Mathlib.AlgebraicGeometry.Sites.ElladicCohomology` `Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic` `Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup` `Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps` `Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit` `Mathlib.AlgebraicTopology.FundamentalGroupoid.Product` `Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected` `Mathlib.AlgebraicTopology.SimplicialSet.TopAdj` `Mathlib.AlgebraicTopology.SingularHomology.Basic` `Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvarianceTopCat` `Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance` `Mathlib.AlgebraicTopology.SingularSet` `Mathlib.AlgebraicTopology.TopologicalSimplex` `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.AsymptoticEquivalent` `Mathlib.Analysis.Asymptotics.Completion` `Mathlib.Analysis.Asymptotics.ExpGrowth` `Mathlib.Analysis.Asymptotics.Lemmas` `Mathlib.Analysis.Asymptotics.LinearGrowth` `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.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.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.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.Multiplier` `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.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.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.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.ProperSpace` `Mathlib.Analysis.Calculus.TangentCone.Real` `Mathlib.Analysis.Calculus.TangentCone.Seq` `Mathlib.Analysis.Calculus.TangentCone` `Mathlib.Analysis.Calculus.Taylor` `Mathlib.Analysis.Calculus.UniformLimitsDeriv` `Mathlib.Analysis.Calculus.VectorField` `Mathlib.Analysis.Complex.AbelLimit` `Mathlib.Analysis.Complex.AbsMax` `Mathlib.Analysis.Complex.Angle` `Mathlib.Analysis.Complex.Arg` `Mathlib.Analysis.Complex.Asymptotics` `Mathlib.Analysis.Complex.Basic` `Mathlib.Analysis.Complex.BorelCaratheodory` `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.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.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.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.ConstantSpeed` `Mathlib.Analysis.Convex.AmpleSet` `Mathlib.Analysis.Convex.Approximation` `Mathlib.Analysis.Convex.Birkhoff` `Mathlib.Analysis.Convex.Body` `Mathlib.Analysis.Convex.Cone.Dual` `Mathlib.Analysis.Convex.Cone.InnerDual` `Mathlib.Analysis.Convex.Cone.TensorProduct` `Mathlib.Analysis.Convex.Continuous` `Mathlib.Analysis.Convex.Contractible` `Mathlib.Analysis.Convex.Deriv` `Mathlib.Analysis.Convex.DoublyStochasticMatrix` `Mathlib.Analysis.Convex.EGauge` `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.PathConnected` `Mathlib.Analysis.Convex.Quasiconvex` `Mathlib.Analysis.Convex.Side` `Mathlib.Analysis.Convex.SpecificFunctions.Basic` `Mathlib.Analysis.Convex.SpecificFunctions.Deriv` `Mathlib.Analysis.Convex.SpecificFunctions.Pow` `Mathlib.Analysis.Convex.StdSimplex` `Mathlib.Analysis.Convex.Strict.Extreme` `Mathlib.Analysis.Convex.StrictCombination` `Mathlib.Analysis.Convex.StrictConvexBetween` `Mathlib.Analysis.Convex.StrictConvexSpace` `Mathlib.Analysis.Convex.Strong` `Mathlib.Analysis.Convex.Topology` `Mathlib.Analysis.Convex.TotallyBounded` `Mathlib.Analysis.Convex.Uniform` `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.FourierSchwartz` `Mathlib.Analysis.Distribution.SchwartzSpace.Basic` `Mathlib.Analysis.Distribution.SchwartzSpace.Deriv` `Mathlib.Analysis.Distribution.SchwartzSpace.Fourier` `Mathlib.Analysis.Distribution.SchwartzSpace` `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.PoissonSummation` `Mathlib.Analysis.Fourier.RiemannLebesgueLemma` `Mathlib.Analysis.Fourier.ZMod` `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.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.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` `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.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.Normed` `Mathlib.Analysis.Matrix.Order` `Mathlib.Analysis.Matrix.PosDef` `Mathlib.Analysis.Matrix.Spectrum` `Mathlib.Analysis.Matrix` `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.NormalForm` `Mathlib.Analysis.Meromorphic.Order` `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.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.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.Ultra` `Mathlib.Analysis.Normed.Field.UnitBall` `Mathlib.Analysis.Normed.Field.WithAbs` `Mathlib.Analysis.Normed.Group.AddCircle` `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.Rat` `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.Tannery` `Mathlib.Analysis.Normed.Group.Ultra` `Mathlib.Analysis.Normed.Group.Uniform` `Mathlib.Analysis.Normed.Group.ZeroAtInfty` `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.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.Shrink` `Mathlib.Analysis.Normed.Module.Span` `Mathlib.Analysis.Normed.Module.TransferInstance` `Mathlib.Analysis.Normed.Module.WeakDual` `Mathlib.Analysis.Normed.Operator.Asymptotics` `Mathlib.Analysis.Normed.Operator.BanachSteinhaus` `Mathlib.Analysis.Normed.Operator.Banach` `Mathlib.Analysis.Normed.Operator.Basic` `Mathlib.Analysis.Normed.Operator.Bilinear` `Mathlib.Analysis.Normed.Operator.BoundedLinearMaps` `Mathlib.Analysis.Normed.Operator.Compact` `Mathlib.Analysis.Normed.Operator.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.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.Prod` `Mathlib.Analysis.Normed.Order.Lattice` `Mathlib.Analysis.Normed.Order.UpperLower` `Mathlib.Analysis.Normed.Ring.InfiniteProd` `Mathlib.Analysis.Normed.Ring.InfiniteSum` `Mathlib.Analysis.Normed.Ring.Int` `Mathlib.Analysis.Normed.Ring.Lemmas` `Mathlib.Analysis.Normed.Ring.Ultra` `Mathlib.Analysis.Normed.Ring.Units` `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.Alternating.Basic` `Mathlib.Analysis.NormedSpace.Alternating.Curry` `Mathlib.Analysis.NormedSpace.Alternating.Uncurry.Fin` `Mathlib.Analysis.NormedSpace.HahnBanach.Extension` `Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual` `Mathlib.Analysis.NormedSpace.HahnBanach.Separation` `Mathlib.Analysis.NormedSpace.Multilinear.Basic` `Mathlib.Analysis.NormedSpace.Multilinear.Curry` `Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn` `Mathlib.Analysis.NormedSpace.Normalize` `Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm` `Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm` `Mathlib.Analysis.ODE.Basic` `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.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.Extend` `Mathlib.Analysis.RCLike.Inner` `Mathlib.Analysis.RCLike.Lemmas` `Mathlib.Analysis.RCLike.Sqrt` `Mathlib.Analysis.RCLike.TangentCone` `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.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.ExpLog` `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.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.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.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.Chebyshev` `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.Subadditive` `Mathlib.Analysis.SumIntegralComparisons` `Mathlib.Analysis.SumIntegralExpDecay` `Mathlib.Analysis.SumOverResidueClass` `Mathlib.Analysis.VonNeumannAlgebra.Basic` `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.Extremal.RuzsaSzemeredi` `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.Galois.Profinite` `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.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.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.SmoothFunctions` `Mathlib.Geometry.Manifold.Algebra.Structures` `Mathlib.Geometry.Manifold.Bordism` `Mathlib.Geometry.Manifold.BumpFunction` `Mathlib.Geometry.Manifold.ChartedSpace` `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.HasGroupoid` `Mathlib.Geometry.Manifold.Immersion` `Mathlib.Geometry.Manifold.Instances.Icc` `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.LocalInvariantProperties` `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.Basic` `Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace` `Mathlib.Geometry.Manifold.Sheaf.Smooth` `Mathlib.Geometry.Manifold.SmoothApprox` `Mathlib.Geometry.Manifold.SmoothEmbedding` `Mathlib.Geometry.Manifold.VectorBundle.Basic` `Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic` `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.KullbackLeibler.Basic` `Mathlib.InformationTheory.KullbackLeibler.ChainRule` `Mathlib.InformationTheory.KullbackLeibler.KLFun` `Mathlib.LinearAlgebra.Complex.FiniteDimensional` `Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus` `Mathlib.LinearAlgebra.Matrix.LDL` `Mathlib.LinearAlgebra.Matrix.Permutation` `Mathlib.LinearAlgebra.Matrix.Stochastic` `Mathlib.LinearAlgebra.Matrix.Swap` `Mathlib.LinearAlgebra.QuadraticForm.Complex` `Mathlib.LinearAlgebra.QuadraticForm.Real` `Mathlib.MeasureTheory.Category.MeasCat` `Mathlib.MeasureTheory.Constructions.BorelSpace.Basic` `Mathlib.MeasureTheory.Constructions.BorelSpace.Complex` `Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap` `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.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.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.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.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` `Mathlib.MeasureTheory.Integral.TorusIntegral` `Mathlib.MeasureTheory.Measure.AEDisjoint` `Mathlib.MeasureTheory.Measure.AEMeasurable` `Mathlib.MeasureTheory.Measure.AbsolutelyContinuous` `Mathlib.MeasureTheory.Measure.AddContent` `Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic` `Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion` `Mathlib.MeasureTheory.Measure.CharacteristicFunction` `Mathlib.MeasureTheory.Measure.Comap` `Mathlib.MeasureTheory.Measure.Complex` `Mathlib.MeasureTheory.Measure.Content` `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.DiracProba` `Mathlib.MeasureTheory.Measure.Dirac` `Mathlib.MeasureTheory.Measure.Doubling` `Mathlib.MeasureTheory.Measure.EverywherePos` `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.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.MutuallySingular` `Mathlib.MeasureTheory.Measure.NullMeasurable` `Mathlib.MeasureTheory.Measure.OpenPos` `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.Restrict` `Mathlib.MeasureTheory.Measure.SeparableMeasure` `Mathlib.MeasureTheory.Measure.Stieltjes` `Mathlib.MeasureTheory.Measure.SubFinite` `Mathlib.MeasureTheory.Measure.Sub` `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.NoAtoms` `Mathlib.MeasureTheory.Measure.Typeclasses.Probability` `Mathlib.MeasureTheory.Measure.Typeclasses.SFinite` `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.Variation.Basic` `Mathlib.MeasureTheory.VectorMeasure.Variation.Defs` `Mathlib.MeasureTheory.VectorMeasure.WithDensity` `Mathlib.NumberTheory.AbelSummation` `Mathlib.NumberTheory.ArithmeticFunction.Carmichael` `Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt` `Mathlib.NumberTheory.ArithmeticFunction` `Mathlib.NumberTheory.Bertrand` `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.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.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.MvPolynomial` `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.RiemannZeta` `Mathlib.NumberTheory.LSeries.SumCoeff` `Mathlib.NumberTheory.LSeries.ZMod` `Mathlib.NumberTheory.LSeries.ZetaZeros` `Mathlib.NumberTheory.LegendreSymbol.AddCharacter` `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.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.LevelOne` `Mathlib.NumberTheory.ModularForms.NormTrace` `Mathlib.NumberTheory.ModularForms.Petersson` `Mathlib.NumberTheory.ModularForms.QExpansion` `Mathlib.NumberTheory.ModularForms.SlashActions` `Mathlib.NumberTheory.ModularForms.SlashInvariantForms` `Mathlib.NumberTheory.Modular` `Mathlib.NumberTheory.MulChar.Duality` `Mathlib.NumberTheory.MulChar.Lemmas` `Mathlib.NumberTheory.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.Discriminant.Basic` `Mathlib.NumberTheory.NumberField.Discriminant.Different` `Mathlib.NumberTheory.NumberField.EquivReindex` `Mathlib.NumberTheory.NumberField.FinitePlaces` `Mathlib.NumberTheory.NumberField.House` `Mathlib.NumberTheory.NumberField.Ideal.Asymptotics` `Mathlib.NumberTheory.NumberField.Ideal.Basic` `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.MahlerBasis` `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.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.VonMangoldt` `Mathlib.NumberTheory.WellApproximable` `Mathlib.NumberTheory.ZetaValues` `Mathlib.NumberTheory.Zsqrtd.ToReal` `Mathlib.Order.Filter.ZeroAndBoundedAtFilter` `Mathlib.Probability.BorelCantelli` `Mathlib.Probability.CDF` `Mathlib.Probability.CentralLimitTheorem` `Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs` `Mathlib.Probability.CondVar` `Mathlib.Probability.ConditionalExpectation` `Mathlib.Probability.ConditionalProbability` `Mathlib.Probability.Decision.Risk.Basic` `Mathlib.Probability.Decision.Risk.Defs` `Mathlib.Probability.Density` `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.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.Kernel` `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.CondDistrib` `Mathlib.Probability.Kernel.Condexp` `Mathlib.Probability.Kernel.Defs` `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.RingTheory.DividedPowers.Padic` `Mathlib.RingTheory.HahnSeries.HahnEmbedding` `Mathlib.RingTheory.Invariant.Profinite` `Mathlib.RingTheory.LittleWedderburn` `Mathlib.RingTheory.Perfection` `Mathlib.RingTheory.Perfectoid.BDeRham` `Mathlib.RingTheory.Perfectoid.FontaineTheta` `Mathlib.RingTheory.Perfectoid.Untilt` `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.Restricted` `Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed` `Mathlib.RingTheory.RootsOfUnity.Complex` `Mathlib.RingTheory.Teichmuller` `Mathlib.RingTheory.Valuation.Discrete.RankOne` `Mathlib.RingTheory.Valuation.DiscreteValuativeRel` `Mathlib.RingTheory.Valuation.RankOne` `Mathlib.RingTheory.WittVector.Compare` `Mathlib.RingTheory.ZMod.UnitsCyclic` `Mathlib.Tactic.ComputeAsymptotics.Lemmas` `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.NormNum.Irrational` `Mathlib.Tactic.NormNum.LegendreSymbol` `Mathlib.Tactic.NormNum.RealSqrt` `Mathlib.Tactic` `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.InfiniteSum.ConditionalInt` `Mathlib.Topology.Algebra.InfiniteSum.ENNReal` `Mathlib.Topology.Algebra.InfiniteSum.Field` `Mathlib.Topology.Algebra.InfiniteSum.Real` `Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn` `Mathlib.Topology.Algebra.Module.Alternating.Topology` `Mathlib.Topology.Algebra.Module.Cardinality` `Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear` `Mathlib.Topology.Algebra.Module.FiniteDimension` `Mathlib.Topology.Algebra.Module.LocallyConvex` `Mathlib.Topology.Algebra.Module.Multilinear.Bounded` `Mathlib.Topology.Algebra.Module.Multilinear.Topology` `Mathlib.Topology.Algebra.Module.PerfectSpace` `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.StrongTopology` `Mathlib.Topology.Algebra.Module.TopDualPairing` `Mathlib.Topology.Algebra.Module.UniformConvergence` `Mathlib.Topology.Algebra.Polynomial` `Mathlib.Topology.Algebra.PontryaginDual` `Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated` `Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous` `Mathlib.Topology.Algebra.Ring.Real` `Mathlib.Topology.Algebra.Valued.LocallyCompact` `Mathlib.Topology.Algebra.Valued.NormedValued` `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.Monoidal` `Mathlib.Topology.Category.TopCat.Sphere` `Mathlib.Topology.Compactification.OnePoint.Sphere` `Mathlib.Topology.Compactness.CompactlyGeneratedSpace` `Mathlib.Topology.Compactness.DeltaGeneratedSpace` `Mathlib.Topology.Connected.LocPathConnected` `Mathlib.Topology.Connected.PathComponentOne` `Mathlib.Topology.Connected.PathConnected` `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.LocallyConvex` `Mathlib.Topology.ContinuousMap.Polynomial` `Mathlib.Topology.ContinuousMap.StarOrdered` `Mathlib.Topology.ContinuousMap.StoneWeierstrass` `Mathlib.Topology.ContinuousMap.Units` `Mathlib.Topology.ContinuousMap.Weierstrass` `Mathlib.Topology.ContinuousMap.ZeroAtInfty` `Mathlib.Topology.EMetricSpace.BoundedVariation` `Mathlib.Topology.EMetricSpace.PairReduction` `Mathlib.Topology.Homotopy.Affine` `Mathlib.Topology.Homotopy.Basic` `Mathlib.Topology.Homotopy.Contractible` `Mathlib.Topology.Homotopy.Equiv` `Mathlib.Topology.Homotopy.HSpaces` `Mathlib.Topology.Homotopy.HomotopyGroup` `Mathlib.Topology.Homotopy.Lifting` `Mathlib.Topology.Homotopy.LocallyContractible` `Mathlib.Topology.Homotopy.Path` `Mathlib.Topology.Homotopy.Product` `Mathlib.Topology.Homotopy.TopCat.Basic` `Mathlib.Topology.Homotopy.TopCat.ToSSet` `Mathlib.Topology.Instances.AddCircle.DenseSubgroup` `Mathlib.Topology.Instances.AddCircle.Real` `Mathlib.Topology.Instances.CantorSet` `Mathlib.Topology.Instances.Complex` `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.Rat` `Mathlib.Topology.Instances.Real.Lemmas` `Mathlib.Topology.Instances.RealVectorSpace` `Mathlib.Topology.Instances.ZMultiples` `Mathlib.Topology.MetricSpace.CantorScheme` `Mathlib.Topology.MetricSpace.Closeds` `Mathlib.Topology.MetricSpace.Completion` `Mathlib.Topology.MetricSpace.Contracting` `Mathlib.Topology.MetricSpace.Cover` `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.ProperSpace.Real` `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.Category.FrameAdjunction` `Mathlib.Topology.PartitionOfUnity` `Mathlib.Topology.Path` `Mathlib.Topology.Semicontinuity.Basic` `Mathlib.Topology.Semicontinuity.Lindelof` `Mathlib.Topology.Separation.CompletelyRegular` `Mathlib.Topology.Separation.Lemmas` `Mathlib.Topology.Sion` `Mathlib.Topology.Subpath` `Mathlib.Topology.TietzeExtension` `Mathlib.Topology.UniformSpace.CompareReals` `Mathlib.Topology.UniformSpace.Dini` `Mathlib.Topology.UniformSpace.Path` `Mathlib.Topology.UniformSpace.Real` `Mathlib.Topology.UniformSpace.Uniformizable` `Mathlib.Topology.UnitInterval` `Mathlib.Topology.UrysohnsBounded` `Mathlib.Topology.UrysohnsLemma` `Mathlib.Topology.VectorBundle.Basic` `Mathlib.Topology.VectorBundle.Constructions` `Mathlib.Topology.VectorBundle.FiniteDimensional` `Mathlib.Topology.VectorBundle.Hom` `Mathlib.Topology.VectorBundle.Riemannian`	2
`Mathlib.Data.Real.Cauchy` (new file)	691

Declarations diff

+ add
+ inf
+ instance : Add ℝ := ⟨Real.add⟩
+ instance : Inv ℝ := ⟨Real.inv⟩
+ instance : LE ℝ := ⟨Real.le⟩
+ instance : LT ℝ := ⟨Real.lt⟩
+ instance : Max ℝ := ⟨Real.sup⟩
+ instance : Min ℝ := ⟨Real.inf⟩
+ instance : Mul ℝ := ⟨Real.mul⟩
+ instance : Neg ℝ := ⟨Real.neg⟩
+ instance : One ℝ := ⟨Real.one⟩
+ instance : Sub ℝ := ⟨fun a b ↦ a + (-b)⟩
+ instance : Zero ℝ := ⟨Real.zero⟩
+ inv
+ le
+ lt
+ mul
+ neg
+ one
+ ratCast
+ sub_def
+ sup
+ zero
- instance : Add ℝ
- instance : Inv ℝ
- instance : LE ℝ
- instance : LT ℝ
- instance : Max ℝ
- instance : Min ℝ
- instance : Mul ℝ
- instance : Neg ℝ
- instance : One ℝ
- instance : Sub ℝ
- instance : Zero ℝ
- lt_cauchy
- ofCauchy_inf
- ofCauchy_sup
- ofRat_rat

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.

Decrease in strong tech debt: (relative, absolute) = (3.84, 0.05)

Current number	Change	Type
129	1	adaptation notes
6176	-1	backward.isDefEq.respectTransparency
738	-20	backward.privateInPublic
384	-10	backward.privateInPublic.warn

Current commit c390d8eab8
Reference commit 1804a9da0a

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.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
- The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Decrease in weak tech debt: (relative, absolute) = (3.84, 0.05)

Current number	Change	Type
129	1	adaptation notes
6176	-1	backward.isDefEq.respectTransparency
738	-20	backward.privateInPublic
384	-10	backward.privateInPublic.warn

Current commit c390d8eab8
Reference commit 1804a9da0a

riccardobrasca · 2026-04-29T10:02:51Z

!radar

leanprover-radar · 2026-04-29T10:03:15Z

Benchmark results for 4d4cf30 against 1804a9d are in. There are significant results. @jcommelin @riccardobrasca

🟥 main exited with code 1

No significant changes detected.

fpvandoorn

Code changes LGTM.

bors d+

Please merge only after running !radar and the results look decent/good.

mathlib-bors · 2026-04-29T12:14:42Z

✌️ jcommelin can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

sgouezel · 2026-04-29T13:40:12Z

Can you explain why you go from a one-type structure to a type synonym? I see that the definition is not exposed, so in theory this shoudn't make any difference, but it's not clear to me if that really hides the definition from the kernel or only from all the tactics.

jcommelin · 2026-04-29T13:49:36Z

@sgouezel My understanding is that it is completely hidden from the kernel, unless import all is used in a downstream module.

Under that assumption, I think the current approach is shorter, easier to read, and hence preferable.

eric-wieser · 2026-04-29T14:17:30Z

!bench

leanprover-radar · 2026-04-29T14:17:57Z

Benchmark results for 513b76c against 1804a9d are in. There are significant results. @eric-wieser

✅ build//instructions: -82.0G (-0.05%)

Large changes (1✅)

✅ build/module/Mathlib.NumberTheory.Padics.Hensel//instructions: -35.4G (-40.18%)

Medium changes (1✅)

✅ build/module/Mathlib.Combinatorics.Additive.ApproximateSubgroup//instructions: -1.4G (-5.78%)

Small changes (5✅, 2🟥)

✅ build/module/Mathlib.Combinatorics.Additive.CovBySMul//instructions: -532.6M (-6.19%)
🟥 build/module/Mathlib.Combinatorics.Quiver.Path.Decomposition//instructions: +401.8M (+7.22%)
✅ build/module/Mathlib.Data.Real.Basic//instructions: -1.9G (-8.31%) (reduced significance based on *//lines)
✅ build/module/Mathlib.NumberTheory.Harmonic.GammaDeriv//instructions: -1.0G (-2.89%)
✅ build/module/Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Def//instructions: -266.7M (-3.70%)
🟥 build/module/Mathlib.Tactic.Attr.Core//instructions: +407.2M (+16.97%)
✅ build/module/Mathlib.Topology.Instances.Rat//instructions: -1.1G (-9.49%)

eric-wieser · 2026-04-29T14:18:40Z

unless import all is used in a downstream module.

I know this will be rare, but we should consider these users too. The one field structure is far more robust when it comes to avoiding bad unfolding and typeclass issues.

jcommelin · 2026-04-29T14:26:43Z

I think people should only need to use import all if they actually want such unfolding to happen.

eric-wieser · 2026-04-29T18:59:27Z

I don't think anyone ever wants accidental unfolding. The status quo of having to opt into this unfolding with cases and ext is a big improvement over a type synonym. I think it's reasonable to have to opt in with both import all and cases/ext, but I don't think we should discard the clean interface that we had before.

JovanGerb · 2026-04-30T12:23:31Z

It is quite common for beginners to not use the module system. This is equivalent to using import all for all imports. And the simpNF linter also doesn't participate in the module system, so it also sees everything with import all.

By the way, I also made the smaller #38198 for Real.

YaelDillies · 2026-05-01T07:05:14Z

 numbers are represented.
 -/
-unsafe instance instRepr : Repr ℂ where
+unsafe instance instRepr [Repr ℝ] : Repr ℂ where


What's happening here?

The Repr instance for Real depends on the implementation details of Real, and has therefore moved to a separate file. It is no longer available by simply importing Real.Basic.
We could move all of these Repr instances to separate files, but this seemed like a more modular solution to me.

jcommelin · 2026-05-04T04:41:48Z

the simpNF linter also doesn't participate in the module system, so it also sees everything with import all.

@JovanGerb I think this is a blocker for future encapsulation work in Mathlib. Do you know how to fix the linter, so that it does participate in the module system?

jcommelin · 2026-05-04T04:43:38Z

@eric-wieser I'm not strongly attached to my approach. I will however note that all the irreducible_defs in the old code had set_option backward.* in front of them... do we want to revert those back in?

JovanGerb · 2026-05-04T08:49:39Z

https://leanprover.zulipchat.com/#narrow/channel/348111-batteries/topic/Environment.20linters.20upstreamed.20to.20core.3F/near/590294602

I asked about environment linters participating in the module system here, but have had no response.

I recall though that when I tried to put simpNF on the module system there were a few errors due to declarations being invalid in the exposed setting. I'm not sure whether this has been fixed already.

wkrozowski · 2026-05-05T09:00:27Z

@JovanGerb - so currently the builtin support for the environment linters mimics the way it is done in batteries. We grab default targets roots from the workspace, iterate through each module in target roots, import it along the environment linters module and run the linters on all declarations.

Is this what you mean or would you like it to be more localised?

JovanGerb · 2026-05-05T09:24:07Z

When you say "import it", this can mean multiple things. There are 3 levels at which you can import things:

You can import everything. This corresponds to import all, or to not using the module system
You can import public data and language server data. This includes doc-strings.
You can import only public data. This excludes doc-strings.

I propose that simpNF should be run with setting (2) or (3). But currently all linters are run with setting (1).

On the other hand, docBlame needs (1) or (2), and unusedHavesSuffices needs (1) (Though arguably, if it needs (1), then it should be a syntax linter and not an environment linter).

wkrozowski · 2026-05-06T10:57:55Z

I see - so in terms of builtin env framework your proposal would be to add an option for an environment linter to be run in a setting, where the imports behave like (3), right?

JovanGerb · 2026-05-06T11:18:13Z

Yes. And I think that at some point this should become the default setting. Because I would argue that anything that needs (1) or (2) should not be an env_linter in the first place. Another example of this is unusedArguments, which would be a lot more convenient if it warned you immediately, rather than in CI.

jcommelin · 2026-05-06T19:05:17Z

The new build failures are absolutely mysterious to me...

Kha · 2026-05-06T19:11:33Z

Uh oh, encapsulation through structures may not be as tested as I thought

Kha · 2026-05-07T12:48:39Z

PSA (while I'm looking into the structure failure): leanprover/lean4#13646 proposes a new Lake option that Mathlib could use to encourage downstream users to adopt the module system

Mark 13 internal-only helper definitions in Mathlib/Tactic/Translate/Core.lean as `private`. None are referenced from outside the file. The change is mechanical (`def → private def`); two declarations are line-wrapped to keep the 100-char style budget after the keyword is added. The privatized declarations: findPrefixTranslation? etaExpandN updateAndAddDecl declUnfoldSimpAuxLemmas findTargetName findAuxDecls copyInstanceAttribute warnAttr warnParametricAttr translateLemmas targetName checkExistingType proceedFields The file already had `private def` precedent (`RelevantArg.min` line 177, `realizeGlobalConst` line 241), so the pattern is established here. Motivation — build-cache hygiene. In Lean 4.10's separated artifact pair, edits to a `private` declaration's body do not move the public interface hash, so downstream modules cache-hit across body edits to these helpers. This is the same lever PR leanprover-community#38702 used to encapsulate Real number plumbing. Empirically demonstrated on this branch: an in-place same-length edit inside the private body of `etaExpandN` (one word swapped in a string literal) left `Translate.Core.olean.server.hash` byte-identical, and downstream `Translate.ToAdditive.olean.hash` and `Translate.ToDual.olean.hash` were both byte-identical (`lake build` of either returned in 400ms with manifest verification only, no re-elaboration). Validation: - `lake build Mathlib.Tactic.Translate.Core` — passes - `lake build Mathlib.Tactic.Translate.ToAdditive` — passes - `lake build Mathlib.Tactic.Translate.ToDual` — passes - `lake build Mathlib` — full mathlib build passes (8,386 modules, 0 errors) A 14th candidate (`elabTranslationAttr`) was identified by static reference scanning but reverted after the build verifier flagged two cross-module uses inside `initialize { add := fun ... ↦ ... }` blocks in ToAdditive.lean and ToDual.lean. So `elabTranslationAttr` stays public. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Final retained: 2 @[no_expose] annotations on internal qNF.add and qNF.mkAddProof meta defs in Mathlib/Tactic/Module.lean. Bulk pipeline run: - Seed: top-100 tier-3 hubs by score (~75 unique modules) - Initial apply: 2,726 decls (1,121 private + 1,605 @[no_expose]) - Revert iterations: 18 (cumulative reverts 2,615) - After auto-iterate stuck on cross-file cascades that no error message pinpointed (Type mismatch / Function expected / Invalid simp theorem in downstream-consumer files, with the culprit upstream in 5 hot files), I wholesale-reverted those 5 files manually - Verified locally with full 'lake build' (8,395 jobs green) The 5 hot files where retained edits caused downstream cascades: - Mathlib/Topology/UniformSpace/Equicontinuity.lean (38 entries) - Mathlib/GroupTheory/Perm/Fin.lean (28 entries) - Mathlib/AlgebraicGeometry/PullbackCarrier.lean (23 entries) - Mathlib/Tactic/FieldSimp.lean (13 entries) - Mathlib/Geometry/RingedSpace/LocallyRingedSpace/ResidueField.lean (7) What made these stuck: their internal helpers were referenced via dot-method dispatch / typeclass projection / simp-rewrite in downstream files. The revert script can't pinpoint the upstream culprit when the error site is downstream and the message is semantic (no constant name in the error). The Module.lean retentions survived because they're 'meta def' in a 'public meta section' — compile-time code with no downstream type-elaboration users. Specifically: @[no_expose] meta def qNF.add @[no_expose] meta def qNF.mkAddProof This is the bulk-pipeline analog of mathlib4 PR leanprover-community#38702 but with the new module system's @[no_expose] tool. The yield (2/2726 = 0.07%) reflects that K=100 is too aggressive for the all-at-once iterate mode: a per-file isolation mode (apply to one file, build, keep iff passes) would produce more retention because per-decl effects could be tested independently. See docs/bulk-no-expose.md in https://github.com/marcelolynch/mathlib-hide-decls for the experiment design. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

chore(Data/Real): encapsulate real numbers

2a0cf15

jcommelin commented Apr 29, 2026

View reviewed changes

Comment thread Mathlib/Analysis/Complex/Norm.lean Outdated

jcommelin added 2 commits April 29, 2026 11:55

wip

046a343

wip

4d4cf30

jcommelin added 3 commits April 29, 2026 13:34

wip

5084f74

docstrings

5d7aa43

why does the linter trigger here, now?

ae5e6fa

fpvandoorn approved these changes Apr 29, 2026

View reviewed changes

mathlib-triage Bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Apr 29, 2026

wip

97c0629

remove simp attribute

7ab1408

fix tests

513b76c

eric-wieser reviewed Apr 29, 2026

View reviewed changes

Comment thread Mathlib/Data/Real/Basic.lean

eric-wieser reviewed Apr 29, 2026

View reviewed changes

Comment thread Mathlib/Data/Real/Cauchy.lean Outdated

YaelDillies reviewed May 1, 2026

View reviewed changes

jcommelin added 2 commits May 6, 2026 20:39

one field structure

7f04150

fix docstring

c390d8e

Conversation

jcommelin commented Apr 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

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

Uh oh!

PR summary 1804a9da0a

Import changes for modified files

Declarations diff

Uh oh!

riccardobrasca commented Apr 29, 2026

Uh oh!

leanprover-radar commented Apr 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

fpvandoorn left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors Bot commented Apr 29, 2026

Uh oh!

sgouezel commented Apr 29, 2026

Uh oh!

jcommelin commented Apr 29, 2026

Uh oh!

Uh oh!

eric-wieser commented Apr 29, 2026

Uh oh!

leanprover-radar commented Apr 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

eric-wieser commented Apr 29, 2026

Uh oh!

jcommelin commented Apr 29, 2026

Uh oh!

eric-wieser commented Apr 29, 2026

Uh oh!

Uh oh!

JovanGerb commented Apr 30, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

YaelDillies May 1, 2026

Choose a reason for hiding this comment

Uh oh!

jcommelin May 4, 2026

Choose a reason for hiding this comment

Uh oh!

jcommelin commented May 4, 2026

Uh oh!

jcommelin commented May 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

JovanGerb commented May 4, 2026

Uh oh!

wkrozowski commented May 5, 2026

Uh oh!

JovanGerb commented May 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

wkrozowski commented May 6, 2026

Uh oh!

JovanGerb commented May 6, 2026

Uh oh!

jcommelin commented May 6, 2026

Uh oh!

Kha commented May 6, 2026

Uh oh!

Kha commented May 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

10 participants

jcommelin commented Apr 29, 2026 •

edited

Loading

github-actions Bot commented Apr 29, 2026 •

edited

Loading

leanprover-radar commented Apr 29, 2026 •

edited

Loading

leanprover-radar commented Apr 29, 2026 •

edited

Loading

JovanGerb commented Apr 30, 2026 •

edited

Loading

jcommelin commented May 4, 2026 •

edited

Loading

JovanGerb commented May 5, 2026 •

edited

Loading