Skip to content

[Merged by Bors] - feat(Topology/Algebra): use Is*Apply for ContinuousLinearMap#39637

Closed
mcdoll wants to merge 37 commits into
leanprover-community:masterfrom
mcdoll:IsApplyCLM
Closed

[Merged by Bors] - feat(Topology/Algebra): use Is*Apply for ContinuousLinearMap#39637
mcdoll wants to merge 37 commits into
leanprover-community:masterfrom
mcdoll:IsApplyCLM

Conversation

@mcdoll

@mcdoll mcdoll commented May 21, 2026 •
edited
Loading

Copy link
Copy Markdown
Member

This is the first in many PRs that use the new Is*Apply classes instead of structure specific foo_apply lemmas.
The main bulk of the PR is in Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean, everything else is just fixing errors.

For each foo in zero, one, add, sub, neg, smul` we do the following:

  • add an instance IsFooApply
  • rename coe_foo to toLinearMap_foo
  • depreprecate coe_foo, coe_foo', and foo_apply

We are rather conservative when it comes to the instances, in future PRs this will be used more.

For consistency, the same renaming has been applied to the comp variants. This resulted in a test being changed.

Note to maintainers: please don't put multiple PRs regarding Is*Apply on the queue, they will most likely create merge conflicts.

About the test: I don't understand what the test is really for. all of the changed proofs are still true by rfl and norm_cast.

Open in Gitpod

@github-actions github-actions Bot added the t-topology Topological spaces, uniform spaces, metric spaces, filters label May 21, 2026
@github-actions

github-actions Bot commented May 21, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary 3df4a86029

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic 1225 1228 +3 (+0.24%)
Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent 1226 1229 +3 (+0.24%)
Mathlib.Topology.Algebra.Module.Equiv 1228 1231 +3 (+0.24%)
Mathlib.Topology.Algebra.Module.Multilinear.Basic 1238 1241 +3 (+0.24%)
Mathlib.Analysis.Convex.Exposed 1273 1276 +3 (+0.24%)
Mathlib.Analysis.Normed.Group.SeparationQuotient 1380 1383 +3 (+0.22%)
Mathlib.MeasureTheory.Measure.Typeclasses.Finite 1507 1510 +3 (+0.20%)
Mathlib.NumberTheory.Padics.PadicNumbers 1510 1513 +3 (+0.20%)
Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn 1518 1521 +3 (+0.20%)
Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan 1524 1527 +3 (+0.20%)
Mathlib.LinearAlgebra.Eigenspace.ContinuousLinearMap 1526 1529 +3 (+0.20%)
Mathlib.MeasureTheory.Integral.Lebesgue.Basic 1526 1529 +3 (+0.20%)
Mathlib.Algebra.Category.ModuleCat.Topology.Basic 1527 1530 +3 (+0.20%)
Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM 1538 1541 +3 (+0.20%)
Mathlib.Analysis.Normed.Operator.Compact.Basic 1541 1544 +3 (+0.19%)
Mathlib.Algebra.Category.ModuleCat.Topology.Homology 1569 1572 +3 (+0.19%)
Mathlib.MeasureTheory.Group.Prod 1647 1650 +3 (+0.18%)
Mathlib.Analysis.Normed.Operator.Bilinear 1660 1663 +3 (+0.18%)
Mathlib.Analysis.Normed.Module.Multilinear.Basic 1671 1674 +3 (+0.18%)
Mathlib.Analysis.Calculus.FormalMultilinearSeries 1678 1681 +3 (+0.18%)
Mathlib.Analysis.Calculus.FDeriv.Comp 1680 1683 +3 (+0.18%)
Mathlib.Analysis.Calculus.Deriv.Basic 1684 1687 +3 (+0.18%)
Mathlib.Topology.VectorBundle.Basic 1737 1740 +3 (+0.17%)
Mathlib.Analysis.Calculus.FDeriv.Add 1745 1748 +3 (+0.17%)
Mathlib.Analysis.Calculus.Deriv.Add 1748 1751 +3 (+0.17%)
Mathlib.Analysis.CStarAlgebra.Unitization 1775 1778 +3 (+0.17%)
Mathlib.Analysis.Calculus.FDeriv.Analytic 1780 1783 +3 (+0.17%)
Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno 1782 1785 +3 (+0.17%)
Mathlib.Analysis.Calculus.ContDiff.Basic 1785 1788 +3 (+0.17%)
Mathlib.Analysis.Calculus.Deriv.Mul 1796 1799 +3 (+0.17%)
Mathlib.Analysis.Calculus.Deriv.CompMul 1797 1800 +3 (+0.17%)
Mathlib.Analysis.Calculus.Darboux 1799 1802 +3 (+0.17%)
Mathlib.Analysis.Calculus.ContDiff.Operations 1807 1810 +3 (+0.17%)
Mathlib.Analysis.Analytic.IteratedFDeriv 1809 1812 +3 (+0.17%)
Mathlib.Analysis.Calculus.AbsolutelyMonotone 1817 1820 +3 (+0.17%)
Mathlib.Analysis.Calculus.ContDiff.Bounds 1827 1830 +3 (+0.16%)
Mathlib.Analysis.InnerProductSpace.LinearMap 1830 1833 +3 (+0.16%)
Mathlib.Analysis.InnerProductSpace.ConformalLinearMap 1832 1835 +3 (+0.16%)
Mathlib.Topology.VectorBundle.Riemannian 1842 1845 +3 (+0.16%)
Mathlib.Analysis.CStarAlgebra.Multiplier 1873 1876 +3 (+0.16%)
Mathlib.Analysis.Calculus.UniformLimitsDeriv 1874 1877 +3 (+0.16%)
Mathlib.Analysis.SpecialFunctions.Exponential 1881 1884 +3 (+0.16%)
Mathlib.Analysis.Normed.Unbundled.FiniteExtension 1883 1886 +3 (+0.16%)
Mathlib.Analysis.Calculus.FDeriv.Symmetric 1887 1890 +3 (+0.16%)
Mathlib.Analysis.Calculus.VectorField 1888 1891 +3 (+0.16%)
Mathlib.Topology.ContinuousMap.StoneWeierstrass 1891 1894 +3 (+0.16%)
Mathlib.NumberTheory.ModularForms.CongruenceSubgroups 1983 1986 +3 (+0.15%)
Mathlib.Analysis.Normed.Module.Bases 2047 2050 +3 (+0.15%)
Mathlib.Analysis.Normed.Module.ContinuousInverse 2049 2052 +3 (+0.15%)
Mathlib.Analysis.LocallyConvex.Separation 2052 2055 +3 (+0.15%)
Mathlib.Analysis.SpecialFunctions.Pow.Deriv 2054 2057 +3 (+0.15%)
Mathlib.NumberTheory.Modular 2077 2080 +3 (+0.14%)
Mathlib.Analysis.Calculus.Implicit 2081 2084 +3 (+0.14%)
Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain 2082 2085 +3 (+0.14%)
Mathlib.Analysis.InnerProductSpace.Projection.Basic 2119 2122 +3 (+0.14%)
Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional 2123 2126 +3 (+0.14%)
Mathlib.Analysis.Complex.Conformal 2142 2145 +3 (+0.14%)
Mathlib.Analysis.InnerProductSpace.PiL2 2162 2165 +3 (+0.14%)
Mathlib.Analysis.InnerProductSpace.Dual 2165 2168 +3 (+0.14%)
Mathlib.NumberTheory.SiegelsLemma 2166 2169 +3 (+0.14%)
Mathlib.Analysis.InnerProductSpace.Adjoint 2175 2178 +3 (+0.14%)
Mathlib.Analysis.Convex.DoublyStochasticMatrix 2183 2186 +3 (+0.14%)
Mathlib.Geometry.Manifold.IntegralCurve.Basic 2194 2197 +3 (+0.14%)
Mathlib.Geometry.Manifold.IntegralCurve.Transform 2195 2198 +3 (+0.14%)
Mathlib.Geometry.Manifold.VectorField.LieBracket 2220 2223 +3 (+0.14%)
Mathlib.Analysis.Calculus.FDeriv.Norm 2243 2246 +3 (+0.13%)
Mathlib.MeasureTheory.Integral.FinMeasAdditive 2267 2270 +3 (+0.13%)
Mathlib.MeasureTheory.Integral.Bochner.L1 2271 2274 +3 (+0.13%)
Mathlib.Geometry.Manifold.Instances.Icc 2279 2282 +3 (+0.13%)
Mathlib.Analysis.Convex.Birkhoff 2283 2286 +3 (+0.13%)
Mathlib.Geometry.Manifold.Instances.Sphere 2316 2319 +3 (+0.13%)
Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic 2352 2355 +3 (+0.13%)
Mathlib.Analysis.Convolution 2358 2361 +3 (+0.13%)
Mathlib.MeasureTheory.Measure.Haar.DistribChar 2366 2369 +3 (+0.13%)
Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar 2366 2369 +3 (+0.13%)
Mathlib.Analysis.Distribution.ContDiffMapSupportedIn 2367 2370 +3 (+0.13%)
Mathlib.Analysis.Fourier.FourierTransform 2369 2372 +3 (+0.13%)
Mathlib.MeasureTheory.Function.Jacobian 2373 2376 +3 (+0.13%)
Mathlib.Probability.Distributions.Uniform 2377 2380 +3 (+0.13%)
Mathlib.Geometry.Euclidean.Volume.Measure 2385 2388 +3 (+0.13%)
Mathlib.Analysis.InnerProductSpace.Rayleigh 2387 2390 +3 (+0.13%)
Mathlib.Analysis.InnerProductSpace.Trace 2405 2408 +3 (+0.12%)
Mathlib.MeasureTheory.Function.JacobianOneDim 2433 2436 +3 (+0.12%)
Mathlib.Analysis.InnerProductSpace.Positive 2485 2488 +3 (+0.12%)
Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv 2486 2489 +3 (+0.12%)
Mathlib.Analysis.InnerProductSpace.Reproducing 2487 2490 +3 (+0.12%)
Mathlib.Analysis.Complex.CauchyIntegral 2518 2521 +3 (+0.12%)
Mathlib.Geometry.Manifold.Riemannian.PathELength 2531 2534 +3 (+0.12%)
Mathlib.Analysis.Complex.Harmonic.Analytic 2538 2541 +3 (+0.12%)
Mathlib.Geometry.Manifold.WhitneyEmbedding 2541 2544 +3 (+0.12%)
Mathlib.Analysis.Analytic.Binomial 2549 2552 +3 (+0.12%)
Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic 2578 2581 +3 (+0.12%)
Mathlib.Probability.Moments.Variance 2696 2699 +3 (+0.11%)
Mathlib.Probability.Moments.Basic 2702 2705 +3 (+0.11%)
Mathlib.Probability.StrongLaw 2707 2710 +3 (+0.11%)
Mathlib.Analysis.CStarAlgebra.CStarMatrix 2734 2737 +3 (+0.11%)
Mathlib.Analysis.Fourier.FourierTransformDeriv 2782 2785 +3 (+0.11%)
Mathlib.Analysis.InnerProductSpace.StarOrder 2783 2786 +3 (+0.11%)
Mathlib.Analysis.Distribution.SchwartzSpace.Deriv 2820 2823 +3 (+0.11%)
Mathlib.Probability.Distributions.Gaussian.Basic 2889 2892 +3 (+0.10%)
Mathlib.Probability.Distributions.Gaussian.Fernique 2892 2895 +3 (+0.10%)
Mathlib.Analysis.Distribution.FourierMultiplier 2903 2906 +3 (+0.10%)
Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable 2903 2906 +3 (+0.10%)
Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence 2906 2909 +3 (+0.10%)
Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence 2913 2916 +3 (+0.10%)
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic 3016 3019 +3 (+0.10%)
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne 3099 3102 +3 (+0.10%)
Import changes for all files
Files Import difference
1837 files Mathlib.Algebra.Category.ContinuousCohomology.Basic Mathlib.Algebra.Category.ModuleCat.Topology.Basic Mathlib.Algebra.Category.ModuleCat.Topology.Homology Mathlib.Algebra.Module.ZLattice.Basic Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.Algebra.Module.ZLattice.Summable Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.AffineTransitionLimit Mathlib.AlgebraicGeometry.AlgClosed.Basic Mathlib.AlgebraicGeometry.Artinian Mathlib.AlgebraicGeometry.Birational.Dominant Mathlib.AlgebraicGeometry.Birational.RationalMap Mathlib.AlgebraicGeometry.ColimitsOver Mathlib.AlgebraicGeometry.Cover.Directed Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.Cover.QuasiCompact Mathlib.AlgebraicGeometry.Cover.Sigma Mathlib.AlgebraicGeometry.EffectiveEpi Mathlib.AlgebraicGeometry.EllipticCurve.LFunction Mathlib.AlgebraicGeometry.EllipticCurve.Reduction Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.Geometrically.Basic Mathlib.AlgebraicGeometry.Geometrically.Connected Mathlib.AlgebraicGeometry.Geometrically.Integral Mathlib.AlgebraicGeometry.Geometrically.Irreducible Mathlib.AlgebraicGeometry.Geometrically.Reduced Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Group.Abelian Mathlib.AlgebraicGeometry.Group.Smooth Mathlib.AlgebraicGeometry.IdealSheaf.Basic Mathlib.AlgebraicGeometry.IdealSheaf.Functorial Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme Mathlib.AlgebraicGeometry.LimitsOver Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.AlgebraicGeometry.Morphisms.AffineAnd Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.Morphisms.Descent Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.AlgebraicGeometry.Morphisms.FlatDescent Mathlib.AlgebraicGeometry.Morphisms.FlatMono Mathlib.AlgebraicGeometry.Morphisms.FlatRank Mathlib.AlgebraicGeometry.Morphisms.Flat Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Morphisms.LocalClosure Mathlib.AlgebraicGeometry.Morphisms.LocalFlatDescent Mathlib.AlgebraicGeometry.Morphisms.LocalIso Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Normalization Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.QuasiAffine Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.RelativeGluing Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Sites.AffineEtale Mathlib.AlgebraicGeometry.Sites.Affine Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.ConstantSheaf Mathlib.AlgebraicGeometry.Sites.ElladicCohomology Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.Fpqc Mathlib.AlgebraicGeometry.Sites.Pretopology Mathlib.AlgebraicGeometry.Sites.Proetale Mathlib.AlgebraicGeometry.Sites.QuasiCompact Mathlib.AlgebraicGeometry.Sites.Representability Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.Stalk Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.AlgebraicGeometry.ZariskisMainTheorem Mathlib.Analysis.AbsoluteValue.Equivalence Mathlib.Analysis.Analytic.Basic Mathlib.Analysis.Analytic.Binomial Mathlib.Analysis.Analytic.CPolynomialDef Mathlib.Analysis.Analytic.CPolynomial Mathlib.Analysis.Analytic.ChangeOrigin Mathlib.Analysis.Analytic.Composition Mathlib.Analysis.Analytic.Constructions Mathlib.Analysis.Analytic.ConvergenceRadius Mathlib.Analysis.Analytic.Inverse Mathlib.Analysis.Analytic.IsolatedZeros Mathlib.Analysis.Analytic.IteratedFDeriv Mathlib.Analysis.Analytic.Linear Mathlib.Analysis.Analytic.OfScalars Mathlib.Analysis.Analytic.Order Mathlib.Analysis.Analytic.Polynomial Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.Analysis.Analytic.Uniqueness Mathlib.Analysis.Analytic.WithLp Mathlib.Analysis.Analytic.Within Mathlib.Analysis.AperiodicOrder.Delone.Basic Mathlib.Analysis.Asymptotics.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.Extreme Mathlib.Analysis.CStarAlgebra.Fuglede Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.CStarAlgebra.Module.Synonym Mathlib.Analysis.CStarAlgebra.Multiplier Mathlib.Analysis.CStarAlgebra.PositiveLinearMap Mathlib.Analysis.CStarAlgebra.Projection Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Analysis.CStarAlgebra.Unitary.Connected Mathlib.Analysis.CStarAlgebra.Unitary.Maps Mathlib.Analysis.CStarAlgebra.Unitary.Span Mathlib.Analysis.CStarAlgebra.Unitization Mathlib.Analysis.CStarAlgebra.lpSpace Mathlib.Analysis.Calculus.AbsolutelyMonotone Mathlib.Analysis.Calculus.AddTorsor.AffineMap Mathlib.Analysis.Calculus.AddTorsor.Coord Mathlib.Analysis.Calculus.BumpFunction.Basic Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox Mathlib.Analysis.Calculus.Conformal.InnerProduct Mathlib.Analysis.Calculus.Conformal.NormedSpace Mathlib.Analysis.Calculus.ContDiff.Basic Mathlib.Analysis.Calculus.ContDiff.Bounds Mathlib.Analysis.Calculus.ContDiff.CPolynomial Mathlib.Analysis.Calculus.ContDiff.Comp Mathlib.Analysis.Calculus.ContDiff.Convolution Mathlib.Analysis.Calculus.ContDiff.Defs Mathlib.Analysis.Calculus.ContDiff.Deriv Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno Mathlib.Analysis.Calculus.ContDiff.FiniteDimension Mathlib.Analysis.Calculus.ContDiff.Operations Mathlib.Analysis.Calculus.ContDiff.Polynomial Mathlib.Analysis.Calculus.ContDiff.RCLike Mathlib.Analysis.Calculus.ContDiff.RestrictScalars Mathlib.Analysis.Calculus.ContDiff.WithLp Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise Mathlib.Analysis.Calculus.DSlope Mathlib.Analysis.Calculus.Darboux Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.Calculus.Deriv.Add Mathlib.Analysis.Calculus.Deriv.AffineMap Mathlib.Analysis.Calculus.Deriv.Basic Mathlib.Analysis.Calculus.Deriv.CompMul Mathlib.Analysis.Calculus.Deriv.Comp Mathlib.Analysis.Calculus.Deriv.Inv Mathlib.Analysis.Calculus.Deriv.Inverse Mathlib.Analysis.Calculus.Deriv.Linear Mathlib.Analysis.Calculus.Deriv.MeanValue Mathlib.Analysis.Calculus.Deriv.Mul Mathlib.Analysis.Calculus.Deriv.Pi Mathlib.Analysis.Calculus.Deriv.Polynomial Mathlib.Analysis.Calculus.Deriv.Pow Mathlib.Analysis.Calculus.Deriv.Prod Mathlib.Analysis.Calculus.Deriv.Shift Mathlib.Analysis.Calculus.Deriv.Slope Mathlib.Analysis.Calculus.Deriv.Star Mathlib.Analysis.Calculus.Deriv.Support Mathlib.Analysis.Calculus.Deriv.ZPow Mathlib.Analysis.Calculus.DerivativeTest Mathlib.Analysis.Calculus.DiffContOnCl Mathlib.Analysis.Calculus.DifferentialForm.Basic Mathlib.Analysis.Calculus.DifferentialForm.VectorField Mathlib.Analysis.Calculus.FDeriv.Add Mathlib.Analysis.Calculus.FDeriv.Affine Mathlib.Analysis.Calculus.FDeriv.Analytic Mathlib.Analysis.Calculus.FDeriv.Basic Mathlib.Analysis.Calculus.FDeriv.Bilinear Mathlib.Analysis.Calculus.FDeriv.CompCLM Mathlib.Analysis.Calculus.FDeriv.Comp Mathlib.Analysis.Calculus.FDeriv.Congr Mathlib.Analysis.Calculus.FDeriv.Const Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap Mathlib.Analysis.Calculus.FDeriv.ContinuousMultilinearMap Mathlib.Analysis.Calculus.FDeriv.Defs Mathlib.Analysis.Calculus.FDeriv.Equiv Mathlib.Analysis.Calculus.FDeriv.Extend Mathlib.Analysis.Calculus.FDeriv.Linear Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.Analysis.Calculus.FDeriv.Mul Mathlib.Analysis.Calculus.FDeriv.Norm Mathlib.Analysis.Calculus.FDeriv.OfCompLeft Mathlib.Analysis.Calculus.FDeriv.Partial Mathlib.Analysis.Calculus.FDeriv.Pi Mathlib.Analysis.Calculus.FDeriv.Pow Mathlib.Analysis.Calculus.FDeriv.Prod Mathlib.Analysis.Calculus.FDeriv.RestrictScalars Mathlib.Analysis.Calculus.FDeriv.Star Mathlib.Analysis.Calculus.FDeriv.Symmetric Mathlib.Analysis.Calculus.FDeriv.WithLp Mathlib.Analysis.Calculus.FormalMultilinearSeries Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.Analysis.Calculus.ImplicitContDiff Mathlib.Analysis.Calculus.ImplicitFunction.Bivariate Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain Mathlib.Analysis.Calculus.Implicit Mathlib.Analysis.Calculus.InverseFunctionTheorem.Analytic Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional Mathlib.Analysis.Calculus.IteratedDeriv.Analytic Mathlib.Analysis.Calculus.IteratedDeriv.ConvergenceOnBall Mathlib.Analysis.Calculus.IteratedDeriv.Defs Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas Mathlib.Analysis.Calculus.IteratedDeriv.WithinZpow Mathlib.Analysis.Calculus.LHopital Mathlib.Analysis.Calculus.LagrangeMultipliers Mathlib.Analysis.Calculus.LineDeriv.Basic Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap Mathlib.Analysis.Calculus.LocalExtr.Basic Mathlib.Analysis.Calculus.LocalExtr.LineDeriv Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.Analysis.Calculus.LocalExtr.Rolle Mathlib.Analysis.Calculus.LogDerivUniformlyOn Mathlib.Analysis.Calculus.LogDeriv Mathlib.Analysis.Calculus.MeanValue Mathlib.Analysis.Calculus.Monotone Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Calculus.SmoothSeries Mathlib.Analysis.Calculus.TangentCone.DimOne Mathlib.Analysis.Calculus.TangentCone.ProperSpace 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.BranchLogRoot Mathlib.Analysis.Complex.CanonicalDecomposition Mathlib.Analysis.Complex.Cardinality Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Analysis.Complex.Circle Mathlib.Analysis.Complex.Conformal Mathlib.Analysis.Complex.Convex Mathlib.Analysis.Complex.CoveringMap Mathlib.Analysis.Complex.ExponentialBounds Mathlib.Analysis.Complex.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.OpenMapping Mathlib.Analysis.Complex.OperatorNorm Mathlib.Analysis.Complex.Periodic Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.Analysis.Complex.Poisson Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.Analysis.Complex.Polynomial.GaussLucas Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Analysis.Complex.Positivity Mathlib.Analysis.Complex.ReImTopology Mathlib.Analysis.Complex.RealDeriv Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Analysis.Complex.RiemannMapping Mathlib.Analysis.Complex.Schwarz Mathlib.Analysis.Complex.Spectrum Mathlib.Analysis.Complex.SqrtDeriv Mathlib.Analysis.Complex.SummableUniformlyOn Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Complex.Tietze Mathlib.Analysis.Complex.UnitDisc.Basic Mathlib.Analysis.Complex.UpperHalfPlane.Basic Mathlib.Analysis.Complex.UpperHalfPlane.Exp Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty Mathlib.Analysis.Complex.UpperHalfPlane.Manifold Mathlib.Analysis.Complex.UpperHalfPlane.Measure Mathlib.Analysis.Complex.UpperHalfPlane.Metric Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction Mathlib.Analysis.Complex.UpperHalfPlane.Topology Mathlib.Analysis.Complex.ValueDistribution.Cartan Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic Mathlib.Analysis.ConstantSpeed Mathlib.Analysis.Convex.AmpleSet Mathlib.Analysis.Convex.Approximation Mathlib.Analysis.Convex.Birkhoff Mathlib.Analysis.Convex.Body Mathlib.Analysis.Convex.Cone.Basic Mathlib.Analysis.Convex.Cone.Dual Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Analysis.Convex.Cone.TensorProduct Mathlib.Analysis.Convex.ContinuousLinearEquiv Mathlib.Analysis.Convex.Continuous Mathlib.Analysis.Convex.Deriv Mathlib.Analysis.Convex.DoublyStochasticMatrix Mathlib.Analysis.Convex.EGauge Mathlib.Analysis.Convex.Exposed Mathlib.Analysis.Convex.GaugeRescale Mathlib.Analysis.Convex.Gauge Mathlib.Analysis.Convex.Integral Mathlib.Analysis.Convex.Intrinsic Mathlib.Analysis.Convex.KreinMilman Mathlib.Analysis.Convex.LinearIsometry Mathlib.Analysis.Convex.Measure Mathlib.Analysis.Convex.MetricSpace Mathlib.Analysis.Convex.PartitionOfUnity Mathlib.Analysis.Convex.Side Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.Analysis.Convex.SpecificFunctions.Deriv Mathlib.Analysis.Convex.SpecificFunctions.Pow Mathlib.Analysis.Convex.Strict.Extreme Mathlib.Analysis.Convex.StrictCombination Mathlib.Analysis.Convex.StrictConvexBetween Mathlib.Analysis.Convex.StrictConvexSpace Mathlib.Analysis.Convex.Strong 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.Notation 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.RCLike Mathlib.Analysis.Meromorphic.TrailingCoefficient Mathlib.Analysis.Normed.Affine.AddTorsorBases Mathlib.Analysis.Normed.Affine.AddTorsor Mathlib.Analysis.Normed.Affine.AsymptoticCone Mathlib.Analysis.Normed.Affine.Ceva Mathlib.Analysis.Normed.Affine.ContinuousAffineMap Mathlib.Analysis.Normed.Affine.Convex Mathlib.Analysis.Normed.Affine.Isometry Mathlib.Analysis.Normed.Affine.MazurUlam Mathlib.Analysis.Normed.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.Completeness Mathlib.Analysis.Normed.Group.Completion Mathlib.Analysis.Normed.Group.ControlledClosure Mathlib.Analysis.Normed.Group.FunctionSeries Mathlib.Analysis.Normed.Group.HomCompletion Mathlib.Analysis.Normed.Group.Hom Mathlib.Analysis.Normed.Group.InfiniteSum Mathlib.Analysis.Normed.Group.Lemmas Mathlib.Analysis.Normed.Group.NullSubmodule Mathlib.Analysis.Normed.Group.Pointwise Mathlib.Analysis.Normed.Group.Quotient Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels Mathlib.Analysis.Normed.Group.SemiNormedGrp Mathlib.Analysis.Normed.Group.SeparationQuotient Mathlib.Analysis.Normed.Group.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.lpHolder Mathlib.Analysis.Normed.Lp.lpSpace Mathlib.Analysis.Normed.Module.Alternating.Basic Mathlib.Analysis.Normed.Module.Alternating.Curry Mathlib.Analysis.Normed.Module.Alternating.Uncurry.Fin Mathlib.Analysis.Normed.Module.Ball.Action Mathlib.Analysis.Normed.Module.Ball.Homeomorph Mathlib.Analysis.Normed.Module.Ball.Pointwise Mathlib.Analysis.Normed.Module.Ball.RadialEquiv Mathlib.Analysis.Normed.Module.Bases Mathlib.Analysis.Normed.Module.Basic Mathlib.Analysis.Normed.Module.Complemented Mathlib.Analysis.Normed.Module.Completion Mathlib.Analysis.Normed.Module.Connected Mathlib.Analysis.Normed.Module.ContinuousInverse Mathlib.Analysis.Normed.Module.Convex Mathlib.Analysis.Normed.Module.DoubleDual Mathlib.Analysis.Normed.Module.Dual Mathlib.Analysis.Normed.Module.Extr Mathlib.Analysis.Normed.Module.FiniteDimension Mathlib.Analysis.Normed.Module.HahnBanach Mathlib.Analysis.Normed.Module.Multilinear.Basic Mathlib.Analysis.Normed.Module.Multilinear.Curry Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn Mathlib.Analysis.Normed.Module.Normalize Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm Mathlib.Analysis.Normed.Module.RCLike.Basic Mathlib.Analysis.Normed.Module.RCLike.Extend Mathlib.Analysis.Normed.Module.RCLike.Real Mathlib.Analysis.Normed.Module.Ray Mathlib.Analysis.Normed.Module.RieszLemma Mathlib.Analysis.Normed.Module.Shrink Mathlib.Analysis.Normed.Module.Span Mathlib.Analysis.Normed.Module.TransferInstance Mathlib.Analysis.Normed.Module.WeakDual Mathlib.Analysis.Normed.MulAction Mathlib.Analysis.Normed.Operator.Asymptotics Mathlib.Analysis.Normed.Operator.BanachSteinhaus Mathlib.Analysis.Normed.Operator.Banach Mathlib.Analysis.Normed.Operator.Basic Mathlib.Analysis.Normed.Operator.Bilinear Mathlib.Analysis.Normed.Operator.BoundedLinearMaps Mathlib.Analysis.Normed.Operator.Compact.Basic Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative Mathlib.Analysis.Normed.Operator.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.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.MultipliableUniformlyOn Mathlib.Analysis.ODE.Basic Mathlib.Analysis.ODE.DiscreteGronwall Mathlib.Analysis.ODE.ExistUnique Mathlib.Analysis.ODE.Gronwall Mathlib.Analysis.ODE.PicardLindelof Mathlib.Analysis.ODE.Transform Mathlib.Analysis.PSeriesComplex Mathlib.Analysis.PSeries Mathlib.Analysis.Polynomial.Basic Mathlib.Analysis.Polynomial.Factorization Mathlib.Analysis.Polynomial.Fourier Mathlib.Analysis.Polynomial.MahlerMeasure Mathlib.Analysis.Polynomial.Norm Mathlib.Analysis.Polynomial.Order Mathlib.Analysis.Quaternion Mathlib.Analysis.RCLike.Basic Mathlib.Analysis.RCLike.BoundedContinuous Mathlib.Analysis.RCLike.ContinuousMap Mathlib.Analysis.RCLike.Extend Mathlib.Analysis.RCLike.Inner Mathlib.Analysis.RCLike.Lemmas Mathlib.Analysis.RCLike.Sqrt Mathlib.Analysis.RCLike.TangentCone Mathlib.Analysis.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.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.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.ChebyshevGauss Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse Mathlib.Analysis.SpecialFunctions.Trigonometric.Meromorphic Mathlib.Analysis.SpecialFunctions.Trigonometric.Series Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc Mathlib.Analysis.SpecificLimits.ArithmeticGeometric Mathlib.Analysis.SpecificLimits.Basic Mathlib.Analysis.SpecificLimits.Fibonacci Mathlib.Analysis.SpecificLimits.FloorPow Mathlib.Analysis.SpecificLimits.Normed Mathlib.Analysis.SpecificLimits.RCLike Mathlib.Analysis.SumIntegralComparisons Mathlib.Analysis.SumIntegralExpDecay Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.Combinatorics.Additive.Randomisation 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.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.FieldTheory.Laurent Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.FieldTheory.RatFunc.Degree Mathlib.FieldTheory.RatFunc.IntermediateField Mathlib.FieldTheory.RatFunc.Luroth Mathlib.FieldTheory.RatFunc.Valuation Mathlib.Geometry.Diffeology.Basic Mathlib.Geometry.Euclidean.Altitude Mathlib.Geometry.Euclidean.Angle.Bisector Mathlib.Geometry.Euclidean.Angle.Incenter Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.Geometry.Euclidean.Angle.Oriented.Projection Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality Mathlib.Geometry.Euclidean.Basic Mathlib.Geometry.Euclidean.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.SMul Mathlib.Geometry.Manifold.Algebra.SmoothFunctions Mathlib.Geometry.Manifold.Algebra.Structures Mathlib.Geometry.Manifold.Bordism Mathlib.Geometry.Manifold.BumpFunction 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.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.LocalSourceTargetProperty Mathlib.Geometry.Manifold.MFDeriv.Atlas Mathlib.Geometry.Manifold.MFDeriv.Basic Mathlib.Geometry.Manifold.MFDeriv.Defs Mathlib.Geometry.Manifold.MFDeriv.FDeriv Mathlib.Geometry.Manifold.MFDeriv.NormedSpace Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions Mathlib.Geometry.Manifold.MFDeriv.Tangent Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential Mathlib.Geometry.Manifold.Metrizable Mathlib.Geometry.Manifold.Notation Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.Geometry.Manifold.Riemannian.Basic Mathlib.Geometry.Manifold.Riemannian.PathELength Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Geometry.Manifold.SmoothApprox Mathlib.Geometry.Manifold.SmoothEmbedding Mathlib.Geometry.Manifold.VectorBundle.Basic Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection 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.Eigenspace.ContinuousLinearMap 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.CompleteOfCompleteLp Mathlib.MeasureTheory.Function.LpSpace.Complete Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.MeasureTheory.Function.LpSpace.Indicator Mathlib.MeasureTheory.Function.LpSpace.InfiniteSum Mathlib.MeasureTheory.Function.Piecewise Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.MeasureTheory.Function.SimpleFuncDense Mathlib.MeasureTheory.Function.SimpleFunc Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan Mathlib.MeasureTheory.Function.SpecialFunctions.Basic Mathlib.MeasureTheory.Function.SpecialFunctions.Inner Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.MeasureTheory.Function.UnifTight Mathlib.MeasureTheory.Function.UniformIntegrable Mathlib.MeasureTheory.Group.AEStabilizer Mathlib.MeasureTheory.Group.Action Mathlib.MeasureTheory.Group.AddCircle Mathlib.MeasureTheory.Group.Arithmetic Mathlib.MeasureTheory.Group.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.ResolventTransform 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.Typeclasses.ZeroOne Mathlib.MeasureTheory.Measure.WithDensityFinite Mathlib.MeasureTheory.Measure.WithDensity Mathlib.MeasureTheory.Order.Group.Lattice Mathlib.MeasureTheory.Order.Lattice Mathlib.MeasureTheory.Order.UpperLower Mathlib.MeasureTheory.OuterMeasure.Caratheodory Mathlib.MeasureTheory.OuterMeasure.Induced Mathlib.MeasureTheory.OuterMeasure.OfAddContent Mathlib.MeasureTheory.OuterMeasure.OfFunction Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap Mathlib.MeasureTheory.SpecificCodomains.Pi Mathlib.MeasureTheory.SpecificCodomains.WithLp Mathlib.MeasureTheory.Topology Mathlib.MeasureTheory.VectorMeasure.AddContent Mathlib.MeasureTheory.VectorMeasure.Basic Mathlib.MeasureTheory.VectorMeasure.BoundedVariation Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue Mathlib.MeasureTheory.VectorMeasure.Decomposition.RadonNikodym Mathlib.MeasureTheory.VectorMeasure.Integral Mathlib.MeasureTheory.VectorMeasure.Variation.Basic Mathlib.MeasureTheory.VectorMeasure.Variation.Defs Mathlib.MeasureTheory.VectorMeasure.WithDensity Mathlib.NumberTheory.AbelSummation Mathlib.NumberTheory.ArithmeticFunction.Carmichael Mathlib.NumberTheory.ArithmeticFunction.LFunction Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt Mathlib.NumberTheory.ArithmeticFunction Mathlib.NumberTheory.BernoulliPolynomials Mathlib.NumberTheory.Bernoulli 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.DirichletCharacter.GaussSum Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.NumberTheory.EulerProduct.Basic Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.NumberTheory.EulerProduct.ExpLog Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.FunctionField Mathlib.NumberTheory.GaussSum Mathlib.NumberTheory.Harmonic.Bounds Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.Harmonic.Int Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.NumberTheory.Height.Basic Mathlib.NumberTheory.Height.MvPolynomial Mathlib.NumberTheory.Height.Northcott Mathlib.NumberTheory.Height.NumberField Mathlib.NumberTheory.Height.Projectivization Mathlib.NumberTheory.JacobiSum.Basic Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.LSeries.Basic Mathlib.NumberTheory.LSeries.Convergence Mathlib.NumberTheory.LSeries.Convolution Mathlib.NumberTheory.LSeries.Deriv Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.NumberTheory.LSeries.Injectivity Mathlib.NumberTheory.LSeries.Linearity Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.NumberTheory.LSeries.Positivity Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.NumberTheory.LSeries.SumCoeff Mathlib.NumberTheory.LSeries.ZMod Mathlib.NumberTheory.LSeries.ZetaZeros Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.LegendreSymbol.Complex Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.NumberTheory.LocalField.Basic Mathlib.NumberTheory.LucasLehmer Mathlib.NumberTheory.MahlerMeasure Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups Mathlib.NumberTheory.ModularForms.Basic Mathlib.NumberTheory.ModularForms.BoundedAtCusp Mathlib.NumberTheory.ModularForms.Bounds Mathlib.NumberTheory.ModularForms.CongruenceSubgroups Mathlib.NumberTheory.ModularForms.CuspFormSubmodule Mathlib.NumberTheory.ModularForms.Cusps Mathlib.NumberTheory.ModularForms.DedekindEta Mathlib.NumberTheory.ModularForms.Delta Mathlib.NumberTheory.ModularForms.Derivative Mathlib.NumberTheory.ModularForms.DimensionFormulas.LevelOne Mathlib.NumberTheory.ModularForms.Discriminant Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence Mathlib.NumberTheory.ModularForms.Identities Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.NumberTheory.ModularForms.LevelOne.Basic Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing Mathlib.NumberTheory.ModularForms.LevelOne Mathlib.NumberTheory.ModularForms.NormTrace Mathlib.NumberTheory.ModularForms.Petersson Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.NumberTheory.ModularForms.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.ExistsRamified 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.PrimesCongruentOne Mathlib.NumberTheory.RamificationInertia.Valuation Mathlib.NumberTheory.RatFunc.Ostrowski 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.Order.Filter.ZeroAndBoundedAtFilter Mathlib.Probability.BorelCantelli Mathlib.Probability.BrownianMotion.Basic Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily Mathlib.Probability.CDF Mathlib.Probability.CentralLimitTheorem Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs Mathlib.Probability.CondVar Mathlib.Probability.ConditionalExpectation Mathlib.Probability.ConditionalProbability Mathlib.Probability.Decision.Risk.Basic Mathlib.Probability.Decision.Risk.Countable Mathlib.Probability.Decision.Risk.Defs Mathlib.Probability.Density Mathlib.Probability.Distributions.Bernoulli Mathlib.Probability.Distributions.Beta Mathlib.Probability.Distributions.Binomial Mathlib.Probability.Distributions.Cauchy Mathlib.Probability.Distributions.Exponential Mathlib.Probability.Distributions.Fernique Mathlib.Probability.Distributions.Gamma Mathlib.Probability.Distributions.Gaussian.Basic Mathlib.Probability.Distributions.Gaussian.CharFun Mathlib.Probability.Distributions.Gaussian.Fernique Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Def Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Def Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence Mathlib.Probability.Distributions.Gaussian.Multivariate Mathlib.Probability.Distributions.Gaussian.Real Mathlib.Probability.Distributions.Geometric Mathlib.Probability.Distributions.Pareto Mathlib.Probability.Distributions.Poisson.Basic Mathlib.Probability.Distributions.Poisson.PoissonLimitThm Mathlib.Probability.Distributions.SetBernoulli Mathlib.Probability.Distributions.TwoValued Mathlib.Probability.Distributions.Uniform Mathlib.Probability.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.Deterministic Mathlib.Probability.Kernel.Disintegration.Basic Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.Probability.Kernel.Disintegration.Density Mathlib.Probability.Kernel.Disintegration.Integral Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.Probability.Kernel.Integral Mathlib.Probability.Kernel.Invariance Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj Mathlib.Probability.Kernel.IonescuTulcea.Traj Mathlib.Probability.Kernel.Irreducible Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Probability.Kernel.MeasurableLIntegral Mathlib.Probability.Kernel.Posterior Mathlib.Probability.Kernel.Proper Mathlib.Probability.Kernel.RadonNikodym Mathlib.Probability.Kernel.Representation Mathlib.Probability.Kernel.SetIntegral Mathlib.Probability.Kernel.WithDensity Mathlib.Probability.Martingale.Basic Mathlib.Probability.Martingale.BorelCantelli Mathlib.Probability.Martingale.Centering Mathlib.Probability.Martingale.Convergence Mathlib.Probability.Martingale.OptionalSampling Mathlib.Probability.Martingale.OptionalStopping Mathlib.Probability.Martingale.Upcrossing Mathlib.Probability.Moments.Basic Mathlib.Probability.Moments.ComplexMGF Mathlib.Probability.Moments.CovarianceBilinDual Mathlib.Probability.Moments.CovarianceBilin Mathlib.Probability.Moments.Covariance Mathlib.Probability.Moments.IntegrableExpMul Mathlib.Probability.Moments.MGFAnalytic Mathlib.Probability.Moments.SubGaussian Mathlib.Probability.Moments.Tilted Mathlib.Probability.Moments.Variance Mathlib.Probability.Notation Mathlib.Probability.ProbabilityMassFunction.Basic Mathlib.Probability.ProbabilityMassFunction.Binomial Mathlib.Probability.ProbabilityMassFunction.Constructions Mathlib.Probability.ProbabilityMassFunction.Integrals Mathlib.Probability.ProbabilityMassFunction.Monad Mathlib.Probability.Process.Adapted Mathlib.Probability.Process.Filtration Mathlib.Probability.Process.FiniteDimensionalLaws Mathlib.Probability.Process.HittingTime Mathlib.Probability.Process.Kolmogorov Mathlib.Probability.Process.LocalProperty Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Process.Predictable Mathlib.Probability.Process.Stopping Mathlib.Probability.ProductMeasure Mathlib.Probability.StrongLaw Mathlib.Probability.UniformOn Mathlib.RepresentationTheory.Continuous.Basic Mathlib.RingTheory.AdicCompletion.Completeness Mathlib.RingTheory.AdicCompletion.LocalRing Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.RingTheory.DedekindDomain.GaussLemma Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.RingTheory.DividedPowers.Padic Mathlib.RingTheory.Etale.QuasiFinite Mathlib.RingTheory.FormalGroup.Basic Mathlib.RingTheory.HahnSeries.HahnEmbedding Mathlib.RingTheory.Invariant.Profinite Mathlib.RingTheory.LaurentSeries Mathlib.RingTheory.LittleWedderburn Mathlib.RingTheory.LocalRing.ResidueField.Polynomial Mathlib.RingTheory.MvPowerSeries.Equiv Mathlib.RingTheory.MvPowerSeries.Evaluation Mathlib.RingTheory.MvPowerSeries.Expand Mathlib.RingTheory.MvPowerSeries.Rename Mathlib.RingTheory.MvPowerSeries.Substitution Mathlib.RingTheory.OrderOfVanishing.Noetherian Mathlib.RingTheory.Perfection Mathlib.RingTheory.Perfectoid.BDeRham Mathlib.RingTheory.Perfectoid.FontaineTheta Mathlib.RingTheory.Perfectoid.Untilt Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.RingTheory.Polynomial.Hermite.Gaussian Mathlib.RingTheory.Polynomial.Selmer Mathlib.RingTheory.PowerSeries.Derivative Mathlib.RingTheory.PowerSeries.Evaluation Mathlib.RingTheory.PowerSeries.Exp Mathlib.RingTheory.PowerSeries.Expand Mathlib.RingTheory.PowerSeries.Log Mathlib.RingTheory.PowerSeries.Restricted Mathlib.RingTheory.PowerSeries.Substitution Mathlib.RingTheory.QuasiFinite.Polynomial Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.RingTheory.RootsOfUnity.Complex Mathlib.RingTheory.Smooth.IntegralClosure Mathlib.RingTheory.Teichmuller Mathlib.RingTheory.Unramified.LocalStructure Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing Mathlib.RingTheory.Valuation.Discrete.RankOne Mathlib.RingTheory.Valuation.DiscreteValuativeRel Mathlib.RingTheory.Valuation.RankOne Mathlib.RingTheory.WittVector.Compare Mathlib.RingTheory.ZMod.UnitsCyclic Mathlib.RingTheory.ZariskisMainTheorem Mathlib.Tactic.ComputeAsymptotics.Lemmas Mathlib.Tactic.ComputeAsymptotics.Multiseries.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 Mathlib.Topology.Algebra.AffineSubspace Mathlib.Topology.Algebra.Algebra.Equiv Mathlib.Topology.Algebra.Algebra Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits Mathlib.Topology.Algebra.ContinuousAffineEquiv Mathlib.Topology.Algebra.ContinuousAffineMap Mathlib.Topology.Algebra.Group.CompactOpen Mathlib.Topology.Algebra.Group.Matrix Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution Mathlib.Topology.Algebra.InfiniteSum.Module Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn Mathlib.Topology.Algebra.LinearMapCompletion Mathlib.Topology.Algebra.Module.Alternating.Basic Mathlib.Topology.Algebra.Module.Alternating.Topology Mathlib.Topology.Algebra.Module.Cardinality Mathlib.Topology.Algebra.Module.ClosedSubmodule Mathlib.Topology.Algebra.Module.Complement Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict Mathlib.Topology.Algebra.Module.Determinant Mathlib.Topology.Algebra.Module.Equiv Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear Mathlib.Topology.Algebra.Module.FiniteDimension Mathlib.Topology.Algebra.Module.LinearMapPiProd Mathlib.Topology.Algebra.Module.LinearMap Mathlib.Topology.Algebra.Module.LinearPMap Mathlib.Topology.Algebra.Module.ModuleTopology Mathlib.Topology.Algebra.Module.Multilinear.Basic Mathlib.Topology.Algebra.Module.Multilinear.Bounded Mathlib.Topology.Algebra.Module.Multilinear.Topology Mathlib.Topology.Algebra.Module.PerfectPairing Mathlib.Topology.Algebra.Module.PerfectSpace Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM Mathlib.Topology.Algebra.Module.Spaces.WeakBilin Mathlib.Topology.Algebra.Module.Spaces.WeakDual Mathlib.Topology.Algebra.Module.Star Mathlib.Topology.Algebra.Module.StrongTopology Mathlib.Topology.Algebra.Module.TopDualPairing Mathlib.Topology.Algebra.Module.TransferInstance Mathlib.Topology.Algebra.Module.UniformConvergence Mathlib.Topology.Algebra.Nonarchimedean.Completion Mathlib.Topology.Algebra.Polynomial Mathlib.Topology.Algebra.PontryaginDual Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous Mathlib.Topology.Algebra.SeparationQuotient.Basic Mathlib.Topology.Algebra.SeparationQuotient.FiniteDimensional Mathlib.Topology.Algebra.SeparationQuotient.Hom Mathlib.Topology.Algebra.SeparationQuotient.Section Mathlib.Topology.Algebra.Star.LinearMap Mathlib.Topology.Algebra.StarSubalgebra Mathlib.Topology.Algebra.UniformField Mathlib.Topology.Algebra.UniformRing Mathlib.Topology.Algebra.Valued.LocallyCompact Mathlib.Topology.Algebra.Valued.NormedValued Mathlib.Topology.Algebra.Valued.ValuedField Mathlib.Topology.Algebra.Valued.WithVal Mathlib.Topology.Baire.BaireMeasurable Mathlib.Topology.Baire.CompleteMetrizable Mathlib.Topology.Bornology.BoundedOperation Mathlib.Topology.CWComplex.Abstract.Basic Mathlib.Topology.CWComplex.Classical.Basic Mathlib.Topology.CWComplex.Classical.Finite Mathlib.Topology.CWComplex.Classical.Graph Mathlib.Topology.CWComplex.Classical.Subcomplex Mathlib.Topology.Category.CompHaus.Basic Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.Topology.Category.CompHaus.Frm Mathlib.Topology.Category.CompHaus.Limits Mathlib.Topology.Category.CompHaus.Projective Mathlib.Topology.Category.CompactlyGenerated Mathlib.Topology.Category.Compactum Mathlib.Topology.Category.DeltaGenerated Mathlib.Topology.Category.LightProfinite.AsLimit Mathlib.Topology.Category.LightProfinite.Basic Mathlib.Topology.Category.LightProfinite.Cartesian Mathlib.Topology.Category.LightProfinite.EffectiveEpi Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Topology.Category.LightProfinite.Injective Mathlib.Topology.Category.LightProfinite.Limits Mathlib.Topology.Category.LightProfinite.Sequence Mathlib.Topology.Category.Locale Mathlib.Topology.Category.Profinite.AsLimit Mathlib.Topology.Category.Profinite.Basic Mathlib.Topology.Category.Profinite.CofilteredLimit Mathlib.Topology.Category.Profinite.EffectiveEpi Mathlib.Topology.Category.Profinite.Extend Mathlib.Topology.Category.Profinite.Limits Mathlib.Topology.Category.Profinite.Nobeling.Basic Mathlib.Topology.Category.Profinite.Nobeling.Induction Mathlib.Topology.Category.Profinite.Nobeling.Span Mathlib.Topology.Category.Profinite.Nobeling.Successor Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit Mathlib.Topology.Category.Profinite.Product Mathlib.Topology.Category.Profinite.Projective Mathlib.Topology.Category.Stonean.Adjunctions Mathlib.Topology.Category.Stonean.Basic Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Topology.Category.Stonean.Limits Mathlib.Topology.Category.TopCat.Sphere Mathlib.Topology.Compactification.OnePoint.Sphere Mathlib.Topology.Compactness.CompactlyGeneratedSpace Mathlib.Topology.Compactness.DeltaGeneratedSpace Mathlib.Topology.ContinuousMap.Algebra Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli Mathlib.Topology.ContinuousMap.Bounded.Basic Mathlib.Topology.ContinuousMap.Bounded.Normed Mathlib.Topology.ContinuousMap.Bounded.Star Mathlib.Topology.ContinuousMap.BoundedCompactlySupported Mathlib.Topology.ContinuousMap.Compact Mathlib.Topology.ContinuousMap.CompactlySupported Mathlib.Topology.ContinuousMap.ContinuousMapZero Mathlib.Topology.ContinuousMap.ContinuousSqrt Mathlib.Topology.ContinuousMap.Ideals Mathlib.Topology.ContinuousMap.Lattice Mathlib.Topology.ContinuousMap.LocallyConstant Mathlib.Topology.ContinuousMap.LocallyConvex Mathlib.Topology.ContinuousMap.Periodic Mathlib.Topology.ContinuousMap.Polynomial Mathlib.Topology.ContinuousMap.StarOrdered Mathlib.Topology.ContinuousMap.Star Mathlib.Topology.ContinuousMap.StoneWeierstrass Mathlib.Topology.ContinuousMap.Units Mathlib.Topology.ContinuousMap.Weierstrass Mathlib.Topology.ContinuousMap.ZeroAtInfty Mathlib.Topology.EMetricSpace.PairReduction Mathlib.Topology.Instances.CantorSet Mathlib.Topology.Instances.Complex Mathlib.Topology.Instances.RealVectorSpace Mathlib.Topology.Instances.TrivSqZeroExt Mathlib.Topology.MetricSpace.Algebra 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.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.Separation.CompletelyRegular Mathlib.Topology.Separation.Lemmas Mathlib.Topology.Separation.PerfectlyNormal Mathlib.Topology.Sheaves.CommRingCat Mathlib.Topology.TietzeExtension Mathlib.Topology.UniformSpace.Dini Mathlib.Topology.UniformSpace.ProdApproximation Mathlib.Topology.UniformSpace.Uniformizable Mathlib.Topology.UrysohnsBounded Mathlib.Topology.UrysohnsLemma Mathlib.Topology.VectorBundle.Basic Mathlib.Topology.VectorBundle.Constructions Mathlib.Topology.VectorBundle.ContinuousAlternatingMap Mathlib.Topology.VectorBundle.FiniteDimensional Mathlib.Topology.VectorBundle.Hom Mathlib.Topology.VectorBundle.Riemannian
 3

Declarations diff (regex)

+ instIsAddApply
+ instIsIntCastApply
+ instIsNatCastApply
+ instIsOneApply
+ instance : IsMulApplyEqComp (M₁ →L[R₁] M₁) M₁
+ instance : IsNegApply (M →SL[σ₁₂] M₂) M M₂
+ instance : IsSMulApply S₂ (M₁ →SL[σ₁₂] M₂) M₁ M₂
+ instance : IsSubApply (M →SL[σ₁₂] M₂) M M₂
+ instance : IsZeroApply (M₁ →SL[σ₁₂] M₂) M₁ M₂
+ instance [IsTopologicalAddGroup M] : IntCast (M →L[R] M)
+ toLinearMap_add
+ toLinearMap_comp
+ toLinearMap_mul
+ toLinearMap_neg
+ toLinearMap_one
+ toLinearMap_smul
+ toLinearMap_sub
+ toLinearMap_sum
+ toLinearMap_zero

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

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

Declarations diff (Lean)

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

  • +19 new declarations
  • −0 removed declarations
+ContinuousLinearMap.instIntCastIdOfIsTopologicalAddGroup
+ContinuousLinearMap.instIsAddApply
+ContinuousLinearMap.instIsIntCastApply
+ContinuousLinearMap.instIsMulApplyEqCompId
+ContinuousLinearMap.instIsNatCastApply
+ContinuousLinearMap.instIsNegApply
+ContinuousLinearMap.instIsOneApply
+ContinuousLinearMap.instIsSMulApply
+ContinuousLinearMap.instIsSubApply
+ContinuousLinearMap.instIsZeroApply
+ContinuousLinearMap.toLinearMap_add
+ContinuousLinearMap.toLinearMap_comp
+ContinuousLinearMap.toLinearMap_mul
+ContinuousLinearMap.toLinearMap_neg
+ContinuousLinearMap.toLinearMap_one
+ContinuousLinearMap.toLinearMap_smul
+ContinuousLinearMap.toLinearMap_sub
+ContinuousLinearMap.toLinearMap_sum
+ContinuousLinearMap.toLinearMap_zero

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 3df4a86029
Reference commit 69a31073de

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

@mcdoll mcdoll mentioned this pull request May 21, 2026
Open
29 tasks
@mcdoll

mcdoll commented May 21, 2026

Copy link
Copy Markdown
Member Author

!radar

@mcdoll
mcdoll marked this pull request as ready for review May 21, 2026 19:36
@leanprover-radar

leanprover-radar commented May 21, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for 04e741d against 89d4407 are in. There are significant results. @mcdoll

  • 🟥 main exited with code 1

No significant changes detected.

@mcdoll

mcdoll commented May 21, 2026

Copy link
Copy Markdown
Member Author

!radar

@leanprover-radar

leanprover-radar commented May 21, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for b458cd6 against 89d4407 are in. No significant results found. @mcdoll

  • 🟥 build//instructions: +52.3G (+0.03%)

Small changes (4✅, 7🟥)

  • ✅ build/module/Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal//instructions: -766.7M (-1.96%)
  • 🟥 build/module/Mathlib.Analysis.Calculus.Deriv.Mul//instructions: +2.2G (+2.14%)
  • 🟥 build/module/Mathlib.Analysis.Calculus.Deriv.Pow//instructions: +810.9M (+4.19%)
  • 🟥 build/module/Mathlib.Analysis.Distribution.FourierMultiplier//instructions: +813.5M (+2.13%)
  • 🟥 build/module/Mathlib.Analysis.Distribution.SchwartzSpace.Fourier//instructions: +1.2G (+1.44%)
  • ✅ build/module/Mathlib.Analysis.InnerProductSpace.Reproducing//instructions: -2.8G (-3.27%)
  • ✅ build/module/Mathlib.Analysis.InnerProductSpace.StarOrder//instructions: -1.5G (-6.16%)
  • 🟥 build/module/Mathlib.Analysis.Normed.Operator.Compact.FredholmAlternative//instructions: +1.3G (+2.90%)
  • 🟥 build/module/Mathlib.Analysis.SpecialFunctions.Pow.Deriv//instructions: +812.5M (+1.29%)
  • ✅ build/module/Mathlib.Analysis.VonNeumannAlgebra.Basic//instructions: -811.9M (-3.85%)
  • 🟥 build/module/Mathlib.NumberTheory.LSeries.HurwitzZetaValues//instructions: +534.5M (+2.62%)

@mathlib-merge-conflicts mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 22, 2026
@mathlib-merge-conflicts

mathlib-merge-conflicts Bot commented May 22, 2026

Copy link
Copy Markdown

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

@mcdoll
mcdoll temporarily deployed to cache-upload-forks June 5, 2026 17:32 — with GitHub Actions Inactive
@mcdoll
mcdoll temporarily deployed to cache-upload-forks June 5, 2026 17:37 — with GitHub Actions Inactive
@mcdoll
mcdoll temporarily deployed to cache-upload-forks June 5, 2026 17:45 — with GitHub Actions Inactive
@mcdoll
mcdoll temporarily deployed to cache-upload-forks June 5, 2026 19:03 — with GitHub Actions Inactive
@mcdoll
mcdoll temporarily deployed to cache-upload-forks June 5, 2026 19:27 — with GitHub Actions Inactive
@mathlib-merge-conflicts mathlib-merge-conflicts Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 7, 2026
@mathlib-merge-conflicts

mathlib-merge-conflicts Bot commented Jun 7, 2026

Copy link
Copy Markdown

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

@github-actions github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 9, 2026
@mcdoll
mcdoll temporarily deployed to cache-upload-forks June 9, 2026 01:03 — with GitHub Actions Inactive
j-loreaux
j-loreaux reviewed Jun 9, 2026
View reviewed changes

@j-loreaux j-loreaux left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Overall I think this is good. Just a few minor comments.

If you push me about the comp_apply issue I may acquiesce.

Comment thread Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean Outdated
Comment thread Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean
Comment thread Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean
Comment thread Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean
Comment thread Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean
Comment thread Mathlib/Topology/Algebra/Module/Spaces/UniformConvergenceCLM.lean
Comment thread Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
Comment thread Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
Comment thread Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
@j-loreaux j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 9, 2026
@mcdoll mcdoll removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 9, 2026
@j-loreaux

j-loreaux commented Jun 10, 2026

Copy link
Copy Markdown
Contributor

@mcdoll I think you missed my very first change, or else didn't push. I'm content with your responses to the rest.

bors d+

@mathlib-bors

mathlib-bors Bot commented Jun 10, 2026

Copy link
Copy Markdown
Contributor

✌️ mcdoll can now approve this pull request until 2026-06-24 03:11 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

⚠️ This delegation only covers changes within Archive/**, Counterexamples/**, docs/**, DownstreamTest/**, Mathlib/**, MathlibTest/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.lean; an author commit touching anything else will revoke it. Bors also revokes it if a later push changes too many files for it to check the full list — even if it stays within scope.

@mathlib-triage mathlib-triage Bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Jun 10, 2026
@mcdoll @j-loreaux
Update Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean
3df4a86 
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
@mcdoll

mcdoll commented Jun 10, 2026

Copy link
Copy Markdown
Member Author

Thanks!
bors merge

mathlib-bors Bot pushed a commit that referenced this pull request Jun 10, 2026
@mcdoll
feat(Topology/Algebra): use Is*Apply for ContinuousLinearMap (#39637
1ccad00 
)

This is the first in many PRs that use the new `Is*Apply` classes instead of structure specific `foo_apply` lemmas.
The main bulk of the PR is in Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean, everything else is just fixing errors.

For each `foo` in `zero`, `one`, `add`, `sub`, `neg`, smul` we do the following:
- add an instance `IsFooApply`
- rename `coe_foo` to `toLinearMap_foo`
- depreprecate `coe_foo`, `coe_foo'`, and `foo_apply`

We are rather conservative when it comes to the instances, in future PRs this will be used more.

For consistency, the same renaming has been applied to the `comp` variants. This resulted in a test being changed.
@mathlib-bors

mathlib-bors Bot commented Jun 10, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title feat(Topology/Algebra): use Is*Apply for ContinuousLinearMap [Merged by Bors] - feat(Topology/Algebra): use Is*Apply for ContinuousLinearMap Jun 10, 2026
@mathlib-bors mathlib-bors Bot closed this Jun 10, 2026
xroblot pushed a commit to xroblot/mathlib4 that referenced this pull request Jun 13, 2026
@mcdoll @xroblot
feat(Topology/Algebra): use Is*Apply for ContinuousLinearMap (lea…
c17b2ef 
…nprover-community#39637)

This is the first in many PRs that use the new `Is*Apply` classes instead of structure specific `foo_apply` lemmas.
The main bulk of the PR is in Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean, everything else is just fixing errors.

For each `foo` in `zero`, `one`, `add`, `sub`, `neg`, smul` we do the following:
- add an instance `IsFooApply`
- rename `coe_foo` to `toLinearMap_foo`
- depreprecate `coe_foo`, `coe_foo'`, and `foo_apply`

We are rather conservative when it comes to the instances, in future PRs this will be used more.

For consistency, the same renaming has been applied to the `comp` variants. This resulted in a test being changed.
ReemMelamed pushed a commit to ReemMelamed/mathlib4 that referenced this pull request Jun 20, 2026
@mcdoll @ReemMelamed
feat(Topology/Algebra): use Is*Apply for ContinuousLinearMap (lea…
f7670fa 
…nprover-community#39637)

This is the first in many PRs that use the new `Is*Apply` classes instead of structure specific `foo_apply` lemmas.
The main bulk of the PR is in Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean, everything else is just fixing errors.

For each `foo` in `zero`, `one`, `add`, `sub`, `neg`, smul` we do the following:
- add an instance `IsFooApply`
- rename `coe_foo` to `toLinearMap_foo`
- depreprecate `coe_foo`, `coe_foo'`, and `foo_apply`

We are rather conservative when it comes to the instances, in future PRs this will be used more.

For consistency, the same renaming has been applied to the `comp` variants. This resulted in a test being changed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@j-loreaux j-loreaux j-loreaux left review comments

Assignees

@j-loreaux j-loreaux

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@mcdoll @leanprover-radar @j-loreaux