[Merged by Bors] - chore(Algebra.Order.Ring.Rat): split into unbundled and bundled ordered algebra results#15071
Closed
mattrobball wants to merge 2 commits intomasterfrom
Closed
[Merged by Bors] - chore(Algebra.Order.Ring.Rat): split into unbundled and bundled ordered algebra results#15071mattrobball wants to merge 2 commits intomasterfrom
mattrobball wants to merge 2 commits intomasterfrom
Conversation
PR summary 51253bc51c
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Algebra.Order.Ring.Rat | 394 | 386 | -8 (-2.03%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Algebra.Order.Ring.Rat |
-8 |
Mathlib.Data.Rat.Denumerable |
-1 |
2337 filesMathlib.Algebra.Homology.ShortComplex.Ab Mathlib.Data.Matroid.Basic Mathlib.LinearAlgebra.FreeModule.Norm Mathlib.LinearAlgebra.Charpoly.Basic Mathlib.Topology.Category.Stonean.Adjunctions Mathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.Analysis.Normed.Group.Uniform Mathlib.Data.Real.Hyperreal Mathlib.Algebra.Polynomial.FieldDivision Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.Analysis.MeanInequalitiesPow Mathlib.Topology.Algebra.Module.Simple Mathlib.Analysis.Asymptotics.SpecificAsymptotics Mathlib.Combinatorics.Additive.ErdosGinzburgZiv Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.RingTheory.IsAdjoinRoot Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.Topology.Algebra.InfiniteSum.Group Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Probability.Process.HittingTime Mathlib.Algebra.Module.Zlattice.Covolume Mathlib.Data.Nat.Choose.Cast Mathlib.NumberTheory.Liouville.LiouvilleWith Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.Analysis.InnerProductSpace.Symmetric Mathlib.Analysis.InnerProductSpace.OfNorm Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.Analysis.Calculus.Deriv.Pi Mathlib.RingTheory.Henselian Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.FieldTheory.IsPerfectClosure Mathlib.Analysis.Calculus.Deriv.Inv Mathlib.Topology.Category.LightProfinite.EffectiveEpi Mathlib.NumberTheory.Padics.PadicNorm Mathlib.Topology.Instances.Nat Mathlib.Algebra.Periodic Mathlib.Probability.BorelCantelli Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.NumberTheory.Wilson Mathlib.Geometry.Manifold.ContMDiff.Atlas Mathlib.Combinatorics.SetFamily.FourFunctions Mathlib.RingTheory.Polynomial.Content Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RingTheory.Localization.AtPrime Mathlib.MeasureTheory.MeasurableSpace.Embedding Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs Mathlib.Data.Real.Pointwise Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.RingTheory.PowerBasis Mathlib.Algebra.Symmetrized Mathlib.Algebra.Lie.Normalizer Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Geometry.Manifold.VectorBundle.Pullback Mathlib.FieldTheory.Finite.Trace Mathlib.FieldTheory.IntermediateField Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.MeasureTheory.Constructions.BorelSpace.Metric Mathlib.CategoryTheory.Abelian.RightDerived Mathlib.RingTheory.AlgebraTower Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual Mathlib.LinearAlgebra.Matrix.ZPow Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Topology.ContinuousFunction.CompactlySupported Mathlib.Algebra.Category.ModuleCat.Limits Mathlib.Analysis.Convex.AmpleSet Mathlib.RingTheory.Ideal.QuotientOperations Mathlib.Probability.Variance Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.Topology.MetricSpace.Antilipschitz Mathlib.Analysis.NormedSpace.OperatorNorm.Basic Mathlib.Analysis.Complex.Angle Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.RingTheory.SimpleModule Mathlib.Algebra.Category.FGModuleCat.Limits Mathlib.Topology.MetricSpace.Thickening Mathlib.Analysis.SpecialFunctions.Integrals Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue Mathlib.Dynamics.Ergodic.AddCircle Mathlib.AlgebraicTopology.SimplicialSet Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Probability.Distributions.Geometric Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.Analysis.Normed.Module.Dual Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.LinearAlgebra.ExteriorAlgebra.Grading Mathlib.Algebra.Polynomial.Degree.Definitions Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.Analysis.Subadditive Mathlib.NumberTheory.MulChar.Lemmas Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.Topology.Algebra.Order.Compact Mathlib.Data.W.Cardinal Mathlib.Algebra.Module.LocalizedModuleIntegers Mathlib.MeasureTheory.Integral.Marginal Mathlib.NumberTheory.Multiplicity Mathlib.RingTheory.PowerSeries.WellKnown Mathlib.GroupTheory.Perm.Cycle.PossibleTypes Mathlib.Geometry.Manifold.VectorBundle.Basic Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.LinearAlgebra.Projection Mathlib.Algebra.Category.Grp.EpiMono Mathlib.Algebra.Homology.Opposite Mathlib.Data.NNReal.Star Mathlib.Analysis.CStarAlgebra.Multiplier Mathlib.Topology.Algebra.UniformField Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.Analysis.SpecialFunctions.Pow.Complex Mathlib.Analysis.Calculus.Deriv.Star Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.Algebra.Module.Bimodule Mathlib.Tactic.FunProp.ContDiff Mathlib.AlgebraicGeometry.PrimeSpectrum.TensorProduct Mathlib.MeasureTheory.Function.SpecialFunctions.Basic Mathlib.LinearAlgebra.SModEq Mathlib.Data.NNRat.BigOperators Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Algebra.Category.Grp.Subobject Mathlib.Analysis.Normed.Lp.PiLp Mathlib.RingTheory.WittVector.Domain Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.Topology.Homotopy.Contractible Mathlib.Tactic.Positivity.Finset Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.Algebra.ContinuedFractions.Computation.Translations Mathlib.Geometry.Manifold.VectorBundle.Tangent Mathlib.RingTheory.Artinian Mathlib.Analysis.Calculus.Deriv.Add Mathlib.Topology.Instances.PNat Mathlib.LinearAlgebra.Matrix.MvPolynomial Mathlib.FieldTheory.Laurent Mathlib.Analysis.Normed.Lp.WithLp Mathlib.Analysis.SpecialFunctions.CompareExp Mathlib.MeasureTheory.Function.UnifTight Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit Mathlib.NumberTheory.GaussSum Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.NumberTheory.Primorial Mathlib.Topology.Algebra.Module.UniformConvergence Mathlib.Tactic.IntervalCases Mathlib.Algebra.Category.Ring.Instances Mathlib.Data.NNReal.Basic Mathlib.Algebra.Lie.Quotient Mathlib.Algebra.Category.CoalgebraCat.ComonEquivalence Mathlib.Geometry.Manifold.Diffeomorph Mathlib.Combinatorics.Derangements.Exponential Mathlib.LinearAlgebra.Dimension.DivisionRing Mathlib.LinearAlgebra.FreeModule.StrongRankCondition Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.MeasureTheory.Function.LpSeminorm.Basic Mathlib.Topology.Category.Profinite.CofilteredLimit Mathlib.NumberTheory.EllipticDivisibilitySequence Mathlib.Condensed.Limits Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.LinearAlgebra.BilinearForm.DualLattice Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.RingTheory.DedekindDomain.Ideal Mathlib.MeasureTheory.OuterMeasure.Caratheodory Mathlib.Algebra.Category.ModuleCat.Abelian Mathlib.Topology.MetricSpace.ShrinkingLemma Mathlib.RingTheory.Ideal.IsPrincipal Mathlib.Analysis.SpecialFunctions.Complex.Log Mathlib.MeasureTheory.Constructions.BorelSpace.Basic Mathlib.Probability.ProbabilityMassFunction.Monad Mathlib.MeasureTheory.OuterMeasure.Induced Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology Mathlib.MeasureTheory.Measure.Regular Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.Analysis.Asymptotics.AsymptoticEquivalent Mathlib.Algebra.Order.BigOperators.Ring.Finset Mathlib.MeasureTheory.Group.MeasurableEquiv Mathlib.CategoryTheory.Abelian.Ext Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.Analysis.Complex.AbsMax Mathlib.RingTheory.Ideal.Over Mathlib.RingTheory.Flat.Basic Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter Mathlib.RingTheory.GradedAlgebra.Noetherian Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Combinatorics.SimpleGraph.StronglyRegular Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.Data.Nat.Factorial.DoubleFactorial Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Data.Real.GoldenRatio Mathlib.MeasureTheory.Order.Lattice Mathlib.RingTheory.QuotSMulTop Mathlib.RingTheory.WittVector.InitTail Mathlib.Condensed.TopComparison Mathlib.Geometry.Manifold.MFDeriv.Basic Mathlib.Topology.Algebra.Group.OpenMapping Mathlib.Data.Rat.Floor Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Data.Finsupp.PWO Mathlib.Algebra.Category.ModuleCat.Kernels Mathlib.Analysis.Hofer Mathlib.RingTheory.Valuation.ExtendToLocalization Mathlib.LinearAlgebra.Dimension.Localization Mathlib.Geometry.Manifold.Instances.Real Mathlib.RingTheory.Localization.NormTrace Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.LinearAlgebra.Lagrange Mathlib.ModelTheory.PartialEquiv Mathlib.RingTheory.AdicCompletion.Basic Mathlib.Topology.Instances.Int Mathlib.Analysis.Convex.Topology Mathlib.Topology.MetricSpace.Pseudo.Real Mathlib.Condensed.Discrete.Basic Mathlib.Geometry.Manifold.Complex Mathlib.Logic.Hydra Mathlib.LinearAlgebra.Coevaluation Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.Algebra.Lie.Submodule Mathlib.FieldTheory.AbelRuffini Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.RingTheory.ClassGroup Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.RingTheory.Ideal.Maps Mathlib.Analysis.Calculus.FDeriv.Linear Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.GroupTheory.DoubleCoset Mathlib.Probability.StrongLaw Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital Mathlib.Algebra.Category.Grp.AB5 Mathlib.Data.Real.ENatENNReal Mathlib.GroupTheory.Perm.Sign Mathlib.Topology.Algebra.Ring.Basic Mathlib.RingTheory.Regular.RegularSequence Mathlib.Analysis.Normed.Module.FiniteDimension Mathlib.Topology.FiberBundle.Constructions Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.LinearAlgebra.Matrix.Diagonal Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.RingTheory.Multiplicity Mathlib.RingTheory.Derivation.Lie Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Data.ZMod.Module Mathlib.RingTheory.Polynomial.Pochhammer Mathlib.Analysis.Complex.HalfPlane Mathlib.Analysis.LocallyConvex.Bounded Mathlib.Algebra.Module.DedekindDomain Mathlib.RingTheory.Trace.Defs Mathlib.RingTheory.WittVector.Compare Mathlib.GroupTheory.Perm.Cycle.Basic Mathlib.Algebra.Polynomial.SpecificDegree Mathlib.Algebra.MvPolynomial.Counit Mathlib.Data.Int.AbsoluteValue Mathlib.LinearAlgebra.Eigenspace.Matrix Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.Algebra.Homology.Embedding.IsSupported Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.Algebra.MvPolynomial.Basic Mathlib.Analysis.Seminorm Mathlib.Analysis.Complex.Isometry Mathlib.MeasureTheory.Measure.AEDisjoint Mathlib.SetTheory.Ordinal.Notation Mathlib.RingTheory.Adjoin.PowerBasis Mathlib.Geometry.Manifold.MFDeriv.FDeriv Mathlib.GroupTheory.Coset Mathlib.Analysis.Convex.Side Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.NumberTheory.ArithmeticFunction Mathlib.MeasureTheory.Function.L2Space Mathlib.Algebra.ContinuedFractions.Computation.Approximations Mathlib.Topology.VectorBundle.Hom Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.Analysis.Complex.UnitDisc.Basic Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.Topology.Instances.CantorSet Mathlib.Analysis.SpecialFunctions.Exp Mathlib.Algebra.Polynomial.AlgebraMap Mathlib.RingTheory.Polynomial.Quotient Mathlib.RingTheory.AdicCompletion.Functoriality Mathlib.Topology.Bornology.BoundedOperation Mathlib.Algebra.CharP.LocalRing Mathlib.LinearAlgebra.Matrix.Reindex Mathlib.LinearAlgebra.PID Mathlib.Data.Matroid.Map Mathlib.RingTheory.LaurentSeries Mathlib.NumberTheory.ModularForms.Identities Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.Analysis.Normed.Group.CocompactMap Mathlib.Computability.AkraBazzi.GrowsPolynomially Mathlib.Geometry.Manifold.ContMDiffMap Mathlib.Algebra.MvPolynomial.Funext Mathlib.CategoryTheory.Galois.GaloisObjects Mathlib.NumberTheory.NumberField.Norm Mathlib.Analysis.Convex.Body Mathlib.Topology.Category.Profinite.Nobeling Mathlib.Analysis.NormedSpace.RCLike Mathlib.LinearAlgebra.FreeModule.Determinant Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Condensed.Light.Explicit Mathlib.Algebra.Algebra.Subalgebra.Operations Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions Mathlib.Probability.CondCount Mathlib.SetTheory.Game.Short Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.Algebra.Ring.Divisibility.Lemmas Mathlib.Data.Real.Sqrt Mathlib.Topology.ContinuousFunction.Ideals Mathlib.Tactic.Positivity Mathlib.LinearAlgebra.QuadraticForm.Prod Mathlib.FieldTheory.Galois Mathlib.RingTheory.Trace.Basic Mathlib.LinearAlgebra.TensorAlgebra.Grading Mathlib.SetTheory.Cardinal.Finsupp Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas Mathlib.RingTheory.Bialgebra.Hom Mathlib.GroupTheory.OrderOfElement Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev Mathlib.NumberTheory.FLT.Four Mathlib.Algebra.Polynomial.HasseDeriv Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated Mathlib.Probability.Distributions.Exponential Mathlib.Algebra.RingQuot Mathlib.RingTheory.WittVector.MulCoeff Mathlib.RingTheory.RingHom.FiniteType Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.Analysis.Calculus.FormalMultilinearSeries Mathlib.MeasureTheory.Order.Group.Lattice Mathlib.Topology.Germ Mathlib.Data.ENNReal.Inv Mathlib.Topology.MetricSpace.Sequences Mathlib.Topology.Algebra.Group.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation Mathlib.Analysis.Calculus.AddTorsor.AffineMap Mathlib.Topology.Algebra.InfiniteSum.ENNReal Mathlib.RingTheory.Localization.BaseChange Mathlib.Algebra.Lie.Nilpotent Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.LinearAlgebra.Charpoly.ToMatrix Mathlib.FieldTheory.Normal Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.RingTheory.DiscreteValuationRing.Basic Mathlib.CategoryTheory.Triangulated.Pretriangulated Mathlib.MeasureTheory.Group.Measure Mathlib.Topology.Order.ExtendFrom Mathlib.GroupTheory.FreeAbelianGroupFinsupp Mathlib.Probability.Kernel.Composition Mathlib.NumberTheory.Liouville.LiouvilleNumber Mathlib.NumberTheory.Zsqrtd.ToReal Mathlib.Algebra.Category.Grp.Abelian Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.Dynamics.OmegaLimit Mathlib.NumberTheory.ADEInequality Mathlib.Data.Real.ConjExponents Mathlib.RingTheory.Localization.Ideal Mathlib.RingTheory.Polynomial.Opposites Mathlib.LinearAlgebra.FreeModule.IdealQuotient Mathlib.SetTheory.Cardinal.Divisibility Mathlib.GroupTheory.Perm.Closure Mathlib.RingTheory.Polynomial.Tower Mathlib.GroupTheory.Abelianization Mathlib.Algebra.Order.Floor Mathlib.AlgebraicTopology.CechNerve Mathlib.Algebra.Category.AlgebraCat.Limits Mathlib.Probability.Martingale.Upcrossing Mathlib.AlgebraicTopology.Quasicategory Mathlib.Order.JordanHolder Mathlib.RingTheory.Coalgebra.Basic Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.RingTheory.Jacobson Mathlib.Analysis.RCLike.Lemmas Mathlib.Combinatorics.SetFamily.AhlswedeZhang Mathlib.Algebra.Quaternion Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv Mathlib.Condensed.Explicit Mathlib.NumberTheory.MulChar.Basic Mathlib.Data.Nat.Choose.Lucas Mathlib.Algebra.Polynomial.Splits Mathlib.Algebra.Algebra.Subalgebra.Tower Mathlib.Probability.Martingale.OptionalSampling Mathlib.RingTheory.Localization.AsSubring Mathlib.RingTheory.Norm.Defs Mathlib.Analysis.BoxIntegral.Box.Basic Mathlib.RingTheory.Kaehler.Polynomial Mathlib.GroupTheory.Exponent Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.RingTheory.Localization.Finiteness Mathlib.RingTheory.WittVector.Identities Mathlib.Condensed.Module Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.Data.Real.Sign Mathlib.Analysis.Calculus.FDeriv.Analytic Mathlib.Analysis.Convex.GaugeRescale Mathlib.FieldTheory.Minpoly.Basic Mathlib.FieldTheory.Adjoin Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.NumberTheory.NumberField.Discriminant Mathlib.GroupTheory.Solvable Mathlib.Algebra.Category.Grp.Kernels Mathlib.RingTheory.Polynomial.Dickson Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.Analysis.Calculus.BumpFunction.Basic Mathlib.Analysis.Calculus.FDeriv.Star Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.Algebra.MvPolynomial.Expand Mathlib.Analysis.Oscillation Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.Topology.ContinuousFunction.ContinuousMapZero Mathlib.LinearAlgebra.Matrix.Gershgorin Mathlib.Algebra.DualQuaternion Mathlib.RingTheory.Localization.Integral Mathlib.Analysis.NormedSpace.RieszLemma Mathlib.ModelTheory.Substructures Mathlib.Analysis.Calculus.FDeriv.Bilinear Mathlib.Algebra.Lie.Derivation.Killing Mathlib.RingTheory.AdicCompletion.Exactness Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift Mathlib.FieldTheory.SeparableClosure Mathlib.Analysis.Complex.Circle Mathlib.Topology.Algebra.Nonarchimedean.Completion Mathlib.Data.ZMod.Quotient Mathlib.ModelTheory.FinitelyGenerated Mathlib.RingTheory.WittVector.Truncated Mathlib.Algebra.Exact Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.Algebra.Order.Floor.Div Mathlib.MeasureTheory.OuterMeasure.OfFunction Mathlib.NumberTheory.RamificationInertia Mathlib.Data.Nat.Squarefree Mathlib.Algebra.Homology.HomotopyCategory.MappingCone Mathlib.Topology.MetricSpace.PartitionOfUnity Mathlib.NumberTheory.SiegelsLemma Mathlib.Analysis.SpecialFunctions.PolynomialExp Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.LinearAlgebra.JordanChevalley Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.Algebra.Category.ModuleCat.Injective Mathlib.Data.Nat.Factorization.Induction Mathlib.Analysis.InnerProductSpace.Dual Mathlib.Topology.ContinuousFunction.Polynomial Mathlib.FieldTheory.ChevalleyWarning Mathlib.RingTheory.Polynomial.Hermite.Gaussian Mathlib.MeasureTheory.Covering.VitaliFamily Mathlib.FieldTheory.IsAlgClosed.Classification Mathlib.LinearAlgebra.QuadraticForm.Basic Mathlib.Analysis.LocallyConvex.Barrelled Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary Mathlib.Analysis.Calculus.AddTorsor.Coord Mathlib.NumberTheory.ClassNumber.AdmissibleAbs Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.LinearAlgebra.QuadraticForm.Basis Mathlib.RepresentationTheory.Rep Mathlib.Analysis.Calculus.Deriv.Linear Mathlib.Data.Matroid.Dual Mathlib.AlgebraicGeometry.EllipticCurve.Affine Mathlib.AlgebraicGeometry.EllipticCurve.Group Mathlib.Algebra.Star.Subalgebra Mathlib.NumberTheory.Padics.PadicNumbers Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.LinearAlgebra.Matrix.Determinant.Misc Mathlib.MeasureTheory.Measure.ContinuousPreimage Mathlib.Data.Finsupp.Weight Mathlib.MeasureTheory.Function.LpSeminorm.Trim Mathlib.Algebra.Quandle Mathlib.Analysis.PSeries Mathlib.Analysis.Fourier.ZMod Mathlib.LinearAlgebra.Multilinear.Basic Mathlib.NumberTheory.Harmonic.Defs Mathlib.ModelTheory.Complexity Mathlib.Algebra.Homology.BifunctorFlip Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.MeasureTheory.Function.LpSpace Mathlib.MeasureTheory.Group.Arithmetic Mathlib.NumberTheory.ModularForms.SlashActions Mathlib.RingTheory.Polynomial.Hermite.Basic Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.LinearAlgebra.Multilinear.Basis Mathlib.Algebra.Homology.TotalComplexShift Mathlib.CategoryTheory.Abelian.ProjectiveResolution Mathlib.Combinatorics.SimpleGraph.Triangle.Counting Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.Dynamics.Ergodic.MeasurePreserving Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity Mathlib.GroupTheory.Divisible Mathlib.Algebra.CubicDiscriminant Mathlib.Topology.Order.ProjIcc Mathlib.Combinatorics.SimpleGraph.Density Mathlib.RingTheory.PrincipalIdealDomain Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat Mathlib.Analysis.Calculus.SmoothSeries Mathlib.RingTheory.Ideal.MinimalPrime Mathlib.GroupTheory.Nilpotent Mathlib.Topology.MetricSpace.Cauchy Mathlib.RingTheory.Bialgebra.Basic Mathlib.GroupTheory.FreeGroup.NielsenSchreier Mathlib.Topology.EMetricSpace.Defs Mathlib.RingTheory.WittVector.WittPolynomial Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff Mathlib.GroupTheory.CommutingProbability Mathlib.Algebra.Lie.Free Mathlib.Analysis.Calculus.FDeriv.Add Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Topology.Algebra.InfiniteSum.Module Mathlib.Analysis.Complex.Basic Mathlib.MeasureTheory.Function.AEMeasurableOrder Mathlib.Analysis.Convex.Intrinsic Mathlib.Topology.MetricSpace.Lipschitz Mathlib.Analysis.Calculus.Deriv.Polynomial Mathlib.LinearAlgebra.BilinearForm.Orthogonal Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.GroupTheory.Coxeter.Basic Mathlib.GroupTheory.NoncommPiCoprod Mathlib.RingTheory.Polynomial.IrreducibleRing Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.AlgebraicGeometry.Spec Mathlib.MeasureTheory.Category.MeasCat Mathlib.NumberTheory.Cyclotomic.Three Mathlib.Analysis.Calculus.TangentCone Mathlib.Probability.Kernel.Disintegration.Integral Mathlib.RingTheory.RingHom.Finite Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.Combinatorics.Additive.Energy Mathlib.RingTheory.EssentialFiniteness Mathlib.Algebra.Order.ToIntervalMod Mathlib.Algebra.GCDMonoid.IntegrallyClosed Mathlib.Algebra.Polynomial.Inductions Mathlib.LinearAlgebra.PerfectPairing Mathlib.Topology.Category.Profinite.EffectiveEpi Mathlib.Data.Nat.Periodic Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.FieldTheory.SeparableDegree Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.Topology.Instances.Discrete Mathlib.FieldTheory.Minpoly.MinpolyDiv Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.RingTheory.PowerSeries.Derivative Mathlib.NumberTheory.LSeries.Deriv Mathlib.MeasureTheory.Constructions.Pi Mathlib.Analysis.Normed.Order.UpperLower Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap Mathlib.Topology.MetricSpace.GromovHausdorffRealized Mathlib.Analysis.Normed.Group.SemiNormedGrp Mathlib.RingTheory.Ideal.Cotangent Mathlib.NumberTheory.EulerProduct.Basic Mathlib.Analysis.Fourier.AddCircle Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.MeasureTheory.Decomposition.UnsignedHahn Mathlib.LinearAlgebra.QuotientPi Mathlib.RingTheory.Nullstellensatz Mathlib.RingTheory.Noetherian Mathlib.Analysis.Normed.Algebra.Unitization Mathlib.Topology.Sheaves.LocalPredicate Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar Mathlib.Analysis.SpecialFunctions.Pow.Continuity Mathlib.Analysis.Calculus.MeanValue Mathlib.GroupTheory.SchurZassenhaus Mathlib.LinearAlgebra.Matrix.Polynomial Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.Analysis.Calculus.FDeriv.Basic Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly Mathlib.Algebra.Lie.CartanSubalgebra Mathlib.LinearAlgebra.Trace Mathlib.Topology.MetricSpace.Pseudo.Basic Mathlib.Analysis.Calculus.FDeriv.Pi Mathlib.CategoryTheory.Action Mathlib.Algebra.Polynomial.DenomsClearable Mathlib.LinearAlgebra.FreeModule.PID Mathlib.Topology.UniformSpace.CompareReals Mathlib.Dynamics.Ergodic.Conservative Mathlib.Algebra.Lie.IdealOperations Mathlib.Algebra.Vertex.HVertexOperator Mathlib.CategoryTheory.Triangulated.Triangulated Mathlib.Analysis.BoxIntegral.Box.SubboxInduction Mathlib.Algebra.Algebra.Subalgebra.Rank Mathlib.Topology.Instances.AddCircle Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv Mathlib.Topology.ContinuousFunction.Algebra Mathlib.Analysis.Convex.Slope Mathlib.Topology.Order.Monotone Mathlib.Probability.Kernel.WithDensity Mathlib.Analysis.Normed.Affine.Isometry Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.Topology.Category.Profinite.AsLimit Mathlib.RingTheory.Ideal.Quotient Mathlib.Topology.Algebra.Valued.NormedValued Mathlib.Combinatorics.SimpleGraph.Triangle.Basic Mathlib.LinearAlgebra.Matrix.FiniteDimensional Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.Analysis.Calculus.Deriv.Pow Mathlib.FieldTheory.Fixed Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic Mathlib.RingTheory.Adjoin.Field Mathlib.Data.Nat.Factorization.Defs Mathlib.GroupTheory.Perm.Fin Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.AlgebraicGeometry.Pullbacks Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp Mathlib.Topology.Order.Bounded Mathlib.Data.Matrix.CharP Mathlib.RingTheory.Derivation.Basic Mathlib.RingTheory.Localization.Away.Basic Mathlib.Topology.Homotopy.Path Mathlib.Topology.Algebra.Order.Field Mathlib.FieldTheory.Finite.Basic Mathlib.GroupTheory.Commutator Mathlib.Topology.Algebra.InfiniteSum.NatInt Mathlib.Topology.Algebra.Module.FiniteDimension Mathlib.Algebra.Polynomial.RingDivision Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.Combinatorics.Derangements.Basic Mathlib.Analysis.Normed.Field.Basic Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.Algebra.Algebra.Operations Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.Analysis.Calculus.Taylor Mathlib.Algebra.AddConstMap.Equiv Mathlib.NumberTheory.DirichletCharacter.Basic Mathlib.MeasureTheory.Group.AddCircle Mathlib.Data.ZMod.Coprime Mathlib.Probability.Independence.ZeroOne Mathlib.Topology.CompletelyRegular Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.Combinatorics.SimpleGraph.Regularity.Increment Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.Algebra.Lie.TraceForm Mathlib.Analysis.Calculus.LHopital Mathlib.Analysis.Convex.Cone.Pointed Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.Algebra.Algebra.Subalgebra.Prod Mathlib.MeasureTheory.Function.UniformIntegrable Mathlib.Tactic.NormNum.NatFib Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv Mathlib.AlgebraicTopology.DoldKan.GammaCompN Mathlib.MeasureTheory.Measure.Hausdorff Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.Data.Complex.Exponential Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion Mathlib.GroupTheory.Perm.Cycle.Factors Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.Algebra.Homology.DerivedCategory.Ext Mathlib.NumberTheory.ModularForms.SlashInvariantForms Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected Mathlib.Geometry.Manifold.SmoothManifoldWithCorners Mathlib.Condensed.Basic Mathlib.MeasureTheory.Measure.NullMeasurable Mathlib.FieldTheory.SplittingField.IsSplittingField Mathlib.Algebra.Polynomial.Taylor Mathlib.FieldTheory.IsSepClosed Mathlib.Algebra.Lie.Killing Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs Mathlib.Analysis.Normed.Operator.BanachSteinhaus Mathlib.Algebra.Lie.Derivation.AdjointAction Mathlib.AlgebraicTopology.FundamentalGroupoid.Product Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict Mathlib.NumberTheory.FrobeniusNumber Mathlib.RingTheory.Polynomial.IntegralNormalization Mathlib.ModelTheory.Graph Mathlib.Probability.Distributions.Gaussian Mathlib.Probability.Kernel.CondDistrib Mathlib.Condensed.Light.TopComparison Mathlib.Topology.MetricSpace.Dilation Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Analysis.SpecificLimits.FloorPow Mathlib.CategoryTheory.Preadditive.Yoneda.Injective Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.GroupTheory.GroupAction.Period Mathlib.Analysis.Calculus.UniformLimitsDeriv Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear Mathlib.NumberTheory.PellMatiyasevic Mathlib.RingTheory.RootsOfUnity.Lemmas Mathlib.MeasureTheory.Integral.Bochner Mathlib.Algebra.Lie.Character Mathlib.Topology.ContinuousFunction.StarOrdered Mathlib.RingTheory.Presentation Mathlib.Analysis.LocallyConvex.Basic Mathlib.ModelTheory.Encoding Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.Geometry.Manifold.BumpFunction Mathlib.Analysis.Calculus.FDeriv.Extend Mathlib.Algebra.Lie.DirectSum Mathlib.GroupTheory.Perm.Option Mathlib.Probability.Martingale.Basic Mathlib.RingTheory.MvPolynomial.Homogeneous Mathlib.Analysis.LocallyConvex.WeakDual Mathlib.RingTheory.Coprime.Ideal Mathlib.Data.Finsupp.Antidiagonal Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.Algebra.Squarefree.Basic Mathlib.Analysis.Normed.Module.Span Mathlib.Algebra.Polynomial.Expand Mathlib.RingTheory.FractionalIdeal.Basic Mathlib.Analysis.Normed.Affine.MazurUlam Mathlib.FieldTheory.Finite.Polynomial Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.Topology.MetricSpace.ProperSpace Mathlib.CategoryTheory.Triangulated.HomologicalFunctor Mathlib.MeasureTheory.Measure.Content Mathlib.LinearAlgebra.FiniteDimensional Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.RingTheory.MvPolynomial.Ideal Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup Mathlib.Probability.Kernel.RadonNikodym Mathlib.RingTheory.Polynomial.Vieta Mathlib.RingTheory.Kaehler.CotangentComplex Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.Geometry.Manifold.InteriorBoundary Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor Mathlib.Combinatorics.Additive.PluenneckeRuzsa Mathlib.FieldTheory.Extension Mathlib.Topology.Order.Filter Mathlib.LinearAlgebra.Orientation Mathlib.Topology.Homotopy.Basic Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.Algebra.DirectSum.Internal Mathlib.RingTheory.Derivation.ToSquareZero Mathlib.NumberTheory.LSeries.Basic Mathlib.RingTheory.Valuation.ValuationRing Mathlib.Geometry.Manifold.ContMDiffMFDeriv Mathlib.Analysis.LocallyConvex.AbsConvex Mathlib.Analysis.Normed.Ring.SeminormFromConst Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels Mathlib.MeasureTheory.Decomposition.SignedLebesgue Mathlib.NumberTheory.SumFourSquares Mathlib.Topology.UrysohnsBounded Mathlib.LinearAlgebra.Matrix.ToLin Mathlib.Combinatorics.Configuration Mathlib.AlgebraicGeometry.Properties Mathlib.Analysis.Convex.StrictConvexSpace Mathlib.MeasureTheory.Decomposition.Exhaustion Mathlib.Geometry.Manifold.ContMDiff.Basic Mathlib.Data.ZMod.IntUnitsPower Mathlib.MeasureTheory.Measure.WithDensityFinite Mathlib.MeasureTheory.Measure.Sub Mathlib.Geometry.Euclidean.Sphere.Power Mathlib.Topology.Homotopy.Product Mathlib.Topology.Instances.Real Mathlib.RingTheory.FinitePresentation Mathlib.Data.Ordmap.Ordset Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Topology.Metrizable.Urysohn Mathlib.Analysis.Convex.SimplicialComplex.Basic Mathlib.RingTheory.IntegralClosure.Algebra.Defs Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal Mathlib.LinearAlgebra.Semisimple Mathlib.Algebra.Order.Module.Rat Mathlib.FieldTheory.AbsoluteGaloisGroup Mathlib.LinearAlgebra.RootSystem.Basic Mathlib.LinearAlgebra.FreeModule.Finite.Basic Mathlib.Algebra.Lie.Weights.Basic Mathlib.MeasureTheory.Measure.HasOuterApproxClosed Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.Analysis.Normed.Group.Tannery Mathlib.Analysis.Calculus.ContDiff.Defs Mathlib.AlgebraicTopology.SimplicialSet.Monoidal Mathlib.Algebra.Algebra.Subalgebra.Order Mathlib.Topology.Order.Basic Mathlib.Analysis.SpecialFunctions.Pow.Deriv Mathlib.Algebra.CharP.Basic Mathlib.Topology.Algebra.Equicontinuity Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.SetTheory.Ordinal.Topology Mathlib.Data.Rat.Cast.Order Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.MeasureTheory.Measure.GiryMonad Mathlib.RingTheory.PiTensorProduct Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.RingTheory.Flat.Algebra Mathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Probability.ProbabilityMassFunction.Constructions Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.Complex.UpperHalfPlane.Topology Mathlib.RepresentationTheory.Invariants Mathlib.RingTheory.Valuation.Integral Mathlib.GroupTheory.Perm.DomMulAct Mathlib.RingTheory.Coalgebra.Hom Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.RingTheory.Flat.CategoryTheory Mathlib.RingTheory.MvPolynomial.Localization Mathlib.RingTheory.Localization.LocalizationLocalization Mathlib.Analysis.SpecialFunctions.Log.Base Mathlib.NumberTheory.Rayleigh Mathlib.MeasureTheory.Order.UpperLower Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.Combinatorics.Additive.RuzsaCovering Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.Probability.Martingale.Convergence Mathlib.Condensed.Solid Mathlib.Analysis.Convex.SpecificFunctions.Pow Mathlib.FieldTheory.KrullTopology Mathlib.Analysis.Complex.UpperHalfPlane.Metric Mathlib.RingTheory.LittleWedderburn Mathlib.Analysis.Normed.Lp.lpSpace Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential Mathlib.Algebra.Homology.HomotopyCategory.Triangulated Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.RingTheory.LocalRing.Basic Mathlib.Analysis.Normed.Group.Seminorm Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner Mathlib.Topology.Category.LightProfinite.AsLimit Mathlib.Probability.Kernel.IntegralCompProd Mathlib.LinearAlgebra.TensorAlgebra.Basic Mathlib.RingTheory.Localization.Submodule Mathlib.RingTheory.Radical Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.RingTheory.Localization.Integer Mathlib.LinearAlgebra.TensorAlgebra.Basis Mathlib.GroupTheory.ClassEquation Mathlib.Topology.Category.LightProfinite.Limits Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.Analysis.NormedSpace.OperatorNorm.Mul Mathlib.Analysis.Normed.Group.Quotient Mathlib.Topology.Category.CompHaus.Basic Mathlib.CategoryTheory.Preadditive.Schur Mathlib.Analysis.Normed.Ring.Seminorm Mathlib.Algebra.Order.CauSeq.Completion Mathlib.RingTheory.Generators Mathlib.Analysis.InnerProductSpace.Basic Mathlib.RingTheory.Adjoin.Tower Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.Combinatorics.SimpleGraph.Regularity.Energy Mathlib.Analysis.Complex.OperatorNorm Mathlib.Data.Complex.Determinant Mathlib.Order.Filter.ZeroAndBoundedAtFilter Mathlib.AlgebraicTopology.SingularSet Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov Mathlib.NumberTheory.Zsqrtd.GaussianInt Mathlib.Analysis.PSeriesComplex Mathlib.RingTheory.PolynomialAlgebra Mathlib.LinearAlgebra.Alternating.DomCoprod Mathlib.RingTheory.QuotientNilpotent Mathlib.Algebra.Category.CoalgebraCat.Basic Mathlib.Algebra.ContinuedFractions.Computation.Basic Mathlib.Topology.MetricSpace.IsometricSMul Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.Probability.Kernel.Disintegration.Density Mathlib.Analysis.Calculus.LagrangeMultipliers Mathlib.Topology.Algebra.UniformMulAction Mathlib.LinearAlgebra.BilinearForm.Properties Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.Analysis.Calculus.Deriv.ZPow Mathlib.Algebra.Polynomial.Mirror Mathlib.LinearAlgebra.TensorProduct.Finiteness Mathlib.Analysis.Convex.Integral Mathlib.Topology.MetricSpace.Pseudo.Pi Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.LinearAlgebra.FiniteDimensional.Defs Mathlib.GroupTheory.QuotientGroup Mathlib.Topology.MetricSpace.Equicontinuity Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.Topology.Category.CompHaus.Projective Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace Mathlib.RingTheory.Nilpotent.Lemmas Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors Mathlib.MeasureTheory.Measure.Trim Mathlib.RingTheory.Polynomial.Bernstein Mathlib.Analysis.Normed.Group.Completeness Mathlib.Analysis.Normed.Group.ZeroAtInfty Mathlib.Algebra.LinearRecurrence Mathlib.MeasureTheory.Constructions.Prod.Integral Mathlib.LinearAlgebra.TensorProduct.Subalgebra Mathlib.Topology.Algebra.StarSubalgebra Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian Mathlib.GroupTheory.FiniteAbelian Mathlib.Analysis.LocallyConvex.StrongTopology Mathlib.Topology.MetricSpace.Ultra.Basic Mathlib.Analysis.Convex.Cone.Extension Mathlib.Algebra.Polynomial.PartialFractions Mathlib.Topology.UniformSpace.Matrix Mathlib.NumberTheory.PythagoreanTriples Mathlib.LinearAlgebra.CliffordAlgebra.Star Mathlib.Algebra.MonoidAlgebra.Ideal Mathlib.Topology.MetricSpace.Isometry Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.Tactic.Linarith Mathlib.Algebra.MvPolynomial.Rename Mathlib.Data.Int.Log Mathlib.LinearAlgebra.AffineSpace.Basis Mathlib.Analysis.NormedSpace.ConformalLinearMap Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.MeasureTheory.Integral.Layercake Mathlib.LinearAlgebra.Matrix.DotProduct Mathlib.MeasureTheory.Decomposition.Jordan Mathlib.Condensed.Light.Epi Mathlib.Analysis.BoxIntegral.Partition.Additive Mathlib.Analysis.Complex.ReImTopology Mathlib.RingTheory.ZMod Mathlib.Algebra.Polynomial.Monic Mathlib.Geometry.Euclidean.Circumcenter Mathlib.LinearAlgebra.Matrix.Nondegenerate Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Algebra.Module.Projective Mathlib.Analysis.Calculus.Deriv.Basic Mathlib.LinearAlgebra.CrossProduct Mathlib.Analysis.Complex.Schwarz Mathlib.NumberTheory.LegendreSymbol.Basic Mathlib.RingTheory.Adjoin.FG Mathlib.Data.Nat.Choose.Vandermonde Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics Mathlib.CategoryTheory.Abelian.Injective Mathlib.Dynamics.Newton Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.RingTheory.FiniteStability Mathlib.RingTheory.Localization.InvSubmonoid Mathlib.Analysis.Calculus.DiffContOnCl Mathlib.Algebra.BigOperators.Intervals Mathlib.Analysis.Complex.UpperHalfPlane.Manifold Mathlib.Analysis.Convex.Join Mathlib.Tactic.CancelDenoms Mathlib.LinearAlgebra.Matrix.Permutation Mathlib.LinearAlgebra.TensorProduct.Matrix Mathlib.Analysis.SpecialFunctions.Complex.Arg Mathlib.Topology.Category.Profinite.Projective Mathlib.Topology.PartitionOfUnity Mathlib.Algebra.Polynomial.Coeff Mathlib.Analysis.NormedSpace.Multilinear.Curry Mathlib.CategoryTheory.Monoidal.Tor Mathlib.FieldTheory.Finite.GaloisField Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.Algebra.Algebra.Subalgebra.Pointwise Mathlib.FieldTheory.MvPolynomial Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic Mathlib.RepresentationTheory.Character Mathlib.AlgebraicGeometry.PrimeSpectrum.Module Mathlib.Algebra.Order.Floor.Prime Mathlib.Analysis.SumOverResidueClass Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.NumberTheory.SmoothNumbers Mathlib.Algebra.MvPolynomial.Derivation Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.MeasureTheory.Covering.OneDim Mathlib.Topology.TietzeExtension Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower Mathlib.Data.Real.Pi.Leibniz Mathlib.LinearAlgebra.QuadraticForm.Real Mathlib.Algebra.Category.Grp.Adjunctions Mathlib.LinearAlgebra.CliffordAlgebra.Equivs Mathlib.Algebra.Order.EuclideanAbsoluteValue Mathlib.Algebra.MvPolynomial.Variables Mathlib.RingTheory.DedekindDomain.IntegralClosure Mathlib.Algebra.Order.Chebyshev Mathlib.RepresentationTheory.Basic Mathlib.CategoryTheory.Galois.Decomposition Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.NumberTheory.FLT.Three Mathlib.RingTheory.WittVector.Verschiebung Mathlib.RingTheory.Filtration Mathlib.Testing.SlimCheck.Functions Mathlib.Geometry.Manifold.Algebra.SmoothFunctions Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Algebra.Lie.SkewAdjoint Mathlib.Analysis.Normed.Group.BallSphere Mathlib.Analysis.SpecialFunctions.Polynomials Mathlib.Topology.MetricSpace.Polish Mathlib.RingTheory.Nakayama Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic Mathlib.GroupTheory.CosetCover Mathlib.LinearAlgebra.LinearDisjoint Mathlib.Topology.MetricSpace.Infsep Mathlib.Analysis.CStarAlgebra.Unitization Mathlib.Analysis.InnerProductSpace.Positive Mathlib.Topology.Category.Profinite.Basic Mathlib.Tactic.NormNum.Ineq Mathlib.CategoryTheory.Abelian.Projective Mathlib.LinearAlgebra.CliffordAlgebra.Fold Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.LinearAlgebra.FreeModule.Finite.Matrix Mathlib.LinearAlgebra.Matrix.Charpoly.Basic Mathlib.Topology.Algebra.Module.Multilinear.Basic Mathlib.Algebra.Lie.Weights.Chain Mathlib.MeasureTheory.Group.LIntegral Mathlib.Topology.Instances.Rat Mathlib.Algebra.Homology.HomotopyCategory.HomComplex Mathlib.RingTheory.Algebraic Mathlib.Topology.Algebra.ProperAction Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital Mathlib.Algebra.Polynomial.Derivation Mathlib.SetTheory.Cardinal.Cofinality Mathlib.Probability.Kernel.Invariance Mathlib.Topology.Order.NhdsSet Mathlib.AlgebraicTopology.TopologicalSimplex Mathlib.RingTheory.Valuation.RamificationGroup Mathlib.Topology.ContinuousFunction.Ordered Mathlib.Tactic.ComputeDegree Mathlib.Probability.Distributions.Uniform Mathlib.SetTheory.Surreal.Dyadic Mathlib.Geometry.Euclidean.Sphere.SecondInter Mathlib.Geometry.Euclidean.Basic Mathlib.Algebra.Lie.Matrix Mathlib.MeasureTheory.Covering.DensityTheorem Mathlib.Algebra.MvPolynomial.Supported Mathlib.MeasureTheory.Integral.LebesgueNormedSpace Mathlib.Probability.ProbabilityMassFunction.Binomial Mathlib.RingTheory.MvPolynomial.Tower Mathlib.Geometry.RingedSpace.Basic Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.Data.Matrix.Rank Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas Mathlib.NumberTheory.Liouville.Measure Mathlib.Combinatorics.SimpleGraph.Girth Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.GroupTheory.Torsion Mathlib.Topology.Algebra.InfiniteSum.Ring Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.Data.Finsupp.Multiset Mathlib.Topology.ContinuousFunction.Weierstrass Mathlib.LinearAlgebra.QuadraticForm.Complex Mathlib.Topology.MetricSpace.Algebra Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.Topology.Order.LeftRightLim Mathlib.Geometry.Manifold.VectorBundle.Hom Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Analysis.InnerProductSpace.Orthogonal Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Data.Fintype.Units Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology Mathlib.Geometry.Euclidean.MongePoint Mathlib.Analysis.Convex.Between Mathlib.GroupTheory.FixedPointFree Mathlib.LinearAlgebra.AffineSpace.Independent Mathlib.Analysis.LocallyConvex.Polar Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional Mathlib.MeasureTheory.Group.Pointwise Mathlib.Algebra.AlgebraicCard Mathlib.Analysis.Calculus.ContDiff.Bounds Mathlib.Topology.Compactness.PseudometrizableLindelof Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.Analysis.Normed.Group.HomCompletion Mathlib.Data.Complex.BigOperators Mathlib.NumberTheory.Ostrowski Mathlib.Data.Real.Irrational Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic Mathlib.Data.Num.Prime Mathlib.CategoryTheory.Galois.Basic Mathlib.Topology.Category.CompHaus.Limits Mathlib.Topology.Algebra.Module.LocallyConvex Mathlib.CategoryTheory.Idempotents.SimplicialObject Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.Algebra.Polynomial.Induction Mathlib.LinearAlgebra.Contraction Mathlib.MeasureTheory.Measure.Doubling Mathlib.SetTheory.Cardinal.Continuum Mathlib.Algebra.Algebra.Spectrum Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.Topology.Order.MonotoneConvergence Mathlib.Analysis.MeanInequalities Mathlib.Data.Nat.Multiplicity Mathlib.LinearAlgebra.Matrix.BilinearForm Mathlib.FieldTheory.PrimitiveElement Mathlib.Data.Rat.Star Mathlib.Algebra.Star.CHSH Mathlib.Probability.Distributions.Poisson Mathlib.RingTheory.Binomial Mathlib.Geometry.Euclidean.Sphere.Basic Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.Data.Real.Archimedean Mathlib.RingTheory.RingHom.Integral Mathlib.RingTheory.Polynomial.Chebyshev Mathlib.Data.Nat.Factorial.BigOperators Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.Analysis.Normed.Ring.SeminormFromBounded Mathlib.Geometry.Manifold.ConformalGroupoid Mathlib.RingTheory.Smooth.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Even Mathlib.Algebra.Polynomial.Laurent Mathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.LinearAlgebra.Multilinear.FiniteDimensional Mathlib.Condensed.TopCatAdjunction Mathlib.Algebra.Module.Submodule.Localization Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.Data.Matroid.Closure Mathlib.Topology.Algebra.MvPolynomial Mathlib.Algebra.Homology.HomotopyCategory.Shift Mathlib.Algebra.Polynomial.Module.Basic Mathlib.Analysis.Normed.MulAction Mathlib.Algebra.Module.Zlattice.Basic Mathlib.Analysis.InnerProductSpace.Projection Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.Analysis.NormedSpace.MStructure Mathlib.Computability.TMComputable Mathlib.Algebra.Lie.Semisimple.Defs Mathlib.Analysis.BoxIntegral.Partition.Tagged Mathlib.Algebra.Polynomial.Degree.CardPowDegree Mathlib.Data.ZMod.Basic Mathlib.LinearAlgebra.Matrix.AbsoluteValue Mathlib.LinearAlgebra.Eigenspace.Triangularizable Mathlib.NumberTheory.LegendreSymbol.ZModChar Mathlib.RingTheory.MvPowerSeries.Inverse Mathlib.Topology.Algebra.UniformConvergence Mathlib.RingTheory.MvPolynomial.Symmetric Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike Mathlib.RingTheory.SurjectiveOnStalks Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Analysis.Convex.Independent Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal Mathlib.RingTheory.ChainOfDivisors Mathlib.Analysis.Calculus.Deriv.Prod Mathlib.Analysis.Convex.Strong Mathlib.Analysis.Calculus.ContDiff.Basic Mathlib.Data.Matrix.ColumnRowPartitioned Mathlib.LinearAlgebra.Projectivization.Independence Mathlib.Analysis.Complex.Asymptotics Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Probability.ConditionalProbability Mathlib.Algebra.Category.ModuleCat.Colimits Mathlib.Order.Filter.ENNReal Mathlib.Analysis.Normed.Field.UnitBall Mathlib.Analysis.Calculus.Deriv.Mul Mathlib.Tactic.NormNum.NatSqrt Mathlib.Analysis.Calculus.Conformal.NormedSpace Mathlib.LinearAlgebra.InvariantBasisNumber Mathlib.Analysis.Normed.Group.Completion Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Algebra.Category.BialgebraCat.Basic Mathlib.Algebra.Polynomial.Derivative Mathlib.Topology.Algebra.Field Mathlib.Data.Complex.FiniteDimensional Mathlib.Topology.ContinuousFunction.Units Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse Mathlib.Topology.Algebra.UniformRing Mathlib.RingTheory.OrzechProperty Mathlib.Topology.MetricSpace.Pseudo.Lemmas Mathlib.Analysis.BoxIntegral.Basic Mathlib.SetTheory.Game.State Mathlib.GroupTheory.Perm.Cycle.Concrete Mathlib.RingTheory.Polynomial.Basic Mathlib.MeasureTheory.Measure.AddContent Mathlib.Analysis.Quaternion Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass Mathlib.Analysis.SpecialFunctions.Bernstein Mathlib.Algebra.Lie.Abelian Mathlib.LinearAlgebra.SesquilinearForm Mathlib.Data.Nat.Choose.Factorization Mathlib.Data.Matrix.Kronecker Mathlib.AlgebraicGeometry.FunctionField Mathlib.RingTheory.DedekindDomain.Different Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.RingTheory.HopfAlgebra Mathlib.Data.Nat.Choose.Sum Mathlib.Topology.EMetricSpace.Basic Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology Mathlib.LinearAlgebra.TensorProduct.Submodule Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.Algebra.Algebra.Subalgebra.Basic Mathlib.RingTheory.LocalRing.ResidueField.Defs Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Analysis.Normed.Group.Bounded Mathlib.Data.ZMod.Parity Mathlib.Analysis.Normed.Algebra.Exponential Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.MeasureTheory.Integral.RieszMarkovKakutani Mathlib.GroupTheory.Commensurable Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex Mathlib.Analysis.BoxIntegral.Integrability Mathlib.Algebra.Star.RingQuot Mathlib.Data.Matroid.Constructions Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.RingTheory.Discriminant Mathlib.Data.Int.Star Mathlib.Analysis.Calculus.FDeriv.RestrictScalars Mathlib.NumberTheory.SumTwoSquares Mathlib.GroupTheory.Complement Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Analysis.SpecialFunctions.Exponential Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup Mathlib.Algebra.Homology.Refinements Mathlib.Algebra.DirectLimit Mathlib.MeasureTheory.Measure.VectorMeasure Mathlib.RingTheory.ReesAlgebra Mathlib.Analysis.Analytic.Meromorphic Mathlib.RingTheory.IsTensorProduct Mathlib.Algebra.Module.PID Mathlib.Algebra.MvPolynomial.Comap Mathlib.Topology.Algebra.Algebra.Rat Mathlib.RingTheory.Ideal.AssociatedPrime Mathlib.Analysis.Convex.KreinMilman Mathlib.RingTheory.Polynomial.GaussLemma Mathlib.LinearAlgebra.CliffordAlgebra.Inversion Mathlib.Topology.Covering Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.RingTheory.Polynomial.Wronskian Mathlib.Algebra.Category.AlgebraCat.Symmetric Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.Analysis.NormedSpace.Extr Mathlib.NumberTheory.ClassNumber.Finite Mathlib.FieldTheory.Finiteness Mathlib.Topology.MetricSpace.GromovHausdorff Mathlib.Topology.UnitInterval Mathlib.Combinatorics.Schnirelmann Mathlib.Topology.UrysohnsLemma Mathlib.Topology.Category.CompactlyGenerated Mathlib.NumberTheory.Harmonic.Int Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.Algebra.Pointwise.Stabilizer Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries Mathlib.Analysis.Calculus.IteratedDeriv.Defs Mathlib.RingTheory.WittVector.StructurePolynomial Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.MeasureTheory.Constructions.BorelSpace.Complex Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic Mathlib.NumberTheory.MaricaSchoenheim Mathlib.Analysis.Complex.Tietze Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving Mathlib.Topology.Homotopy.HomotopyGroup Mathlib.Data.Real.StarOrdered Mathlib.Analysis.Normed.Order.Basic Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.Algebra.CharP.ExpChar Mathlib.Topology.Metrizable.Basic Mathlib.MeasureTheory.Function.L1Space Mathlib.Analysis.NormedSpace.HahnBanach.Extension Mathlib.MeasureTheory.Measure.Count Mathlib.Analysis.Calculus.Deriv.Shift Mathlib.Probability.Kernel.Disintegration.Basic Mathlib.LinearAlgebra.FreeAlgebra Mathlib.Analysis.Complex.RemovableSingularity Mathlib.RingTheory.Nilpotent.Basic Mathlib.RingTheory.DedekindDomain.Basic Mathlib.LinearAlgebra.Matrix.Charpoly.Univ Mathlib.RingTheory.JacobsonIdeal Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting Mathlib.Topology.Algebra.UniformFilterBasis Mathlib.Analysis.Convex.Normed Mathlib.Topology.Algebra.Nonarchimedean.Bases Mathlib.Probability.Kernel.Basic Mathlib.GroupTheory.Index Mathlib.MeasureTheory.Measure.Tilted Mathlib.Analysis.Calculus.Deriv.Inverse Mathlib.Analysis.Complex.Liouville Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.GroupTheory.Perm.Finite Mathlib.Topology.Algebra.UniformGroup Mathlib.Topology.FiberBundle.Trivialization Mathlib.MeasureTheory.Group.AEStabilizer Mathlib.Data.Nat.Digits Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber Mathlib.Data.Finset.Pointwise.Card Mathlib.GroupTheory.SpecificGroups.Quaternion Mathlib.Topology.Algebra.OpenSubgroup Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.Topology.Algebra.Module.StrongTopology Mathlib.MeasureTheory.Constructions.Prod.Basic Mathlib.Analysis.Convex.EGauge Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.LinearAlgebra.Ray Mathlib.CategoryTheory.Localization.Triangulated Mathlib.Analysis.Normed.Group.Int Mathlib.Analysis.Convex.Mul Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.Topology.Algebra.Module.LinearPMap Mathlib.Topology.MetricSpace.ThickenedIndicator Mathlib.CategoryTheory.Galois.Prorepresentability Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.Topology.Algebra.Group.Compact Mathlib.CategoryTheory.Triangulated.Opposite Mathlib.Topology.Algebra.Polynomial Mathlib.Algebra.Homology.ComplexShapeSigns Mathlib.Analysis.Convex.Segment Mathlib.Data.ZMod.Units Mathlib.Tactic.Qify Mathlib.Analysis.Calculus.Darboux Mathlib.Probability.ProbabilityMassFunction.Basic Mathlib.MeasureTheory.Function.Jacobian Mathlib.FieldTheory.Perfect Mathlib.AlgebraicTopology.DoldKan.Faces Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.Algebra.Module.Injective Mathlib.Topology.FiberBundle.Basic Mathlib.LinearAlgebra.TensorProduct.Graded.External Mathlib.Topology.MetricSpace.Contracting Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.FieldTheory.IsAlgClosed.Basic Mathlib.ModelTheory.Skolem Mathlib.Algebra.Category.FGModuleCat.Basic Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.Data.Complex.Cardinality Mathlib.Algebra.Homology.Localization Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.MeasureTheory.Function.LpOrder Mathlib.RingTheory.UniqueFactorizationDomain Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.Analysis.Convex.Measure Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.Probability.Moments Mathlib.Topology.Algebra.Nonarchimedean.Basic Mathlib.Algebra.Homology.BifunctorHomotopy Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Analysis.Analytic.Linear Mathlib.Analysis.SpecialFunctions.Log.Deriv Mathlib.LinearAlgebra.Eigenspace.Basic Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.FieldTheory.Cardinality Mathlib.Algebra.Lie.EngelSubalgebra Mathlib.NumberTheory.Cyclotomic.PID Mathlib.Analysis.NormedSpace.Int Mathlib.Algebra.Algebra.Subalgebra.MulOpposite Mathlib.Analysis.Normed.Lp.LpEquiv Mathlib.Topology.Algebra.Group.TopologicalAbelianization Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.RCLike.Basic Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.Analysis.Normed.Operator.Banach Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Algebra.Module.CharacterModule Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs Mathlib.AlgebraicGeometry.EllipticCurve.Projective Mathlib.Analysis.Calculus.LineDeriv.Basic Mathlib.Topology.Algebra.Algebra Mathlib.NumberTheory.Dioph Mathlib.MeasureTheory.Group.FundamentalDomain Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane Mathlib.Algebra.Module.Torsion Mathlib.AlgebraicTopology.DoldKan.Equivalence Mathlib.Analysis.Complex.Conformal Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.Analysis.Normed.Group.AddCircle Mathlib.Topology.Instances.Matrix Mathlib.Topology.Instances.Complex Mathlib.MeasureTheory.MeasurableSpace.Basic Mathlib.Algebra.Jordan.Basic Mathlib.Algebra.Polynomial.GroupRingAction Mathlib.SetTheory.Cardinal.Subfield Mathlib.RingTheory.HahnSeries.Valuation Mathlib.Analysis.Convex.Contractible Mathlib.Data.Finsupp.WellFounded Mathlib.RingTheory.EuclideanDomain Mathlib.AlgebraicGeometry.AffineScheme Mathlib.SetTheory.Game.Domineering Mathlib.MeasureTheory.Group.Convolution Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.RingTheory.RootsOfUnity.Complex Mathlib.MeasureTheory.MeasurableSpace.Card Mathlib.Analysis.Normed.Ring.Units Mathlib.NumberTheory.Liouville.Basic Mathlib.NumberTheory.Padics.RingHoms Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics Mathlib.RingTheory.LocalRing.ResidueField.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Grading Mathlib.Data.Real.Pi.Bounds Mathlib.Data.Nat.Factorization.Root Mathlib.MeasureTheory.Decomposition.Lebesgue Mathlib.Data.ZMod.Factorial Mathlib.Analysis.BoxIntegral.Partition.Filter Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic Mathlib.RingTheory.Valuation.Integers Mathlib.RingTheory.Polynomial.SeparableDegree Mathlib.Topology.MetricSpace.Perfect Mathlib.Computability.DFA Mathlib.Topology.MetricSpace.CauSeqFilter Mathlib.Algebra.Category.Grp.Images Mathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.FieldTheory.Separable Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.LinearAlgebra.TensorProduct.Opposite Mathlib.Algebra.Homology.SingleHomology Mathlib.AlgebraicTopology.SimplexCategory Mathlib.Topology.EMetricSpace.Diam Mathlib.Topology.Connected.PathConnected Mathlib.Analysis.Normed.Operator.WeakOperatorTopology Mathlib.Topology.Order.DenselyOrdered Mathlib.RingTheory.HahnSeries.Summable Mathlib.Dynamics.Ergodic.Ergodic Mathlib.Data.Finite.Card Mathlib.Algebra.Algebra.Quasispectrum Mathlib.Algebra.Module.FinitePresentation Mathlib.NumberTheory.KummerDedekind Mathlib.AlgebraicGeometry.Limits Mathlib.RingTheory.EisensteinCriterion Mathlib.Algebra.Star.Free Mathlib.RingTheory.Int.Basic Mathlib.Geometry.Manifold.MFDeriv.Defs Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.Analysis.NormedSpace.ENorm Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional Mathlib.Algebra.Polynomial.BigOperators Mathlib.Topology.Algebra.Affine Mathlib.Analysis.CStarAlgebra.Basic Mathlib.MeasureTheory.Measure.OpenPos Mathlib.Topology.Algebra.PontryaginDual Mathlib.MeasureTheory.Function.LocallyIntegrable Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence Mathlib.Analysis.Analytic.Constructions Mathlib.RingTheory.Localization.Basic Mathlib.Topology.MetricSpace.Holder Mathlib.Algebra.MvPolynomial.Monad Mathlib.Combinatorics.Colex Mathlib.MeasureTheory.Measure.Dirac Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization Mathlib.RingTheory.Ideal.Operations Mathlib.RingTheory.Smooth.StandardSmooth Mathlib.LinearAlgebra.CliffordAlgebra.Basic Mathlib.FieldTheory.IsAlgClosed.Spectrum Mathlib.Topology.Algebra.Valued.ValuationTopology Mathlib.Analysis.SpecificLimits.Normed Mathlib.NumberTheory.ModularForms.Basic Mathlib.Analysis.Calculus.FDeriv.Prod Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra Mathlib.Topology.Algebra.Order.UpperLower Mathlib.SetTheory.Cardinal.CountableCover Mathlib.Algebra.Order.Hom.Basic Mathlib.Analysis.NormedSpace.HahnBanach.Separation Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits Mathlib.Topology.Algebra.FilterBasis Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.LinearAlgebra.Alternating.Basic Mathlib.RingTheory.WittVector.Frobenius Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.MeasureTheory.Decomposition.SignedHahn Mathlib.Topology.ContinuousFunction.LocallyConstant Mathlib.RingTheory.AlgebraicIndependent Mathlib.LinearAlgebra.Vandermonde Mathlib.LinearAlgebra.Matrix.SesquilinearForm Mathlib.RingTheory.Localization.NumDen Mathlib.Topology.Category.Compactum Mathlib.Analysis.Normed.Group.InfiniteSum Mathlib.Analysis.NormedSpace.DualNumber Mathlib.Data.Rat.Cast.Lemmas Mathlib.NumberTheory.Pell Mathlib.Analysis.Calculus.Deriv.Comp Mathlib.Probability.Process.Stopping Mathlib.Algebra.Category.AlgebraCat.Monoidal Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous Mathlib.RingTheory.IntegralClosure.IntegrallyClosed Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.CategoryTheory.Triangulated.TriangleShift Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.NumberTheory.NumberField.Basic Mathlib.Topology.Algebra.Ring.Ideal Mathlib.Analysis.Normed.Affine.AddTorsor Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.MeasureTheory.Function.SpecialFunctions.Inner Mathlib.Geometry.RingedSpace.Stalks Mathlib.Topology.Order.LeftRightNhds Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps Mathlib.Analysis.Normed.Affine.AddTorsorBases Mathlib.NumberTheory.Modular Mathlib.RingTheory.WittVector.Basic Mathlib.Algebra.Homology.TotalComplex Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.Topology.UniformSpace.AbsoluteValue Mathlib.Tactic.ReduceModChar Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.MeasureTheory.Integral.MeanInequalities Mathlib.Algebra.Polynomial.Eval Mathlib.Topology.VectorBundle.Constructions Mathlib.GroupTheory.Transfer Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.Topology.MetricSpace.PiNat Mathlib.RingTheory.HahnSeries.PowerSeries Mathlib.Analysis.NormedSpace.HomeomorphBall Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty Mathlib.ModelTheory.ElementarySubstructures Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.Algebra.Homology.HomologySequenceLemmas Mathlib.Algebra.Polynomial.Reverse Mathlib.RingTheory.Smooth.Kaehler Mathlib.Geometry.Manifold.ContMDiff.Defs Mathlib.LinearAlgebra.TensorProduct.DirectLimit Mathlib.Analysis.Normed.Algebra.Basic Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.RepresentationTheory.FDRep Mathlib.Algebra.Order.Antidiag.Finsupp Mathlib.Analysis.Normed.Group.Lemmas Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal Mathlib.Algebra.MvPolynomial.Equiv Mathlib.AlgebraicTopology.SimplicialObject Mathlib.GroupTheory.Coxeter.Inversion Mathlib.RingTheory.WittVector.Isocrystal Mathlib.Analysis.SpecialFunctions.Log.Basic Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.MeasureTheory.Measure.Stieltjes Mathlib.Analysis.Calculus.ContDiff.RCLike Mathlib.RingTheory.Ideal.IsPrimary Mathlib.Analysis.Convex.Function Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.ODE.Gronwall Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed Mathlib.Topology.ContinuousFunction.Compact Mathlib.GroupTheory.Finiteness Mathlib.Analysis.Analytic.Composition Mathlib.FieldTheory.RatFunc.Defs Mathlib.Topology.VectorBundle.Basic Mathlib.Topology.MetricSpace.Basic Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn Mathlib.CategoryTheory.Preadditive.ProjectiveResolution Mathlib.Topology.Sheaves.PresheafOfFunctions Mathlib.Dynamics.Ergodic.Action.Regular Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic Mathlib.Analysis.Calculus.FDeriv.Mul Mathlib.Topology.Compactness.CompactlyGeneratedSpace Mathlib.RingTheory.Bezout Mathlib.Analysis.ConstantSpeed Mathlib.Topology.Category.Stonean.Basic Mathlib.Analysis.Normed.Operator.LinearIsometry Mathlib.SetTheory.Surreal.Multiplication Mathlib.AlgebraicTopology.Nerve Mathlib.RingTheory.Polynomial.Nilpotent Mathlib.Tactic.NormNum.OfScientific Mathlib.LinearAlgebra.Matrix.Hermitian Mathlib.CategoryTheory.Monoidal.Internal.Module Mathlib.Analysis.Calculus.Monotone Mathlib.RingTheory.Polynomial.Selmer Mathlib.Analysis.Calculus.Implicit Mathlib.RingTheory.Unramified.Basic Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv Mathlib.FieldTheory.NormalClosure Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm Mathlib.Algebra.QuadraticDiscriminant Mathlib.Geometry.Manifold.IntegralCurve Mathlib.Analysis.SumIntegralComparisons Mathlib.Data.Nat.Factorization.Basic Mathlib.GroupTheory.PresentedGroup Mathlib.Topology.Instances.EReal Mathlib.Topology.Algebra.Module.Multilinear.Bounded Mathlib.Topology.MetricSpace.HausdorffDistance Mathlib.LinearAlgebra.Reflection Mathlib.LinearAlgebra.AnnihilatingPolynomial Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.Tactic.NormNum.DivMod Mathlib.Computability.NFA Mathlib.Data.Complex.Order Mathlib.Analysis.Calculus.Deriv.AffineMap Mathlib.Topology.MetricSpace.Defs Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.Topology.EMetricSpace.Lipschitz Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.Data.ENNReal.Real Mathlib.NumberTheory.FermatPsp Mathlib.Combinatorics.SetFamily.CauchyDavenport Mathlib.RingTheory.Kaehler.Basic Mathlib.SetTheory.Cardinal.PartENat Mathlib.GroupTheory.Sylow Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.Probability.Kernel.MeasureCompProd Mathlib.Order.Filter.Archimedean Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField Mathlib.Analysis.NormedSpace.Extend Mathlib.AlgebraicTopology.SplitSimplicialObject Mathlib.NumberTheory.VonMangoldt Mathlib.NumberTheory.ZetaValues Mathlib.Topology.Algebra.Order.LiminfLimsup Mathlib.Analysis.Asymptotics.Theta Mathlib.Combinatorics.SimpleGraph.DegreeSum Mathlib.Analysis.Convex.Deriv Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.RingTheory.LocalProperties Mathlib.Topology.MetricSpace.Gluing Mathlib.MeasureTheory.Function.Egorov Mathlib.Probability.Independence.Basic Mathlib.Topology.Category.LightProfinite.Basic Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction Mathlib.Analysis.CStarAlgebra.Exponential Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine Mathlib.Analysis.SpecialFunctions.Arsinh Mathlib.Algebra.Order.CauSeq.BigOperators Mathlib.Analysis.Calculus.ContDiff.FiniteDimension Mathlib.Algebra.Lie.Semisimple.Basic Mathlib.MeasureTheory.Constructions.Cylinders Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.Analysis.BoxIntegral.Partition.Basic Mathlib.Analysis.Normed.Operator.BoundedLinearMaps Mathlib.Analysis.Fourier.FourierTransform Mathlib.RingTheory.MatrixAlgebra Mathlib.LinearAlgebra.Dimension.LinearMap Mathlib.Topology.MetricSpace.CantorScheme Mathlib.Algebra.Lie.Derivation.Basic Mathlib.Analysis.Convex.Cone.Basic Mathlib.LinearAlgebra.Matrix.LDL Mathlib.Algebra.Category.AlgebraCat.Basic Mathlib.Tactic.FunProp.Differentiable Mathlib.Algebra.Group.Subgroup.Finite Mathlib.RingTheory.AdjoinRoot Mathlib.Topology.ContinuousFunction.ZeroAtInfty Mathlib.RingTheory.Adjoin.Basic Mathlib.RingTheory.GradedAlgebra.Radical Mathlib.LinearAlgebra.Multilinear.TensorProduct Mathlib.RingTheory.Coalgebra.Equiv Mathlib.Algebra.Lie.Weights.Killing Mathlib.Combinatorics.Enumerative.Catalan Mathlib.Algebra.Homology.LocalCohomology Mathlib.Analysis.Matrix Mathlib.Analysis.Convex.Uniform Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup Mathlib.RingTheory.GradedAlgebra.Basic Mathlib.RingTheory.Idempotents Mathlib.Analysis.SpecialFunctions.Pow.Real Mathlib.Dynamics.Flow Mathlib.RingTheory.Valuation.ValuationSubring Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion Mathlib.Tactic.Rify Mathlib.Algebra.CharP.Quotient Mathlib.Algebra.MvPolynomial.Cardinal Mathlib.Algebra.MvPolynomial.Division Mathlib.Probability.IdentDistrib Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.RingTheory.Complex Mathlib.Analysis.Convolution Mathlib.AlgebraicGeometry.Scheme Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm Mathlib.MeasureTheory.Covering.Vitali Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle Mathlib.Topology.EMetricSpace.Paracompact Mathlib.LinearAlgebra.Matrix.Adjugate Mathlib.Data.Complex.Module Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.LinearAlgebra.Eigenspace.Semisimple Mathlib.Analysis.Convex.Gauge Mathlib.Data.ENNReal.Operations Mathlib.Analysis.Calculus.Conformal.InnerProduct Mathlib.FieldTheory.KummerExtension Mathlib.Analysis.CStarAlgebra.Module.Synonym Mathlib.NumberTheory.LucasPrimality Mathlib.Topology.Category.LightProfinite.Sequence Mathlib.Algebra.Homology.QuasiIso Mathlib.Analysis.Analytic.Basic Mathlib.ModelTheory.Bundled Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.Analysis.Analytic.Uniqueness Mathlib.Condensed.Light.Basic Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.AlgebraicGeometry.Gluing Mathlib.LinearAlgebra.AffineSpace.Combination Mathlib.GroupTheory.GroupAction.Quotient Mathlib.LinearAlgebra.QuadraticForm.Isometry Mathlib.Combinatorics.SetFamily.LYM Mathlib.Analysis.Convex.Jensen Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence Mathlib.Topology.Instances.Irrational Mathlib.Topology.Algebra.Module.Basic Mathlib.Order.RelSeries Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.ModelTheory.Algebra.Ring.FreeCommRing Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition Mathlib.Analysis.Complex.Arg Mathlib.Analysis.Calculus.Deriv.Support Mathlib.Geometry.Manifold.Algebra.Monoid Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv Mathlib.FieldTheory.Minpoly.Field Mathlib.LinearAlgebra.UnitaryGroup Mathlib.Algebra.AddConstMap.Basic Mathlib.Computability.EpsilonNFA Mathlib.Topology.Algebra.Module.Determinant Mathlib.MeasureTheory.Constructions.Polish.Basic Mathlib.Topology.Algebra.GroupCompletion Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber Mathlib.Order.Interval.Finset.Box Mathlib.Topology.MetricSpace.Kuratowski Mathlib.Algebra.Module.LinearMap.Polynomial Mathlib.Data.Matroid.IndepAxioms Mathlib.Analysis.MellinInversion Mathlib.NumberTheory.BernoulliPolynomials Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.NumberTheory.LucasLehmer Mathlib.Algebra.MonoidAlgebra.Grading Mathlib.RingTheory.RingHomProperties Mathlib.LinearAlgebra.BilinearForm.TensorProduct Mathlib.AlgebraicGeometry.Cover.Open Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Geometry.Manifold.Algebra.Structures Mathlib.Topology.Sheaves.Operations Mathlib.Data.Real.EReal Mathlib.AlgebraicGeometry.Stalk Mathlib.Condensed.Light.Module Mathlib.Data.Real.Cardinality Mathlib.RingTheory.AdicCompletion.Algebra Mathlib.Topology.Category.Sequential Mathlib.GroupTheory.PushoutI Mathlib.ModelTheory.Types Mathlib.Analysis.Convex.Strict Mathlib.RingTheory.Valuation.Quotient Mathlib.Algebra.Category.Ring.Constructions Mathlib.RingTheory.Polynomial.Eisenstein.Basic Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.LinearAlgebra.Dimension.Free Mathlib.Order.Filter.Cocardinal Mathlib.Dynamics.Ergodic.Function Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian Mathlib.Algebra.CharP.Reduced Mathlib.Algebra.Lie.BaseChange Mathlib.Data.Nat.PartENat Mathlib.Algebra.CharZero.Quotient Mathlib.Analysis.Normed.Module.Basic Mathlib.Algebra.Algebra.Subalgebra.Unitization Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating Mathlib.LinearAlgebra.Isomorphisms Mathlib.Analysis.Complex.Convex Mathlib.Topology.Separation.NotNormal Mathlib.Topology.Category.Locale Mathlib.NumberTheory.PrimeCounting Mathlib.LinearAlgebra.Dual Mathlib.LinearAlgebra.TensorProduct.RightExactness Mathlib.Topology.MetricSpace.ProperSpace.Lemmas Mathlib.Analysis.Complex.UpperHalfPlane.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv Mathlib.Algebra.Lie.CartanMatrix Mathlib.Geometry.Manifold.MFDeriv.Atlas Mathlib.Combinatorics.SimpleGraph.Acyclic Mathlib.Analysis.Convex.Combination Mathlib.Analysis.Normed.Group.Pointwise Mathlib.MeasureTheory.OuterMeasure.Defs Mathlib.ModelTheory.Fraisse Mathlib.LinearAlgebra.Matrix.Basis Mathlib.RingTheory.Bialgebra.Equiv Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.Algebra.Polynomial.Lifts Mathlib.RingTheory.Finiteness Mathlib.NumberTheory.Padics.Hensel Mathlib.MeasureTheory.Covering.Differentiation Mathlib.Data.Nat.Choose.Multinomial Mathlib.GroupTheory.HNNExtension Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.CategoryTheory.Galois.Examples Mathlib.RingTheory.Polynomial.ScaleRoots Mathlib.GroupTheory.SpecificGroups.Alternating Mathlib.RingTheory.FractionalIdeal.Operations Mathlib.Analysis.Calculus.FDeriv.Comp Mathlib.Topology.Instances.RealVectorSpace Mathlib.Analysis.LocallyConvex.ContinuousOfBounded Mathlib.LinearAlgebra.QuadraticForm.TensorProduct Mathlib.Analysis.Convex.Hull Mathlib.RingTheory.Fintype Mathlib.Analysis.Complex.Hadamard Mathlib.RingTheory.Etale.Basic Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.Convex.Star Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm Mathlib.Geometry.Manifold.Algebra.LieGroup Mathlib.Tactic.Positivity.Basic Mathlib.Algebra.Lie.UniversalEnveloping Mathlib.Topology.Algebra.Order.Group Mathlib.Topology.Algebra.InfiniteSum.Order Mathlib.NumberTheory.PrimesCongruentOne Mathlib.Data.ZMod.Algebra Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.ModelTheory.Algebra.Field.CharP Mathlib.Algebra.Order.CompleteField Mathlib.RingTheory.Ideal.Norm Mathlib.Analysis.Analytic.CPolynomial Mathlib.Analysis.BoundedVariation Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Combinatorics.SimpleGraph.Regularity.Bound Mathlib.Algebra.Homology.HomotopyCategory.ShortExact Mathlib.CategoryTheory.Triangulated.Subcategory Mathlib.RingTheory.Ideal.Pointwise Mathlib.RingTheory.Ideal.Colon Mathlib.LinearAlgebra.Basis.Basic Mathlib.MeasureTheory.Measure.Restrict Mathlib.CategoryTheory.Triangulated.Functor Mathlib.Data.Finsupp.Lex Mathlib.RingTheory.WittVector.Teichmuller Mathlib.Algebra.Polynomial.Degree.Lemmas Mathlib.NumberTheory.WellApproximable Mathlib.Analysis.LocallyConvex.WithSeminorms Mathlib.RingTheory.LocalRing.Module Mathlib.MeasureTheory.Measure.Lebesgue.Basic Mathlib.Analysis.Asymptotics.SuperpolynomialDecay Mathlib.Analysis.Convex.Basic Mathlib.NumberTheory.LSeries.Convergence Mathlib.LinearAlgebra.CliffordAlgebra.Contraction Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.MetricSpace.Bilipschitz Mathlib.CategoryTheory.Abelian.InjectiveResolution Mathlib.InformationTheory.Hamming Mathlib.Analysis.Calculus.LocalExtr.Basic Mathlib.Algebra.CharP.Algebra Mathlib.CategoryTheory.Triangulated.TStructure.Basic Mathlib.RingTheory.Localization.Module Mathlib.Analysis.Convex.Cone.Proper Mathlib.Algebra.Lie.Subalgebra Mathlib.Probability.Process.Adapted Mathlib.RingTheory.MvPolynomial.Basic Mathlib.Analysis.Normed.Order.Lattice Mathlib.Algebra.MvPolynomial.PDeriv Mathlib.Topology.ContinuousFunction.Bounded Mathlib.Data.Finsupp.Interval Mathlib.NumberTheory.DirichletCharacter.Bounds Mathlib.Algebra.Lie.Sl2 Mathlib.Topology.Algebra.Module.WeakDual Mathlib.Analysis.Convex.Cone.Closure Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.Data.Nat.Factorial.Cast Mathlib.Analysis.Convex.Complex Mathlib.Data.Rat.Sqrt Mathlib.Logic.Equiv.Fintype Mathlib.RingTheory.FreeCommRing Mathlib.Tactic.NormNum.IsCoprime Mathlib.RingTheory.PowerSeries.Order Mathlib.FieldTheory.PurelyInseparable Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv Mathlib.Analysis.Normed.Module.Ray Mathlib.Algebra.Group.UniqueProds Mathlib.RingTheory.Valuation.PrimeMultiplicity Mathlib.CategoryTheory.Preadditive.InjectiveResolution Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.Algebra.MvPolynomial.CommRing Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.MeasureTheory.Measure.MutuallySingular Mathlib.Algebra.Polynomial.Module.FiniteDimensional Mathlib.Analysis.Analytic.Within Mathlib.CategoryTheory.Preadditive.HomOrthogonal Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Convex.Extrema Mathlib.Analysis.Convex.Extreme Mathlib.Data.Finset.Density Mathlib.Probability.Independence.Kernel Mathlib.Analysis.Calculus.FDeriv.Equiv Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.RingTheory.WittVector.IsPoly Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.MeasureTheory.Group.Prod Mathlib.LinearAlgebra.Dimension.Constructions Mathlib.Order.Category.Frm Mathlib.Topology.Algebra.Localization Mathlib.MeasureTheory.Integral.Pi Mathlib.Data.Real.Basic Mathlib.NumberTheory.NumberField.House Mathlib.Algebra.Category.Grp.Colimits Mathlib.Analysis.Normed.Module.Complemented Mathlib.Analysis.NormedSpace.OperatorNorm.Prod Mathlib.Data.Matroid.Restrict Mathlib.Data.Real.Star Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap Mathlib.Algebra.Lie.Solvable Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.GroupTheory.SpecificGroups.Cyclic Mathlib.Analysis.Complex.UpperHalfPlane.Exp Mathlib.NumberTheory.NumberField.Embeddings Mathlib.MeasureTheory.Function.Intersectivity Mathlib.Topology.Order.T5 Mathlib.Topology.KrullDimension Mathlib.CategoryTheory.Abelian.LeftDerived Mathlib.Condensed.Epi Mathlib.GroupTheory.Coxeter.Length Mathlib.Algebra.Lie.Weights.Cartan Mathlib.MeasureTheory.Measure.Typeclasses Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.Probability.Process.Filtration Mathlib.MeasureTheory.Integral.Periodic Mathlib.Algebra.Homology.Homotopy Mathlib.LinearAlgebra.TensorPower Mathlib.RingTheory.MvPolynomial.NewtonIdentities Mathlib.Algebra.QuaternionBasis Mathlib.NumberTheory.Harmonic.Bounds Mathlib.NumberTheory.Basic Mathlib.NumberTheory.Bernoulli Mathlib.Algebra.Polynomial.UnitTrinomial Mathlib.LinearAlgebra.SymplecticGroup Mathlib.Geometry.Manifold.AnalyticManifold Mathlib.Analysis.MellinTransform Mathlib.LinearAlgebra.Determinant Mathlib.LinearAlgebra.Matrix.Transvection Mathlib.RingTheory.LocalRing.RingHom.Basic Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating Mathlib.Analysis.Convex.StrictConvexBetween Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.NumberTheory.LSeries.Linearity Mathlib.Analysis.NormedSpace.Real Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card Mathlib.Analysis.Analytic.IsolatedZeros Mathlib.MeasureTheory.Integral.Gamma Mathlib.Geometry.Manifold.ContMDiff.NormedSpace Mathlib.MeasureTheory.OuterMeasure.Operations Mathlib.Algebra.Order.CauSeq.Basic Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Integral.IntegrableOn Mathlib.Topology.Algebra.Valued.ValuedField Mathlib.LinearAlgebra.Dimension.StrongRankCondition Mathlib.Analysis.Convex.SpecificFunctions.Deriv Mathlib.Analysis.Normed.Group.Submodule Mathlib.Analysis.Normed.Module.WeakDual Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.ModelTheory.DirectLimit Mathlib.Algebra.Lie.Engel Mathlib.Analysis.Calculus.FDeriv.Symmetric Mathlib.RingTheory.WittVector.Defs Mathlib.Algebra.Category.ModuleCat.Free Mathlib.Analysis.Normed.Field.InfiniteSum Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear Mathlib.Algebra.Algebra.Subalgebra.Directed Mathlib.Geometry.Euclidean.Inversion.Basic Mathlib.Algebra.MvPolynomial.Polynomial Mathlib.Topology.Algebra.Module.Multilinear.Topology Mathlib.Analysis.Normed.Group.ControlledClosure Mathlib.Algebra.Lie.Rank Mathlib.AlgebraicTopology.MooreComplex Mathlib.Probability.Kernel.Condexp Mathlib.Condensed.Light.Functors Mathlib.NumberTheory.Zsqrtd.Basic Mathlib.RingTheory.IntegralClosure.Algebra.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree Mathlib.LinearAlgebra.AffineSpace.Matrix Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite Mathlib.MeasureTheory.Measure.AEMeasurable Mathlib.GroupTheory.Order.Min Mathlib.Analysis.Asymptotics.Asymptotics Mathlib.Algebra.GeomSum Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.FieldTheory.PerfectClosure Mathlib.LinearAlgebra.CliffordAlgebra.Prod Mathlib.MeasureTheory.Measure.WithDensity Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.Data.Complex.Basic Mathlib.RingTheory.Ideal.IdempotentFG Mathlib.MeasureTheory.Function.AEEqFun Mathlib.Algebra.Lie.Classical Mathlib.Algebra.CharP.Two Mathlib.RingTheory.MvPowerSeries.Trunc Mathlib.MeasureTheory.Function.SimpleFuncDense Mathlib.Data.Complex.Abs Mathlib.LinearAlgebra.PiTensorProduct Mathlib.Analysis.SpecialFunctions.Complex.Circle Mathlib.Topology.Order.IntermediateValue Mathlib.NumberTheory.Liouville.Residual Mathlib.Topology.Algebra.Order.Floor Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries Mathlib.Algebra.Homology.Bifunctor Mathlib.Analysis.Analytic.Inverse Mathlib.Algebra.Polynomial.Bivariate Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.Analysis.NormedSpace.FunctionSeries Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma Mathlib.Geometry.Euclidean.Triangle Mathlib.AlgebraicGeometry.Restrict Mathlib.Algebra.Order.Archimedean.Hom Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.Analysis.Normed.Operator.Compact Mathlib.Topology.Algebra.Module.Alternating.Basic Mathlib.RingTheory.MvPowerSeries.Basic Mathlib.Data.Int.CardIntervalMod Mathlib.Analysis.NormedSpace.IndicatorFunction Mathlib.Algebra.Category.ModuleCat.Projective Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.RingTheory.MaximalSpectrum Mathlib.Topology.Algebra.Order.Rolle Mathlib.Algebra.Homology.HomotopyCofiber Mathlib.GroupTheory.SpecificGroups.KleinFour Mathlib.RingTheory.Unramified.Derivations Mathlib.Probability.Distributions.Gamma Mathlib.LinearAlgebra.Eigenspace.Zero Mathlib.Algebra.Polynomial.Roots Mathlib.Dynamics.Ergodic.Action.Basic Mathlib.AlgebraicTopology.KanComplex Mathlib.Analysis.Normed.Group.Constructions Mathlib.RingTheory.Ideal.Basic Mathlib.Probability.Martingale.OptionalStopping Mathlib.RingTheory.Flat.Stability Mathlib.Data.Nat.Choose.Central Mathlib.Probability.Martingale.BorelCantelli Mathlib.Analysis.SpecialFunctions.ExpDeriv Mathlib.RingTheory.FiniteType Mathlib.RingTheory.Ideal.Basis Mathlib.Condensed.Functors Mathlib.Geometry.Manifold.DerivationBundle Mathlib.LinearAlgebra.Eigenspace.Minpoly Mathlib.MeasureTheory.Constructions.Projective Mathlib.Computability.Ackermann Mathlib.Algebra.Category.ModuleCat.Images Mathlib.Analysis.NormedSpace.BallAction Mathlib.MeasureTheory.Measure.MeasureSpace Mathlib.Algebra.CharP.IntermediateField Mathlib.MeasureTheory.Measure.MeasureSpaceDef Mathlib.MeasureTheory.Group.Action Mathlib.Probability.Density Mathlib.Dynamics.BirkhoffSum.NormedSpace Mathlib.Data.Nat.Factorization.PrimePow Mathlib.LinearAlgebra.Projectivization.Subspace Mathlib.Topology.Category.TopCommRingCat Mathlib.Analysis.Convex.Caratheodory Mathlib.Analysis.Complex.RealDeriv Mathlib.Analysis.Complex.OpenMapping Mathlib.AlgebraicGeometry.PrimeSpectrum.IsOpenComapC Mathlib.MeasureTheory.OuterMeasure.Basic Mathlib.Probability.ProbabilityMassFunction.Integrals Mathlib.MeasureTheory.Function.AEMeasurableSequence Mathlib.Condensed.Equivalence Mathlib.Data.Complex.Orientation Mathlib.RingTheory.Polynomial.RationalRoot Mathlib.Analysis.Convex.Quasiconvex Mathlib.Analysis.Calculus.Dslope Mathlib.RingTheory.WittVector.FrobeniusFractionField Mathlib.Topology.Algebra.Module.CharacterSpace Mathlib.Data.ENNReal.Basic Mathlib.LinearAlgebra.Matrix.ToLinearEquiv Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Topology.Homotopy.Equiv Mathlib.RingTheory.Ideal.Prod Mathlib.Algebra.Polynomial.CancelLeads Mathlib.Analysis.NormedSpace.Connected Mathlib.Algebra.MvPolynomial.Degrees Mathlib.Topology.Category.Profinite.Product Mathlib.RingTheory.IntegralDomain Mathlib.Topology.Homotopy.HSpaces Mathlib.Topology.Category.Profinite.Limits Mathlib.Topology.MetricSpace.Completion Mathlib.Analysis.ODE.PicardLindelof Mathlib.GroupTheory.SpecificGroups.Dihedral Mathlib.RingTheory.RootsOfUnity.Minpoly Mathlib.Topology.Instances.NNReal Mathlib.RingTheory.Localization.Cardinality Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.Probability.ConditionalExpectation Mathlib.Analysis.Calculus.LogDeriv Mathlib.FieldTheory.Tower Mathlib.MeasureTheory.Measure.Haar.Basic Mathlib.MeasureTheory.Integral.SetIntegral Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs Mathlib.RingTheory.HahnSeries.Multiplication Mathlib.Analysis.Calculus.Deriv.Slope Mathlib.NumberTheory.FLT.Basic Mathlib.Analysis.Analytic.Polynomial Mathlib.Algebra.Homology.HomologySequence Mathlib.SetTheory.Cardinal.Finite Mathlib.RingTheory.PrimeSpectrum Mathlib.Analysis.SpecificLimits.RCLike Mathlib.Analysis.InnerProductSpace.ConformalLinearMap Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.Algebra.CharP.MixedCharZero Mathlib.GroupTheory.Frattini Mathlib.Algebra.Polynomial.Identities Mathlib.RingTheory.WittVector.DiscreteValuationRing Mathlib.Data.Set.Card Mathlib.Geometry.Manifold.LocalDiffeomorph Mathlib.Data.Finsupp.Order Mathlib.Analysis.NormedSpace.Multilinear.Basic Mathlib.FieldTheory.PolynomialGaloisGroup Mathlib.Algebra.CharP.CharAndCard Mathlib.Topology.Metrizable.Uniformity Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.MeasureTheory.Constructions.BorelSpace.Real Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.Topology.Metrizable.ContinuousMap Mathlib.Algebra.Order.Nonneg.Floor Mathlib.Algebra.Polynomial.EraseLead Mathlib.Algebra.MvPolynomial.Invertible Mathlib.GroupTheory.PGroup Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian Mathlib.RingTheory.RingHom.Surjective Mathlib.NumberTheory.ModularForms.CongruenceSubgroups Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward Mathlib.LinearAlgebra.TensorProduct.Graded.Internal Mathlib.LinearAlgebra.Dimension.Finite Mathlib.Analysis.LocallyConvex.BalancedCoreHull Mathlib.RingTheory.DedekindDomain.PID Mathlib.SetTheory.Cardinal.Ordinal Mathlib.Analysis.SpecialFunctions.Pow.NNReal Mathlib.Algebra.Category.Grp.Injective Mathlib.RingTheory.FreeRing Mathlib.MeasureTheory.Constructions.BorelSpace.Order Mathlib.FieldTheory.AxGrothendieck Mathlib.Analysis.Convex.StoneSeparation Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.LinearAlgebra.RootSystem.RootPositive Mathlib.Tactic Mathlib.AlgebraicTopology.SimplicialCategory.Basic Mathlib.MeasureTheory.Integral.Indicator Mathlib.Algebra.Module.LocalizedModule Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.Algebra.Star.Unitary Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.Geometry.Euclidean.PerpBisector Mathlib.Topology.Order.IsLUB Mathlib.Topology.Algebra.InfiniteSum.Real Mathlib.Analysis.Normed.Group.Rat Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.Topology.MetricSpace.Closeds Mathlib.LinearAlgebra.FiniteSpan Mathlib.MeasureTheory.Group.Integral Mathlib.Topology.ContinuousFunction.StoneWeierstrass Mathlib.Topology.Algebra.ContinuousAffineMap Mathlib.Analysis.Convex.Radon Mathlib.LinearAlgebra.Matrix.IsDiag Mathlib.Algebra.Category.Ring.Adjunctions Mathlib.Algebra.Lie.TensorProduct Mathlib.Algebra.Homology.HomotopyCategory Mathlib.FieldTheory.SplittingField.Construction Mathlib.Analysis.Normed.Affine.ContinuousAffineMap Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Topology.Sheaves.Sheafify Mathlib.Topology.MetricSpace.DilationEquiv Mathlib.FieldTheory.RatFunc.Basic Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.Topology.Semicontinuous Mathlib.RingTheory.Support Mathlib.Algebra.Lie.Weights.Linear Mathlib.RingTheory.Unramified.Finite Mathlib.MeasureTheory.Measure.EverywherePos Mathlib.Topology.Instances.TrivSqZeroExt Mathlib.GroupTheory.Archimedean Mathlib.LinearAlgebra.Matrix.Determinant.Basic Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic Mathlib.RepresentationTheory.Maschke Mathlib.Analysis.BoxIntegral.Partition.Split Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.Probability.Integration Mathlib.Analysis.SpecificLimits.Basic Mathlib.GroupTheory.Perm.Cycle.Type Mathlib.MeasureTheory.Function.EssSup Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit Mathlib.NumberTheory.Bertrand Mathlib.RingTheory.Valuation.Basic Mathlib.Analysis.Calculus.LocalExtr.Rolle Mathlib.Algebra.Category.HopfAlgebraCat.Basic Mathlib.MeasureTheory.OuterMeasure.AE Mathlib.GroupTheory.Schreier Mathlib.RingTheory.NormTrace Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean Mathlib.MeasureTheory.Measure.Complex Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.RingTheory.Localization.FractionRing Mathlib.RingTheory.TensorProduct.Basic Mathlib.ModelTheory.ElementaryMaps Mathlib.Combinatorics.SimpleGraph.AdjMatrix Mathlib.Algebra.Module.GradedModule Mathlib.Algebra.Polynomial.Degree.TrailingDegree Mathlib.Topology.Order.MonotoneContinuity Mathlib.Geometry.Manifold.Metrizable Mathlib.Topology.Algebra.Module.Cardinality Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.RingTheory.Valuation.RankOne Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.NumberTheory.LSeries.Convolution Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.MeasureTheory.Function.Floor Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.LinearAlgebra.Dimension.RankNullity Mathlib.LinearAlgebra.Basis.Flag Mathlib.Analysis.Normed.Operator.ContinuousLinearMap Mathlib.Algebra.Ring.NegOnePow Mathlib.Analysis.Normed.Group.AddTorsor Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.Combinatorics.Derangements.Finite Mathlib.Analysis.Calculus.LocalExtr.LineDeriv Mathlib.LinearAlgebra.Basis.Cardinality Mathlib.MeasureTheory.Measure.WithDensityVectorMeasure Mathlib.LinearAlgebra.Matrix.NonsingularInverse Mathlib.Algebra.Homology.BifunctorShift Mathlib.Algebra.Polynomial.Cardinal Mathlib.Algebra.Lie.InvariantForm Mathlib.Topology.Algebra.Module.Star Mathlib.ModelTheory.Satisfiability Mathlib.Algebra.Order.Archimedean.Basic Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Data.Matroid.Sum Mathlib.Analysis.NormedSpace.SphereNormEquiv Mathlib.Topology.Order.Category.FrameAdjunction Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.FieldTheory.RatFunc.Degree Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.RingTheory.QuotientNoetherian Mathlib.RingTheory.RootsOfUnity.Basic Mathlib.RingTheory.Localization.Away.AdjoinRoot Mathlib.Algebra.Lie.CartanExists Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated Mathlib.Algebra.Order.AbsoluteValue Mathlib.Analysis.SpecialFunctions.Trigonometric.Series Mathlib.Algebra.Polynomial.Module.AEval Mathlib.MeasureTheory.Integral.Average Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.Analysis.Convex.PartitionOfUnity Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.Combinatorics.SimpleGraph.Matching Mathlib.LinearAlgebra.FreeModule.Basic Mathlib.Topology.Sheaves.Stalks Mathlib.Tactic.NormNum.GCD Mathlib.Probability.Independence.Conditional Mathlib.Analysis.Complex.AbelLimit Mathlib.Algebra.FreeAlgebra Mathlib.Analysis.SpecialFunctions.Sqrt Mathlib.Analysis.Normed.Group.Hom Mathlib.RingTheory.PowerSeries.Trunc Mathlib.NumberTheory.Padics.PadicVal Mathlib.GroupTheory.Perm.Subgroup Mathlib.Analysis.NormedSpace.Pointwise Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.MeasureTheory.Integral.Lebesgue Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.Algebra.ModEq Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog Mathlib.Order.Filter.CardinalInter Mathlib.RingTheory.Perfection Mathlib.Analysis.Normed.Group.Basic Mathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Algebra.Homology.ConcreteCategory Mathlib.Analysis.SpecialFunctions.Log.ERealExp Mathlib.RingTheory.Norm.Basic Mathlib.Data.Real.Pi.Wallis Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Notation Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.FunctionField Mathlib.Algebra.DirectSum.LinearMap Mathlib.Topology.Algebra.InfiniteSum.Constructions Mathlib.Probability.CDF Mathlib.Tactic.NormNum Mathlib.Algebra.Group.ConjFinite Mathlib.Topology.Baire.CompleteMetrizable Mathlib.LinearAlgebra.ExteriorAlgebra.Basic Mathlib.MeasureTheory.Function.SimpleFunc Mathlib.Algebra.BigOperators.Module Mathlib.NumberTheory.DiophantineApproximation Mathlib.Data.Nat.Totient Mathlib.RingTheory.PowerSeries.Basic Mathlib.RingTheory.TensorProduct.MvPolynomial Mathlib.LinearAlgebra.TensorProduct.Vanishing Mathlib.Algebra.Module.Submodule.Pointwise Mathlib.MeasureTheory.Group.Defs Mathlib.Algebra.Polynomial.Smeval Mathlib.Analysis.Convex.Exposed Mathlib.RingTheory.Localization.Algebra Mathlib.Order.KrullDimension Mathlib.Topology.MetricSpace.Pseudo.Defs Mathlib.LinearAlgebra.Matrix.Dual Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors Mathlib.Analysis.Normed.Module.Completion Mathlib.CategoryTheory.Preadditive.Yoneda.Limits Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.Topology.Instances.Sign Mathlib.Topology.MetricSpace.Pseudo.Constructions Mathlib.LinearAlgebra.Basis.VectorSpace Mathlib.Data.Complex.ExponentialBounds Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.Topology.Instances.ENNReal Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic Mathlib.Probability.Martingale.Centering Mathlib.Algebra.Lie.OfAssociative Mathlib.Topology.Category.Stonean.Limits Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat Mathlib.GroupTheory.FreeAbelianGroup Mathlib.RingTheory.PowerSeries.Inverse Mathlib.LinearAlgebra.QuadraticForm.Dual Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.Topology.Instances.RatLemmas Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.Algebra.Polynomial.Div Mathlib.Topology.MetricSpace.Bounded Mathlib.LinearAlgebra.Matrix.Block Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.LinearAlgebra.FreeProduct.Basic Mathlib.Geometry.Manifold.VectorBundle.SmoothSection Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.Geometry.Manifold.ContMDiff.Product Mathlib.LinearAlgebra.RootSystem.Defs Mathlib.Algebra.Homology.Embedding.TruncGE Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.LinearAlgebra.Projectivization.Basic Mathlib.RingTheory.WittVector.MulP Mathlib.LinearAlgebra.Quotient Mathlib.Topology.Algebra.Order.Archimedean Mathlib.Analysis.Normed.Algebra.UnitizationL1 Mathlib.Topology.Algebra.ContinuousMonoidHom Mathlib.Topology.MetricSpace.MetricSeparated Mathlib.Data.Nat.Factorial.SuperFactorial |
1 |
Mathlib.Algebra.Order.Ring.Unbundled.Rat |
376 |
Declarations diff
+ instance : CovariantClass ℚ ℚ (· + ·) (· ≤ ·)
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
1 task
|
This PR/issue depends on: |
b91ddb3 to
35b6de6
Compare
…ed algebra results Author: Matthew Ballard <matt@mrb.email> Date: Fri Aug 9 13:48:05 2024 -0400
35b6de6 to
e675f84
Compare
eric-wieser
reviewed
Aug 16, 2024
Contributor
|
I think it's a good change, but I'm curious if there are performance benefits. !bench |
Contributor
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit 51253bc. |
Contributor
Author
|
@j-loreaux about what I would expect for this step, the next step #15072 should be more interesting since |
Contributor
|
bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Aug 17, 2024
…ed algebra results (#15071) We split off all but the `LinearOrderedCommRing` and the inferred `OrderedAddCommMonoid` instances on `Rat` into `Algebra.Order.Ring.Unbundled.Rat` as these results do not require bundled ordered algebra classes.
Contributor
|
Pull request successfully merged into master. Build succeeded: |
bjoernkjoshanssen
pushed a commit
that referenced
this pull request
Sep 9, 2024
…ed algebra results (#15071) We split off all but the `LinearOrderedCommRing` and the inferred `OrderedAddCommMonoid` instances on `Rat` into `Algebra.Order.Ring.Unbundled.Rat` as these results do not require bundled ordered algebra classes.
bjoernkjoshanssen
pushed a commit
that referenced
this pull request
Sep 9, 2024
…ed algebra results (#15071) We split off all but the `LinearOrderedCommRing` and the inferred `OrderedAddCommMonoid` instances on `Rat` into `Algebra.Order.Ring.Unbundled.Rat` as these results do not require bundled ordered algebra classes.
bjoernkjoshanssen
pushed a commit
that referenced
this pull request
Sep 12, 2024
…ed algebra results (#15071) We split off all but the `LinearOrderedCommRing` and the inferred `OrderedAddCommMonoid` instances on `Rat` into `Algebra.Order.Ring.Unbundled.Rat` as these results do not require bundled ordered algebra classes.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
We split off all but the
LinearOrderedCommRingand the inferredOrderedAddCommMonoidinstances onRatintoAlgebra.Order.Ring.Unbundled.Ratas these results do not require bundled ordered algebra classes.