[Merged by Bors] - chore (Algebra.Order.Group.Defs): split out unbundled ordered algebra results to Algebra.Order.Group.Unbundled.Basic

[mattrobball]

Currently, you have to import bundled ordered algebra to use these facts about unbundled ordered algebra classes. This should be unnecessary.

---

[github-actions]

PR summary aca313f01b

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Order.Group.OrderIso	226	225	-1 (-0.44%)
Mathlib.Order.ConditionallyCompleteLattice.Group	346	345	-1 (-0.29%)

Import changes for all files

Files	Import difference
Too many changes (2872)!

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[adomani]

Import changes for all files

Files	Import difference
5 files Mathlib.Algebra.Order.Group.Lattice Mathlib.Algebra.Order.Pointwise Mathlib.Algebra.Order.Group.OrderIso Mathlib.Order.ConditionallyCompleteLattice.Group Mathlib.Algebra.Bounds	-1
2895 files Mathlib.Algebra.Homology.ShortComplex.Ab Mathlib.Data.Matroid.Basic Mathlib.LinearAlgebra.FreeModule.Norm Mathlib.Algebra.Ring.Subring.MulOpposite Mathlib.LinearAlgebra.Charpoly.Basic Mathlib.Topology.Category.Stonean.Adjunctions Mathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.Tactic.Ring.Basic Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.Order.Partition.Equipartition Mathlib.Analysis.Normed.Group.Uniform Mathlib.Data.Nat.Hyperoperation Mathlib.Data.Real.Hyperreal Mathlib.Algebra.Polynomial.FieldDivision Mathlib.Topology.Algebra.Monoid Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.Analysis.MeanInequalitiesPow Mathlib.Topology.Algebra.Module.Simple Mathlib.Algebra.Star.Module Mathlib.Analysis.Asymptotics.SpecificAsymptotics Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.RingTheory.IsAdjoinRoot Mathlib.CategoryTheory.Abelian.Generator Mathlib.Algebra.Module.Submodule.Bilinear Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Algebra.Star.NonUnitalSubalgebra Mathlib.Topology.Order.LawsonTopology Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.Topology.Algebra.InfiniteSum.Group Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs Mathlib.Probability.Process.HittingTime Mathlib.Combinatorics.Additive.ETransform Mathlib.LinearAlgebra.FinsuppVectorSpace Mathlib.LinearAlgebra.BilinearMap Mathlib.Algebra.Module.Zlattice.Covolume Mathlib.Data.Nat.Choose.Cast Mathlib.Algebra.Order.Interval.Set.Instances Mathlib.NumberTheory.Liouville.LiouvilleWith Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.Analysis.InnerProductSpace.Symmetric Mathlib.Analysis.Complex.Polynomial 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.CategoryTheory.Sites.Pullback 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.Topology.Algebra.Semigroup Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RingTheory.Localization.AtPrime Mathlib.MeasureTheory.MeasurableSpace.Embedding Mathlib.RingTheory.Ideal.LocalRing Mathlib.Data.Real.Pointwise Mathlib.Algebra.Ring.Action.Invariant Mathlib.Topology.CompactOpen 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.Control.Fix Mathlib.FieldTheory.Finite.Trace Mathlib.FieldTheory.IntermediateField Mathlib.ModelTheory.Ultraproducts Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.MeasureTheory.Constructions.BorelSpace.Metric Mathlib.CategoryTheory.Abelian.RightDerived Mathlib.RingTheory.AlgebraTower Mathlib.Data.Matrix.Auto Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits Mathlib.CategoryTheory.Sites.Coherent.Comparison Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff Mathlib.Topology.IndicatorConstPointwise Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four Mathlib.LinearAlgebra.DirectSum.Finsupp Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual Mathlib.LinearAlgebra.Matrix.ZPow Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Topology.ContinuousFunction.CompactlySupported Mathlib.Algebra.Category.ModuleCat.Limits Mathlib.GroupTheory.Submonoid.Inverses Mathlib.Analysis.Convex.AmpleSet Mathlib.Geometry.Manifold.LocalInvariantProperties Mathlib.RingTheory.Ideal.QuotientOperations Mathlib.Probability.Variance Mathlib.Algebra.BigOperators.Finsupp Mathlib.Data.Finset.Interval Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.Topology.MetricSpace.Antilipschitz Mathlib.Analysis.NormedSpace.OperatorNorm.Basic Mathlib.GroupTheory.CoprodI 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.Combinatorics.SimpleGraph.Connectivity.Subgraph Mathlib.SetTheory.Ordinal.NaturalOps Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Algebra.GCDMonoid.Nat Mathlib.AlgebraicTopology.SimplicialSet Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.LinearAlgebra.Finsupp Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Probability.Distributions.Geometric Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.LinearAlgebra.ExteriorAlgebra.Grading Mathlib.Algebra.Polynomial.Degree.Definitions Mathlib.Algebra.IsPrimePow Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.Analysis.Subadditive Mathlib.Analysis.NormedSpace.LinearIsometry 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.Combinatorics.Enumerative.DoubleCounting Mathlib.Geometry.Manifold.VectorBundle.Basic Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.LinearAlgebra.Projection Mathlib.Order.Grade Mathlib.Algebra.Category.Grp.EpiMono Mathlib.Algebra.EuclideanDomain.Instances Mathlib.Algebra.Homology.Opposite Mathlib.Data.NNReal.Star Mathlib.Topology.Algebra.UniformField Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.Analysis.SpecialFunctions.Pow.Complex Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.Analysis.Calculus.Deriv.Star Mathlib.Algebra.Module.Bimodule Mathlib.Tactic.FunProp.ContDiff Mathlib.MeasureTheory.Function.SpecialFunctions.Basic Mathlib.LinearAlgebra.SModEq Mathlib.Data.NNRat.BigOperators Mathlib.Algebra.Order.Interval.Basic Mathlib.Algebra.Order.Group.Units Mathlib.Tactic.NormNum.Prime Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Order.Filter.SmallSets Mathlib.Algebra.Category.Grp.Subobject Mathlib.LinearAlgebra.Span Mathlib.Algebra.Ring.Subring.Order Mathlib.Data.PNat.Find Mathlib.Data.Nat.WithBot Mathlib.RingTheory.WittVector.Domain Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.Topology.Homotopy.Contractible Mathlib.Data.Finset.Grade Mathlib.Algebra.Order.Ring.Basic Mathlib.Tactic.Positivity.Finset Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.Tactic.mwe_mvars_for_moveAdd Mathlib.Algebra.ContinuedFractions.Computation.Translations Mathlib.Geometry.Manifold.VectorBundle.Tangent Mathlib.Topology.DiscreteSubset Mathlib.Topology.Compactification.OnePoint Mathlib.RingTheory.Artinian Mathlib.Analysis.Calculus.Deriv.Add Mathlib.Topology.Instances.PNat Mathlib.LinearAlgebra.Matrix.MvPolynomial Mathlib.FieldTheory.Laurent Mathlib.Analysis.SpecialFunctions.CompareExp Mathlib.Topology.DenseEmbedding Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit Mathlib.LinearAlgebra.AffineSpace.Ordered Mathlib.NumberTheory.GaussSum Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.Algebra.Module.Submodule.Basic Mathlib.NumberTheory.Primorial Mathlib.Algebra.Homology.ShortComplex.SnakeLemma Mathlib.Topology.Algebra.Module.UniformConvergence Mathlib.Tactic.IntervalCases Mathlib.Algebra.Category.Ring.Instances Mathlib.Analysis.NormedSpace.Basic Mathlib.Data.Nat.Nth Mathlib.Data.NNReal.Basic Mathlib.Data.Finsupp.Basic Mathlib.Algebra.Lie.Quotient Mathlib.Geometry.Manifold.Diffeomorph Mathlib.Combinatorics.Derangements.Exponential Mathlib.LinearAlgebra.Dimension.DivisionRing Mathlib.Algebra.Order.Algebra Mathlib.Data.DFinsupp.Multiset Mathlib.LinearAlgebra.FreeModule.StrongRankCondition Mathlib.Analysis.NormedSpace.Unitization Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.MeasureTheory.Function.LpSeminorm.Basic Mathlib.Topology.UniformSpace.Ascoli 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.Topology.UniformSpace.Compact Mathlib.RingTheory.DedekindDomain.Ideal Mathlib.MeasureTheory.OuterMeasure.Caratheodory Mathlib.Algebra.Category.ModuleCat.Abelian Mathlib.Topology.MetricSpace.ShrinkingLemma Mathlib.Combinatorics.SimpleGraph.Clique Mathlib.RingTheory.Ideal.IsPrincipal Mathlib.Analysis.SpecialFunctions.Complex.Log Mathlib.MeasureTheory.Constructions.BorelSpace.Basic Mathlib.Probability.ProbabilityMassFunction.Monad Mathlib.MeasureTheory.OuterMeasure.Induced Mathlib.MeasureTheory.Measure.Regular Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.Analysis.Asymptotics.AsymptoticEquivalent Mathlib.Topology.Order.Lattice Mathlib.Algebra.Order.BigOperators.Ring.Finset Mathlib.Algebra.CharZero.Lemmas Mathlib.MeasureTheory.Group.MeasurableEquiv Mathlib.CategoryTheory.Abelian.Ext Mathlib.Topology.Sheaves.Sheaf Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.Analysis.Complex.AbsMax Mathlib.RingTheory.Ideal.Over Mathlib.RingTheory.Flat.Basic Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter Mathlib.adomaniLeanUtils.LFTCM_Duesseldorf_2023.exercises Mathlib.Topology.Partial Mathlib.RingTheory.GradedAlgebra.Noetherian Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Combinatorics.SimpleGraph.StronglyRegular Mathlib.Tactic.Ring.PNat Mathlib.Algebra.Ring.Subring.Pointwise Mathlib.Data.Nat.Factorial.DoubleFactorial Mathlib.Algebra.Module.Algebra 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.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.RingTheory.AdicCompletion.Basic Mathlib.Data.Matrix.Invertible Mathlib.Topology.Instances.Int Mathlib.Analysis.Convex.Topology Mathlib.Tactic.Linarith.Preprocessing Mathlib.RingTheory.Prime Mathlib.Geometry.Manifold.Complex Mathlib.Logic.Hydra Mathlib.LinearAlgebra.Coevaluation Mathlib.Algebra.Order.Monoid.ToMulBot Mathlib.Data.DFinsupp.Basic Mathlib.Data.Nat.SqrtNormNum Mathlib.mwe_thmLem Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.Geometry.Manifold.ChartedSpace Mathlib.Algebra.Lie.Submodule Mathlib.FieldTheory.AbelRuffini Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.CategoryTheory.Monoidal.Linear Mathlib.RingTheory.ClassGroup Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.RingTheory.Ideal.Maps Mathlib.Tactic.FunProp.AEMeasurable Mathlib.Analysis.Calculus.FDeriv.Linear Mathlib.Algebra.DirectSum.Module Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.GroupTheory.DoubleCoset Mathlib.Probability.StrongLaw Mathlib.Algebra.Order.Group.MinMax Mathlib.Data.Real.ENatENNReal Mathlib.GroupTheory.Perm.Sign Mathlib.Topology.Algebra.Ring.Basic Mathlib.Tactic.LinearCombination Mathlib.RingTheory.Regular.RegularSequence Mathlib.Topology.FiberBundle.Constructions Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.LinearAlgebra.Matrix.Diagonal Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.Data.Matrix.Basic Mathlib.Combinatorics.Hall.Basic Mathlib.RingTheory.Multiplicity Mathlib.RingTheory.Derivation.Lie Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.Data.ZMod.Module Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.RingTheory.Polynomial.Pochhammer Mathlib.Analysis.Complex.HalfPlane Mathlib.Data.Matrix.Basis Mathlib.Data.ENat.Basic Mathlib.Analysis.LocallyConvex.Bounded Mathlib.Algebra.Module.DedekindDomain Mathlib.RingTheory.WittVector.Compare Mathlib.Topology.Sets.Closeds Mathlib.GroupTheory.Perm.Cycle.Basic Mathlib.Algebra.Polynomial.SpecificDegree Mathlib.Data.Int.AbsoluteValue Mathlib.Algebra.MvPolynomial.Counit Mathlib.Algebra.Ring.Subsemiring.MulOpposite Mathlib.LinearAlgebra.Eigenspace.Matrix Mathlib.Topology.Order.ScottTopology Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.Algebra.MvPolynomial.Basic Mathlib.Analysis.Seminorm Mathlib.SetTheory.Ordinal.Notation Mathlib.Analysis.Complex.Isometry Mathlib.MeasureTheory.Measure.AEDisjoint Mathlib.RingTheory.Adjoin.PowerBasis Mathlib.Geometry.Manifold.MFDeriv.FDeriv Mathlib.GroupTheory.Coset Mathlib.Algebra.Order.Pi Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.Analysis.Convex.Side Mathlib.NumberTheory.ArithmeticFunction Mathlib.MeasureTheory.Function.L2Space Mathlib.Algebra.Order.BigOperators.Ring.List Mathlib.Data.Int.ConditionallyCompleteOrder Mathlib.GroupTheory.Coxeter.Matrix Mathlib.LinearAlgebra.AffineSpace.Pointwise Mathlib.Algebra.ContinuedFractions.Computation.Approximations Mathlib.Topology.VectorBundle.Hom Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.Analysis.Complex.UnitDisc.Basic Mathlib.Topology.Instances.CantorSet Mathlib.Analysis.SpecialFunctions.Exp Mathlib.Algebra.Polynomial.AlgebraMap Mathlib.RingTheory.Polynomial.Quotient Mathlib.Tactic.Positivity.Core Mathlib.Topology.ExtremallyDisconnected Mathlib.Topology.Category.TopCat.EpiMono Mathlib.RingTheory.AdicCompletion.Functoriality Mathlib.Topology.Bornology.BoundedOperation Mathlib.Algebra.CharP.LocalRing Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.LinearAlgebra.PID Mathlib.LinearAlgebra.Matrix.Reindex Mathlib.Topology.Sheaves.SheafCondition.Sites Mathlib.Data.Matroid.Map Mathlib.RingTheory.LaurentSeries Mathlib.Data.Int.Order.Lemmas Mathlib.NumberTheory.ModularForms.Identities Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.Analysis.NormedSpace.WeakDual Mathlib.Combinatorics.Enumerative.Composition Mathlib.Analysis.Normed.Group.CocompactMap Mathlib.Computability.AkraBazzi.GrowsPolynomially Mathlib.Geometry.Manifold.ContMDiffMap Mathlib.Analysis.NormedSpace.AddTorsor Mathlib.Algebra.MvPolynomial.Funext Mathlib.ModelTheory.Algebra.Ring.Basic Mathlib.CategoryTheory.Galois.GaloisObjects Mathlib.NumberTheory.NumberField.Norm Mathlib.Analysis.Convex.Body Mathlib.Topology.Category.Profinite.Nobeling Mathlib.Algebra.Order.Field.InjSurj Mathlib.Analysis.NormedSpace.RCLike Mathlib.adomaniLeanUtils.Sierpinski Mathlib.LinearAlgebra.AffineSpace.AffineEquiv Mathlib.LinearAlgebra.FreeModule.Determinant Mathlib.LinearAlgebra.DFinsupp Mathlib.Analysis.Complex.TaylorSeries Mathlib.Condensed.Light.Explicit Mathlib.Algebra.Algebra.Subalgebra.Operations Mathlib.NumberTheory.Divisors Mathlib.Algebra.Module.Submodule.Map Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions Mathlib.Probability.CondCount Mathlib.SetTheory.Game.Short Mathlib.Algebra.Ring.Divisibility.Lemmas Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.Data.Real.Sqrt Mathlib.Topology.ContinuousFunction.Ideals Mathlib.Tactic.Positivity Mathlib.LinearAlgebra.QuadraticForm.Prod Mathlib.FieldTheory.Galois Mathlib.CategoryTheory.Preadditive.Yoneda.Basic Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel Mathlib.Data.Analysis.Topology Mathlib.LinearAlgebra.TensorAlgebra.Grading Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas Mathlib.Data.Finsupp.Encodable Mathlib.RingTheory.Bialgebra.Hom Mathlib.GroupTheory.OrderOfElement Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev Mathlib.NumberTheory.FLT.Four Mathlib.Analysis.NormedSpace.Units Mathlib.Algebra.Polynomial.HasseDeriv Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated Mathlib.Topology.Compactness.LocallyCompact Mathlib.Probability.Distributions.Exponential Mathlib.Data.Matrix.PEquiv Mathlib.Algebra.RingQuot Mathlib.RingTheory.WittVector.MulCoeff Mathlib.CategoryTheory.Sites.Subsheaf 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.Algebra.Homology.ModuleCat Mathlib.Dynamics.PeriodicPts Mathlib.Topology.ShrinkingLemma Mathlib.Algebra.Order.Field.Power Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric Mathlib.RingTheory.Localization.BaseChange Mathlib.SetTheory.Cardinal.Basic Mathlib.Algebra.Lie.Nilpotent Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.adomaniLeanUtils.LFTCM_Duesseldorf_2023.S11A_Algebraic_Geometry_exercises_noSols Mathlib.Algebra.Order.Interval.Set.Group Mathlib.LinearAlgebra.Charpoly.ToMatrix Mathlib.SetTheory.Cardinal.UnivLE Mathlib.FieldTheory.Normal Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.RingTheory.DiscreteValuationRing.Basic Mathlib.Topology.CountableSeparatingOn Mathlib.CategoryTheory.Triangulated.Pretriangulated Mathlib.MeasureTheory.Group.Measure Mathlib.Topology.Order.ExtendFrom Mathlib.Probability.Kernel.Composition Mathlib.GroupTheory.FreeAbelianGroupFinsupp Mathlib.NumberTheory.Liouville.LiouvilleNumber Mathlib.NumberTheory.Zsqrtd.ToReal Mathlib.Algebra.Category.Grp.Abelian Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.Algebra.MonoidAlgebra.ToDirectSum 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.CategoryTheory.Sites.EpiMono Mathlib.GroupTheory.Abelianization Mathlib.Data.Rat.Encodable Mathlib.Algebra.Order.Group.Indicator Mathlib.Algebra.Order.Floor Mathlib.AlgebraicTopology.CechNerve Mathlib.CategoryTheory.Abelian.Opposite Mathlib.Order.Filter.FilterProduct Mathlib.Algebra.Category.AlgebraCat.Limits Mathlib.Probability.Martingale.Upcrossing Mathlib.Order.Filter.Ultrafilter Mathlib.AlgebraicTopology.Quasicategory Mathlib.Topology.Filter Mathlib.Order.JordanHolder Mathlib.Topology.Order.PartialSups Mathlib.RingTheory.Coalgebra.Basic Mathlib.CategoryTheory.Preadditive.Generator Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.Data.Nat.Cast.Field 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.Algebra.Polynomial.Splits Mathlib.Algebra.Algebra.Subalgebra.Tower Mathlib.Probability.Martingale.OptionalSampling Mathlib.RingTheory.Localization.AsSubring Mathlib.Analysis.BoxIntegral.Box.Basic Mathlib.RingTheory.Kaehler.Polynomial Mathlib.GroupTheory.Exponent Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Analysis.NormedSpace.Star.GelfandDuality Mathlib.Topology.UniformSpace.CompactConvergence Mathlib.Data.Set.Pointwise.Interval Mathlib.RingTheory.Localization.Finiteness Mathlib.RingTheory.WittVector.Identities Mathlib.Condensed.Module Mathlib.Analysis.NormedSpace.TrivSqZeroExt Mathlib.Data.Real.Sign Mathlib.Data.Int.NatPrime Mathlib.Topology.RestrictGenTopology 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.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.RingTheory.Polynomial.Dickson Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.Topology.Sheaves.Forget Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.Analysis.Calculus.BumpFunction.Basic Mathlib.Algebra.Order.Nonneg.Ring Mathlib.Analysis.Calculus.FDeriv.Star Mathlib.SetTheory.Game.Nim Mathlib.Algebra.MvPolynomial.Expand Mathlib.Order.Filter.Subsingleton Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.Topology.ContinuousFunction.ContinuousMapZero Mathlib.LinearAlgebra.Matrix.Gershgorin Mathlib.Algebra.DualQuaternion Mathlib.RingTheory.Localization.Integral Mathlib.Analysis.NormedSpace.RieszLemma Mathlib.Topology.LocallyFinite Mathlib.Algebra.Order.Module.Algebra Mathlib.adomaniLeanUtils.LFTCM_Duesseldorf_2023.AG_presentation Mathlib.ModelTheory.Substructures Mathlib.Analysis.Calculus.FDeriv.Bilinear Mathlib.Algebra.Lie.Derivation.Killing Mathlib.Topology.Order.LocalExtr Mathlib.RingTheory.AdicCompletion.Exactness Mathlib.LinearAlgebra.Dimension.Finrank 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.Data.DFinsupp.WellFounded Mathlib.MeasureTheory.OuterMeasure.OfFunction Mathlib.Algebra.Order.Group.Instances Mathlib.Topology.Order Mathlib.NumberTheory.RamificationInertia Mathlib.Data.Nat.Squarefree Mathlib.Algebra.Homology.HomotopyCategory.MappingCone Mathlib.Topology.MetricSpace.PartitionOfUnity Mathlib.NumberTheory.SiegelsLemma Mathlib.LinearAlgebra.JordanChevalley Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.Analysis.SpecialFunctions.PolynomialExp Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.Algebra.Category.ModuleCat.Injective Mathlib.LinearAlgebra.TensorProduct.Prod 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.NumberTheory.ClassNumber.AdmissibleAbs Mathlib.Algebra.TrivSqZeroExt Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.Algebra.Module.Submodule.Range Mathlib.RepresentationTheory.Rep Mathlib.Combinatorics.Additive.AP.Three.Defs Mathlib.Analysis.Calculus.Deriv.Linear Mathlib.Data.Matroid.Dual Mathlib.Analysis.NormedSpace.Complemented Mathlib.AlgebraicGeometry.EllipticCurve.Affine Mathlib.AlgebraicGeometry.EllipticCurve.Group Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic Mathlib.Topology.LocalAtTarget Mathlib.Algebra.Star.Subalgebra Mathlib.Analysis.NormedSpace.UnitizationL1 Mathlib.NumberTheory.Padics.PadicNumbers Mathlib.Algebra.Order.Ring.Finset Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.LinearAlgebra.Matrix.Determinant.Misc Mathlib.MeasureTheory.Function.LpSeminorm.Trim Mathlib.Algebra.Quandle Mathlib.Analysis.PSeries Mathlib.LinearAlgebra.Multilinear.Basic Mathlib.NumberTheory.Harmonic.Defs Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.MeasureTheory.Function.LpSpace Mathlib.MeasureTheory.Group.Arithmetic Mathlib.NumberTheory.ModularForms.SlashActions Mathlib.RingTheory.Polynomial.Hermite.Basic Mathlib.Algebra.Order.GroupWithZero.WithZero Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.LinearAlgebra.Multilinear.Basis Mathlib.Algebra.Ring.Subring.Basic Mathlib.Algebra.Homology.TotalComplexShift Mathlib.Analysis.NormedSpace.BoundedLinearMaps Mathlib.adomaniLeanUtils.move_add_short_test 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.Topology.LocallyConstant.Basic Mathlib.GroupTheory.Divisible Mathlib.Algebra.MonoidAlgebra.Support Mathlib.Algebra.CubicDiscriminant Mathlib.Topology.Order.ProjIcc Mathlib.RingTheory.NonUnitalSubsemiring.Basic Mathlib.Combinatorics.SimpleGraph.Density Mathlib.RingTheory.PrincipalIdealDomain Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat Mathlib.Analysis.Calculus.SmoothSeries Mathlib.Analysis.NormedSpace.Star.Unitization Mathlib.Topology.ContinuousFunction.CocompactMap Mathlib.RingTheory.Ideal.MinimalPrime Mathlib.GroupTheory.Nilpotent Mathlib.Topology.MetricSpace.Cauchy Mathlib.GroupTheory.GroupAction.FixedPoints Mathlib.RingTheory.Bialgebra.Basic Mathlib.GroupTheory.FreeGroup.NielsenSchreier Mathlib.RingTheory.WittVector.WittPolynomial Mathlib.adomaniLeanUtils.NoZeroDivisors_and_opposites Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.Topology.Order.Hom.Esakia Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff Mathlib.GroupTheory.CommutingProbability Mathlib.Algebra.Lie.Free Mathlib.adomaniLeanUtils.extractDecl1 Mathlib.Analysis.Calculus.FDeriv.Add Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Data.Rat.Denumerable Mathlib.Topology.Algebra.InfiniteSum.Module Mathlib.Analysis.Complex.Basic Mathlib.Data.Nat.Upto Mathlib.MeasureTheory.Function.AEMeasurableOrder Mathlib.Analysis.Convex.Intrinsic Mathlib.Topology.MetricSpace.Lipschitz Mathlib.LinearAlgebra.BilinearForm.Orthogonal Mathlib.Analysis.Calculus.Deriv.Polynomial Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.GroupTheory.Coxeter.Basic Mathlib.GroupTheory.NoncommPiCoprod Mathlib.RingTheory.Polynomial.IrreducibleRing Mathlib.Data.DFinsupp.NeLocus Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.AlgebraicGeometry.Spec Mathlib.MeasureTheory.Category.MeasCat Mathlib.RingTheory.Norm 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.Combinatorics.Additive.Energy Mathlib.Topology.Baire.LocallyCompactRegular 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.CategoryTheory.Localization.CalculusOfFractions.Preadditive Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.FieldTheory.SeparableDegree Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.Topology.Instances.Discrete Mathlib.FieldTheory.Minpoly.MinpolyDiv Mathlib.GroupTheory.MonoidLocalization Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.Algebra.DirectSum.Basic Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.RingTheory.PowerSeries.Derivative Mathlib.NumberTheory.LSeries.Deriv Mathlib.Data.Set.Equitable Mathlib.MeasureTheory.Constructions.Pi Mathlib.Topology.Spectral.Hom 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.Topology.PartialHomeomorph Mathlib.NumberTheory.EulerProduct.Basic Mathlib.Analysis.Fourier.AddCircle Mathlib.adomaniLeanUtils.LFTCM_Duesseldorf_2023.S11A_Algebraic_Geometry_exercises_withSols Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.MeasureTheory.Decomposition.UnsignedHahn Mathlib.LinearAlgebra.QuotientPi Mathlib.Topology.ClopenBox Mathlib.RingTheory.Nullstellensatz Mathlib.Probability.Cdf Mathlib.RingTheory.Noetherian Mathlib.GroupTheory.Coprod.Basic Mathlib.RingTheory.NonUnitalSubring.Basic Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.Topology.Algebra.ValuedField Mathlib.Data.Int.Interval Mathlib.RingTheory.Coprime.Lemmas Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Analysis.SpecialFunctions.Pow.Continuity Mathlib.Analysis.Calculus.MeanValue Mathlib.GroupTheory.SchurZassenhaus Mathlib.LinearAlgebra.Matrix.Polynomial Mathlib.Analysis.Fourier.Inversion 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.Analysis.Calculus.FDeriv.Pi Mathlib.CategoryTheory.Action Mathlib.Algebra.Polynomial.DenomsClearable Mathlib.LinearAlgebra.FreeModule.PID Mathlib.Dynamics.Ergodic.Conservative Mathlib.Topology.UniformSpace.CompareReals Mathlib.Algebra.Lie.IdealOperations Mathlib.Algebra.Vertex.HVertexOperator Mathlib.SetTheory.Game.Basic Mathlib.CategoryTheory.Triangulated.Triangulated Mathlib.Analysis.BoxIntegral.Box.SubboxInduction Mathlib.SetTheory.Ordinal.Arithmetic Mathlib.Algebra.Algebra.Subalgebra.Rank Mathlib.Algebra.Category.ModuleCat.Products Mathlib.Algebra.GroupWithZero.NonZeroDivisors Mathlib.Topology.Instances.AddCircle Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform Mathlib.Topology.Sequences Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv Mathlib.Algebra.Order.BigOperators.Ring.Multiset Mathlib.Topology.ContinuousFunction.Algebra Mathlib.Analysis.Convex.Slope Mathlib.Topology.Order.Monotone Mathlib.Probability.Kernel.WithDensity Mathlib.Order.LiminfLimsup Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.Topology.Algebra.WithZeroTopology Mathlib.Tactic.mwe_field_simp Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.Topology.Category.Profinite.AsLimit Mathlib.RingTheory.Ideal.Quotient Mathlib.Combinatorics.SimpleGraph.Triangle.Basic Mathlib.Combinatorics.SetFamily.Kleitman Mathlib.LinearAlgebra.Matrix.FiniteDimensional Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.Analysis.Calculus.Deriv.Pow Mathlib.Algebra.Algebra.Basic Mathlib.FieldTheory.Fixed Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic Mathlib.RingTheory.Adjoin.Field Mathlib.GroupTheory.Perm.Fin Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.AlgebraicGeometry.Pullbacks 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.Data.Nat.Fib.Basic Mathlib.Topology.Bornology.Absorbs Mathlib.Combinatorics.Derangements.Basic Mathlib.Analysis.Normed.Field.Basic Mathlib.Algebra.Category.MonCat.Limits Mathlib.Algebra.Algebra.Operations Mathlib.Topology.Order.LowerUpperTopology Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable Mathlib.Order.Filter.Pointwise Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.Tactic.Polyrith Mathlib.Analysis.Calculus.Taylor Mathlib.Data.ZMod.Coprime Mathlib.MeasureTheory.Group.AddCircle Mathlib.NumberTheory.DirichletCharacter.Basic Mathlib.Algebra.Star.StarAlgHom Mathlib.Algebra.Order.Field.Basic Mathlib.Probability.Independence.ZeroOne Mathlib.Topology.CompletelyRegular Mathlib.Algebra.Lie.Basic Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.Combinatorics.SimpleGraph.Regularity.Increment Mathlib.Tactic.Linarith.Frontend Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.Algebra.Lie.TraceForm Mathlib.Order.Filter.IndicatorFunction Mathlib.Analysis.Calculus.LHopital Mathlib.Analysis.Convex.Cone.Pointed Mathlib.adomaniLeanUtils.LFTCM_Duesseldorf_2023.S11A_Algebraic_Geometry_exercises Mathlib.Topology.Defs.Induced Mathlib.Algebra.Algebra.Subalgebra.Prod Mathlib.Algebra.Order.Monovary Mathlib.MeasureTheory.Function.UniformIntegrable Mathlib.Tactic.NormNum.NatFib Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv Mathlib.Order.Filter.ModEq 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.NumberTheory.ModularForms.SlashInvariantForms Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected Mathlib.Algebra.Ring.Subring.Units Mathlib.Geometry.Manifold.SmoothManifoldWithCorners Mathlib.Condensed.Basic Mathlib.MeasureTheory.Measure.NullMeasurable Mathlib.FieldTheory.SplittingField.IsSplittingField Mathlib.Algebra.Polynomial.Taylor Mathlib.FieldTheory.IsSepClosed Mathlib.Topology.UniformSpace.AbstractCompletion Mathlib.Topology.Category.TopCat.Basic Mathlib.Algebra.Lie.Killing Mathlib.SetTheory.Ordinal.Principal Mathlib.Algebra.Lie.Derivation.AdjointAction Mathlib.Data.Rat.BigOperators Mathlib.AlgebraicTopology.FundamentalGroupoid.Product Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.Data.Nat.ModEq Mathlib.Control.LawfulFix Mathlib.NumberTheory.FrobeniusNumber Mathlib.RingTheory.Polynomial.IntegralNormalization Mathlib.ModelTheory.Graph Mathlib.Topology.Clopen Mathlib.Analysis.NormedSpace.Spectrum Mathlib.Analysis.NormedSpace.AffineIsometry Mathlib.Probability.Distributions.Gaussian Mathlib.Probability.Kernel.CondDistrib Mathlib.Condensed.Light.TopComparison Mathlib.Topology.MetricSpace.Dilation 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.Algebra.Group.AddChar Mathlib.Topology.Sober Mathlib.RingTheory.Presentation Mathlib.ModelTheory.LanguageMap Mathlib.Analysis.LocallyConvex.Basic Mathlib.Topology.Defs.Sequences Mathlib.Topology.Separation Mathlib.ModelTheory.Encoding Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.Topology.ExtendFrom Mathlib.Geometry.Manifold.BumpFunction Mathlib.Analysis.Calculus.FDeriv.Extend Mathlib.Algebra.Lie.DirectSum Mathlib.GroupTheory.Perm.Option Mathlib.Topology.UniformSpace.CompleteSeparated Mathlib.RingTheory.MvPolynomial.Homogeneous Mathlib.Probability.Martingale.Basic Mathlib.Analysis.LocallyConvex.WeakDual Mathlib.RingTheory.Coprime.Ideal Mathlib.Data.Finsupp.Antidiagonal Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.Algebra.Squarefree.Basic Mathlib.Algebra.Polynomial.Expand Mathlib.RingTheory.FractionalIdeal.Basic Mathlib.FieldTheory.Finite.Polynomial Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.Topology.MetricSpace.ProperSpace Mathlib.CategoryTheory.Triangulated.HomologicalFunctor Mathlib.MeasureTheory.Measure.Content Mathlib.LinearAlgebra.FiniteDimensional Mathlib.RingTheory.MvPolynomial.Ideal Mathlib.Topology.Category.TopCat.Limits.Cofiltered Mathlib.Algebra.Order.Group.PosPart Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup Mathlib.Probability.Kernel.RadonNikodym Mathlib.RingTheory.Polynomial.Vieta Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.Algebra.Order.Ring.WithTop Mathlib.adomaniLeanUtils.LFTCM_Duesseldorf_2023.noSolutions 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.Topology.Bases Mathlib.LinearAlgebra.Orientation Mathlib.Topology.Homotopy.Basic Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.Algebra.DirectSum.Internal Mathlib.Data.Matrix.Block Mathlib.RingTheory.Derivation.ToSquareZero Mathlib.NumberTheory.LSeries.Basic Mathlib.RingTheory.Valuation.ValuationRing Mathlib.Analysis.NormedSpace.Exponential Mathlib.Geometry.Manifold.ContMDiffMFDeriv Mathlib.Analysis.LocallyConvex.AbsConvex Mathlib.ModelTheory.Definability Mathlib.Algebra.Order.Nonneg.Field 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.Geometry.Manifold.ContMDiff.Basic Mathlib.Data.ZMod.IntUnitsPower Mathlib.MeasureTheory.Measure.WithDensityFinite Mathlib.MeasureTheory.Measure.Sub Mathlib.Topology.Algebra.Star Mathlib.Geometry.Euclidean.Sphere.Power Mathlib.Topology.Homotopy.Product Mathlib.Data.Nat.Dist Mathlib.Topology.Instances.Real Mathlib.Data.Ordmap.Ordset Mathlib.RingTheory.FinitePresentation Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Topology.Metrizable.Urysohn Mathlib.Analysis.Convex.SimplicialComplex.Basic Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal Mathlib.Data.Bool.Count Mathlib.LinearAlgebra.Semisimple Mathlib.Order.Filter.Cofinite Mathlib.FieldTheory.AbsoluteGaloisGroup Mathlib.LinearAlgebra.RootSystem.Basic Mathlib.Order.Monotone.Odd 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.RingTheory.IntegralClosure Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.MeasureTheory.Measure.GiryMonad Mathlib.adomaniLeanUtils.importAutocomplete 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.Complex.UpperHalfPlane.Topology Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.NormedSpace.CompactOperator Mathlib.Algebra.Algebra.Opposite Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus Mathlib.RepresentationTheory.Invariants Mathlib.RingTheory.Valuation.Integral Mathlib.Topology.Homeomorph Mathlib.GroupTheory.Perm.DomMulAct Mathlib.RingTheory.Coalgebra.Hom Mathlib.Combinatorics.SimpleGraph.Ends.Defs Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.Data.Nat.SuccPred 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.Topology.Basic Mathlib.Probability.Martingale.Convergence Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.Condensed.Solid Mathlib.Topology.List Mathlib.Analysis.Convex.SpecificFunctions.Pow Mathlib.FieldTheory.KrullTopology Mathlib.Analysis.Complex.UpperHalfPlane.Metric Mathlib.RingTheory.LittleWedderburn Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential Mathlib.Algebra.Homology.HomotopyCategory.Triangulated Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.Topology.Tactic Mathlib.Analysis.Normed.Group.Seminorm Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner Mathlib.Probability.Kernel.IntegralCompProd Mathlib.LinearAlgebra.TensorAlgebra.Basic Mathlib.RingTheory.Localization.Submodule Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.RingTheory.Localization.Integer Mathlib.LinearAlgebra.TensorAlgebra.Basis Mathlib.CategoryTheory.Sites.Coherent.Basic Mathlib.GroupTheory.ClassEquation Mathlib.Algebra.Tropical.Lattice Mathlib.CategoryTheory.Sites.LocallyInjective 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.Module.Defs Mathlib.Algebra.Order.Nonneg.Module Mathlib.SetTheory.Ordinal.Exponential Mathlib.Algebra.Order.CauSeq.Completion Mathlib.Algebra.Order.Ring.Star Mathlib.RingTheory.Generators Mathlib.Analysis.InnerProductSpace.Basic Mathlib.Algebra.Homology.Embedding.Basic Mathlib.RingTheory.Adjoin.Tower Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.Combinatorics.SimpleGraph.Regularity.Energy Mathlib.Data.Complex.Determinant Mathlib.Tactic.Monotonicity Mathlib.Order.Filter.ZeroAndBoundedAtFilter Mathlib.Analysis.Complex.OperatorNorm Mathlib.Analysis.NormedSpace.Dual Mathlib.Analysis.NormedSpace.Star.Spectrum Mathlib.AlgebraicTopology.SingularSet Mathlib.Algebra.Tropical.Basic Mathlib.Data.Finset.Finsupp 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.Algebra.Field.Rat Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.LinearAlgebra.AffineSpace.MidpointZero Mathlib.Analysis.Calculus.Deriv.ZPow Mathlib.Algebra.Module.Card Mathlib.Topology.NhdsSet Mathlib.Algebra.Polynomial.Mirror Mathlib.LinearAlgebra.TensorProduct.Finiteness Mathlib.Algebra.Algebra.Unitization Mathlib.Data.Rat.Cast.Defs Mathlib.Analysis.Convex.Integral Mathlib.Analysis.NormedSpace.FiniteDimension Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.GroupTheory.QuotientGroup Mathlib.Topology.MetricSpace.Equicontinuity Mathlib.Algebra.CharP.Invertible Mathlib.LinearAlgebra.DirectSum.TensorProduct Mathlib.Topology.Category.CompHaus.Projective Mathlib.Topology.Gluing Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace Mathlib.Algebra.DirectSum.Decomposition Mathlib.CategoryTheory.Preadditive.Mat Mathlib.RingTheory.Nilpotent.Lemmas Mathlib.Topology.Connected.LocallyConnected Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors Mathlib.MeasureTheory.Measure.Trim Mathlib.Topology.UniformSpace.Basic Mathlib.RingTheory.Polynomial.Bernstein Mathlib.Analysis.Normed.Group.Completeness Mathlib.Analysis.NormedSpace.MatrixExponential Mathlib.Topology.Sets.Order Mathlib.CategoryTheory.Abelian.Refinements Mathlib.Analysis.Normed.Group.ZeroAtInfty Mathlib.Algebra.LinearRecurrence Mathlib.Data.BitVec Mathlib.MeasureTheory.Constructions.Prod.Integral Mathlib.CategoryTheory.Quotient.Linear Mathlib.Analysis.NormedSpace.Star.Basic Mathlib.Algebra.MonoidAlgebra.Degree Mathlib.Topology.Algebra.StarSubalgebra Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian Mathlib.GroupTheory.FiniteAbelian Mathlib.Combinatorics.SetFamily.Compression.UV Mathlib.Analysis.LocallyConvex.StrongTopology Mathlib.Analysis.Convex.Cone.Extension Mathlib.Algebra.Polynomial.PartialFractions Mathlib.Topology.UniformSpace.Matrix Mathlib.adomaniLeanUtils.LFTCM_Duesseldorf_2023.API_advice Mathlib.LinearAlgebra.CliffordAlgebra.Star Mathlib.NumberTheory.PythagoreanTriples Mathlib.Algebra.MonoidAlgebra.Ideal Mathlib.Topology.MetricSpace.Isometry Mathlib.Tactic.Linarith Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.LinearAlgebra.BilinearForm.Hom Mathlib.Algebra.MvPolynomial.Rename Mathlib.Data.Int.Log Mathlib.LinearAlgebra.AffineSpace.Basis Mathlib.Analysis.NormedSpace.ConformalLinearMap Mathlib.Algebra.Algebra.Pi Mathlib.Data.Nat.Choose.Dvd Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.SetTheory.Game.Birthday Mathlib.Computability.Halting Mathlib.MeasureTheory.Integral.Layercake Mathlib.LinearAlgebra.Matrix.DotProduct Mathlib.MeasureTheory.Decomposition.Jordan Mathlib.Analysis.BoxIntegral.Partition.Additive Mathlib.Combinatorics.Additive.FreimanHom Mathlib.Algebra.Category.Grp.FilteredColimits Mathlib.Analysis.Complex.ReImTopology Mathlib.RingTheory.ZMod Mathlib.Algebra.Polynomial.Monic Mathlib.Geometry.Euclidean.Circumcenter Mathlib.LinearAlgebra.Matrix.Nondegenerate Mathlib.Data.Matrix.Reflection Mathlib.Algebra.Module.Projective Mathlib.Analysis.Calculus.Deriv.Basic Mathlib.LinearAlgebra.CrossProduct Mathlib.Analysis.Complex.Schwarz Mathlib.Data.DFinsupp.Interval 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.Topology.Hom.Open Mathlib.Dynamics.Newton Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.RingTheory.FiniteStability Mathlib.RingTheory.Localization.InvSubmonoid Mathlib.Topology.Algebra.MulAction Mathlib.Analysis.Calculus.DiffContOnCl Mathlib.Algebra.Ring.Identities Mathlib.Algebra.BigOperators.Intervals Mathlib.Analysis.Complex.UpperHalfPlane.Manifold Mathlib.Analysis.Convex.Join Mathlib.LinearAlgebra.Matrix.Permutation Mathlib.Tactic.CancelDenoms Mathlib.adomaniLeanUtils.extractDeclData Mathlib.LinearAlgebra.TensorProduct.Matrix Mathlib.Analysis.SpecialFunctions.Complex.Arg Mathlib.Topology.Category.Profinite.Projective Mathlib.Algebra.Order.GroupWithZero.Canonical Mathlib.Topology.PartitionOfUnity Mathlib.Algebra.Polynomial.Coeff Mathlib.Analysis.NormedSpace.Multilinear.Curry Mathlib.CategoryTheory.Monoidal.Tor Mathlib.FieldTheory.Finite.GaloisField Mathlib.Analysis.NormedSpace.BanachSteinhaus Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.Algebra.Algebra.Subalgebra.Pointwise Mathlib.FieldTheory.MvPolynomial Mathlib.RepresentationTheory.Character Mathlib.Algebra.Order.Floor.Prime Mathlib.Analysis.SumOverResidueClass Mathlib.NumberTheory.SmoothNumbers Mathlib.Algebra.CharP.Defs Mathlib.Algebra.MvPolynomial.Derivation Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.MeasureTheory.Covering.OneDim Mathlib.Topology.TietzeExtension Mathlib.Algebra.Homology.Embedding.Extend Mathlib.Analysis.NormedSpace.ContinuousAffineMap Mathlib.Algebra.Category.Ring.FilteredColimits Mathlib.Topology.ContinuousFunction.Basic Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower Mathlib.Data.Real.Pi.Leibniz Mathlib.Topology.Category.TopCat.OpenNhds Mathlib.Algebra.CharP.Subring 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.Analysis.NormedSpace.Algebra Mathlib.Combinatorics.SimpleGraph.Finsubgraph 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.Topology.MetricSpace.Polish Mathlib.RingTheory.Nakayama Mathlib.Analysis.SpecialFunctions.Polynomials Mathlib.Topology.MetricSpace.Infsep Mathlib.Data.Set.Semiring 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.LinearAlgebra.Matrix.GeneralLinearGroup Mathlib.Topology.Instances.Rat Mathlib.Algebra.Homology.HomotopyCategory.HomComplex Mathlib.RingTheory.Algebraic Mathlib.NumberTheory.NumberField.Units.Basic 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.Probability.Distributions.Uniform Mathlib.Tactic.ComputeDegree Mathlib.SetTheory.Surreal.Dyadic Mathlib.Geometry.Euclidean.Sphere.SecondInter Mathlib.Topology.Category.CompHausLike.Basic Mathlib.Geometry.Euclidean.Basic Mathlib.Data.Nat.Cast.SetInterval Mathlib.Computability.Partrec Mathlib.Algebra.Lie.Matrix Mathlib.MeasureTheory.Covering.DensityTheorem Mathlib.Algebra.MvPolynomial.Supported Mathlib.MeasureTheory.Integral.LebesgueNormedSpace Mathlib.Probability.ProbabilityMassFunction.Binomial Mathlib.Data.PNat.Prime Mathlib.RingTheory.MvPolynomial.Tower Mathlib.Geometry.RingedSpace.Basic Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.Order.Extension.Well Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.Data.Matrix.Rank Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas Mathlib.NumberTheory.Liouville.Measure Mathlib.LinearAlgebra.Pi Mathlib.Combinatorics.SimpleGraph.Girth Mathlib.GroupTheory.Torsion Mathlib.Topology.Algebra.InfiniteSum.Ring Mathlib.LinearAlgebra.Dimension.Basic 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.Combinatorics.SimpleGraph.Metric Mathlib.Topology.Order.LeftRightLim Mathlib.CategoryTheory.Sites.LeftExact Mathlib.Algebra.DirectSum.Finsupp Mathlib.Geometry.Manifold.VectorBundle.Hom Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Analysis.InnerProductSpace.Orthogonal Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Data.Fintype.Units Mathlib.Algebra.Ring.CentroidHom Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology Mathlib.LinearAlgebra.LinearIndependent Mathlib.Geometry.Euclidean.MongePoint Mathlib.Analysis.NormedSpace.Star.Multiplier Mathlib.LinearAlgebra.AffineSpace.Restrict Mathlib.Analysis.Convex.Between Mathlib.GroupTheory.FixedPointFree Mathlib.LinearAlgebra.AffineSpace.Independent Mathlib.Analysis.LocallyConvex.Polar Mathlib.Analysis.NormedSpace.WithLp Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional Mathlib.MeasureTheory.Group.Pointwise Mathlib.Tactic.Ring.RingNF Mathlib.Algebra.AlgebraicCard Mathlib.Algebra.Order.Field.Canonical.Defs Mathlib.Analysis.Calculus.ContDiff.Bounds Mathlib.Topology.Compactness.PseudometrizableLindelof Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.Data.Complex.BigOperators Mathlib.Analysis.Normed.Group.HomCompletion Mathlib.Data.Real.Irrational Mathlib.NumberTheory.Ostrowski Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic Mathlib.Data.Num.Prime Mathlib.Topology.Category.CompHaus.Limits Mathlib.CategoryTheory.Galois.Basic Mathlib.Topology.Algebra.Module.LocallyConvex Mathlib.Algebra.Tropical.BigOperators Mathlib.CategoryTheory.Idempotents.SimplicialObject Mathlib.CategoryTheory.Linear.Basic Mathlib.Order.Filter.AtTopBot Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.Algebra.Polynomial.Induction Mathlib.LinearAlgebra.Contraction Mathlib.MeasureTheory.Measure.Doubling Mathlib.SetTheory.Cardinal.Continuum Mathlib.Algebra.Algebra.Spectrum Mathlib.Topology.Order.MonotoneConvergence Mathlib.Analysis.MeanInequalities Mathlib.Data.Nat.Multiplicity Mathlib.MeasureTheory.Tactic Mathlib.LinearAlgebra.Matrix.BilinearForm Mathlib.Tactic.Linarith.Oracle.FourierMotzkin Mathlib.FieldTheory.PrimitiveElement Mathlib.Data.Rat.Star Mathlib.Algebra.Star.CHSH Mathlib.Probability.Distributions.Poisson Mathlib.RingTheory.Binomial Mathlib.Geometry.Euclidean.Sphere.Basic Mathlib.Algebra.Module.Submodule.RestrictScalars Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.SetTheory.Lists 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.Geometry.Manifold.ConformalGroupoid Mathlib.RingTheory.Smooth.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Even Mathlib.Algebra.Polynomial.Laurent Mathlib.Algebra.Category.ModuleCat.Tannaka Mathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.LinearAlgebra.Multilinear.FiniteDimensional Mathlib.Algebra.Module.Submodule.Localization Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.ModelTheory.Quotients Mathlib.Topology.Algebra.MvPolynomial Mathlib.Algebra.Homology.HomotopyCategory.Shift Mathlib.Algebra.Polynomial.Module.Basic Mathlib.Algebra.Star.Rat Mathlib.Algebra.Ring.BooleanRing Mathlib.Analysis.Normed.MulAction Mathlib.Topology.Order.LeftRight Mathlib.Algebra.Homology.ShortComplex.Linear Mathlib.CategoryTheory.Shift.Opposite Mathlib.Algebra.Module.Zlattice.Basic Mathlib.Analysis.InnerProductSpace.Projection Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.SetTheory.Game.Impartial Mathlib.Algebra.Order.Ring.Nat Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.Analysis.NormedSpace.MStructure Mathlib.Analysis.NormedSpace.Star.Exponential Mathlib.Computability.TMComputable Mathlib.Algebra.Lie.Semisimple.Defs Mathlib.Analysis.BoxIntegral.Partition.Tagged Mathlib.Data.NNRat.Lemmas Mathlib.Algebra.Polynomial.Degree.CardPowDegree Mathlib.Topology.Algebra.ProperConstSMul Mathlib.Data.ZMod.Basic Mathlib.Data.Nat.Count Mathlib.Algebra.Category.ModuleCat.FilteredColimits 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.Topology.Bornology.Basic Mathlib.Analysis.NormedSpace.Completion Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike Mathlib.Tactic.NormNum.LegendreSymbol Mathlib.Analysis.Convex.Independent Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal Mathlib.Combinatorics.SimpleGraph.Trails Mathlib.RingTheory.ChainOfDivisors Mathlib.Analysis.Calculus.Deriv.Prod Mathlib.Analysis.Convex.Strong Mathlib.Analysis.Calculus.ContDiff.Basic Mathlib.Analysis.Calculus.AffineMap Mathlib.Algebra.Order.Positive.Field Mathlib.Order.Interval.Set.IsoIoo Mathlib.Topology.Algebra.ConstMulAction Mathlib.adomaniLeanUtils.all_tactics Mathlib.Data.Matrix.ColumnRowPartitioned Mathlib.LinearAlgebra.Projectivization.Independence Mathlib.Analysis.Complex.Asymptotics Mathlib.Data.Int.LeastGreatest Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Probability.ConditionalProbability Mathlib.Topology.Bornology.Constructions Mathlib.Algebra.Category.ModuleCat.Colimits Mathlib.Topology.NoetherianSpace 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.Combinatorics.SimpleGraph.Turan Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Algebra.Category.BialgebraCat.Basic Mathlib.Topology.Category.Born Mathlib.Algebra.Polynomial.Derivative Mathlib.Topology.Algebra.Field Mathlib.Logic.Equiv.TransferInstance Mathlib.Data.Complex.FiniteDimensional Mathlib.Topology.ContinuousFunction.Units Mathlib.Combinatorics.SetFamily.Shadow Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective Mathlib.Topology.Algebra.UniformRing Mathlib.RingTheory.OrzechProperty Mathlib.LinearAlgebra.Matrix.Trace Mathlib.Topology.MetricSpace.Pseudo.Lemmas Mathlib.Analysis.BoxIntegral.Basic Mathlib.Algebra.Star.Order Mathlib.SetTheory.Game.State Mathlib.GroupTheory.Perm.Cycle.Concrete Mathlib.RingTheory.Polynomial.Basic Mathlib.MeasureTheory.Measure.AddContent Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes Mathlib.Analysis.Quaternion Mathlib.Combinatorics.SimpleGraph.Partition 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.Algebra.Order.Ring.Cast Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.RingTheory.HopfAlgebra Mathlib.Data.DFinsupp.Encodable 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.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Analysis.Normed.Group.Bounded Mathlib.Data.ZMod.Parity Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.Topology.Category.TopCat.Opens Mathlib.MeasureTheory.Integral.RieszMarkovKakutani Mathlib.GroupTheory.Commensurable Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex Mathlib.Analysis.BoxIntegral.Integrability Mathlib.Analysis.NormedSpace.Star.Matrix Mathlib.Algebra.Star.RingQuot Mathlib.Data.Matroid.Constructions Mathlib.CategoryTheory.CofilteredSystem Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.RingTheory.Discriminant Mathlib.Data.Int.Star Mathlib.Analysis.Calculus.FDeriv.RestrictScalars Mathlib.Algebra.Order.Group.Int Mathlib.NumberTheory.SumTwoSquares Mathlib.GroupTheory.Complement Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Analysis.SpecialFunctions.Exponential Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup Mathlib.LinearAlgebra.Basis Mathlib.Algebra.Homology.Refinements Mathlib.Algebra.Group.Submonoid.Units Mathlib.Algebra.DirectLimit Mathlib.MeasureTheory.Measure.VectorMeasure Mathlib.RingTheory.ReesAlgebra Mathlib.Analysis.Analytic.Meromorphic Mathlib.RingTheory.IsTensorProduct Mathlib.Algebra.Module.PID Mathlib.Algebra.Group.Subgroup.Order Mathlib.RepresentationTheory.Action.Monoidal Mathlib.Algebra.MvPolynomial.Comap Mathlib.RingTheory.Ideal.AssociatedPrime Mathlib.RingTheory.Polynomial.GaussLemma Mathlib.Analysis.Convex.KreinMilman Mathlib.Algebra.Order.Group.Prod Mathlib.LinearAlgebra.CliffordAlgebra.Inversion Mathlib.Topology.Covering Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.Algebra.Category.AlgebraCat.Symmetric Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.Analysis.NormedSpace.Extr Mathlib.FieldTheory.Finiteness Mathlib.NumberTheory.ClassNumber.Finite Mathlib.Topology.UniformSpace.UniformEmbedding Mathlib.Topology.MetricSpace.GromovHausdorff Mathlib.Analysis.NormedSpace.lpSpace Mathlib.Topology.UnitInterval Mathlib.Combinatorics.Schnirelmann Mathlib.Topology.UrysohnsLemma Mathlib.RepresentationTheory.Action.Limits Mathlib.NumberTheory.Harmonic.Int Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.CategoryTheory.Sites.Spaces Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.Algebra.Pointwise.Stabilizer Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries Mathlib.Analysis.Calculus.IteratedDeriv.Defs Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.RingTheory.WittVector.StructurePolynomial Mathlib.MeasureTheory.Constructions.BorelSpace.Complex Mathlib.Algebra.Algebra.RestrictScalars Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic Mathlib.NumberTheory.MaricaSchoenheim Mathlib.Analysis.Complex.Tietze Mathlib.Topology.UniformSpace.Completion Mathlib.Topology.Category.TopCat.Limits.Konig Mathlib.Topology.Homotopy.HomotopyGroup Mathlib.adomaniLeanUtils.to_left_right Mathlib.Data.Real.StarOrdered Mathlib.CategoryTheory.Sites.Coherent.Equivalence Mathlib.Analysis.Normed.Order.Basic Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.Data.PNat.Xgcd Mathlib.Algebra.CharP.ExpChar Mathlib.Topology.Metrizable.Basic Mathlib.Analysis.NormedSpace.ContinuousLinearMap 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.ModelTheory.Syntax Mathlib.Data.Finset.NatDivisors Mathlib.Topology.Algebra.UniformFilterBasis Mathlib.Algebra.BigOperators.Associated Mathlib.Analysis.Convex.Normed Mathlib.Topology.Algebra.Nonarchimedean.Bases Mathlib.Probability.Kernel.Basic Mathlib.GroupTheory.Index Mathlib.Algebra.Order.Group.WithTop Mathlib.MeasureTheory.Measure.Tilted Mathlib.Analysis.Calculus.Deriv.Inverse Mathlib.Analysis.Complex.Liouville Mathlib.GroupTheory.Perm.Finite Mathlib.Algebra.Category.ModuleCat.Basic Mathlib.Topology.Algebra.UniformGroup Mathlib.Computability.TMToPartrec Mathlib.Topology.FiberBundle.Trivialization Mathlib.Data.Nat.Digits Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber Mathlib.Algebra.Order.Ring.Canonical Mathlib.Tactic.NormNum.Inv Mathlib.GroupTheory.SpecificGroups.Quaternion Mathlib.Algebra.Order.Group.Abs Mathlib.Topology.Algebra.OpenSubgroup Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.Topology.Algebra.Module.StrongTopology Mathlib.MeasureTheory.Constructions.Prod.Basic Mathlib.Topology.Sheaves.Limits Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Instances Mathlib.Analysis.Convex.EGauge Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.LinearAlgebra.Ray Mathlib.Topology.ContinuousFunction.Sigma Mathlib.CategoryTheory.Localization.Triangulated Mathlib.Analysis.Normed.Group.Int Mathlib.Analysis.Convex.Mul Mathlib.Data.FP.Basic Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.Topology.Algebra.Module.LinearPMap Mathlib.Topology.MetricSpace.ThickenedIndicator Mathlib.CategoryTheory.Galois.Prorepresentability Mathlib.Algebra.Order.Ring.Int Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.Algebra.Order.Group.Bounds Mathlib.Algebra.Module.Submodule.IterateMapComap Mathlib.Topology.Algebra.Group.Compact Mathlib.Topology.StoneCech Mathlib.CategoryTheory.Triangulated.Opposite Mathlib.Data.Nat.Factors Mathlib.Topology.Algebra.Polynomial Mathlib.Algebra.Homology.ComplexShapeSigns Mathlib.Analysis.Convex.Segment Mathlib.Data.ZMod.Units Mathlib.Data.PNat.Basic 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.CategoryTheory.Limits.SmallComplete 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.Topology.Baire.Lemmas Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.Analysis.Convex.Measure Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.Probability.Moments Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.Topology.Algebra.Nonarchimedean.Basic Mathlib.Algebra.Group.Submonoid.Pointwise Mathlib.Mathport.Syntax Mathlib.Algebra.Homology.ShortComplex.Preadditive Mathlib.Algebra.Homology.BifunctorHomotopy Mathlib.Algebra.Order.Invertible Mathlib.Analysis.Analytic.Linear Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Analysis.SpecialFunctions.Log.Deriv Mathlib.LinearAlgebra.Eigenspace.Basic Mathlib.Algebra.Order.UpperLower Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.FieldTheory.Cardinality Mathlib.Algebra.Homology.ShortComplex.Exact Mathlib.Algebra.Lie.EngelSubalgebra Mathlib.RingTheory.IntegralRestrict Mathlib.NumberTheory.Cyclotomic.PID Mathlib.Analysis.NormedSpace.Int Mathlib.Algebra.Algebra.Subalgebra.MulOpposite Mathlib.Topology.Algebra.Group.TopologicalAbelianization Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Tactic.Group Mathlib.Analysis.RCLike.Basic Mathlib.LinearAlgebra.TensorProduct.Tower Mathlib.Topology.Specialization Mathlib.Topology.Connected.Basic Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Algebra.Module.CharacterModule Mathlib.AlgebraicGeometry.EllipticCurve.Projective Mathlib.Topology.Algebra.Algebra Mathlib.Analysis.Calculus.LineDeriv.Basic 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.ModelTheory.Semantics Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.Analysis.Normed.Group.AddCircle Mathlib.Topology.Instances.Matrix Mathlib.Topology.Irreducible Mathlib.Topology.Instances.Complex Mathlib.MeasureTheory.MeasurableSpace.Basic Mathlib.Logic.Small.Group Mathlib.Algebra.Order.Ring.Abs Mathlib.Algebra.Jordan.Basic Mathlib.adomaniLeanUtils.mwe_revcharpoly Mathlib.Algebra.Polynomial.GroupRingAction Mathlib.SetTheory.Cardinal.Subfield Mathlib.Topology.Order.UpperLowerSetTopology Mathlib.Analysis.Convex.Contractible Mathlib.Data.Finsupp.WellFounded Mathlib.RingTheory.EuclideanDomain Mathlib.AlgebraicGeometry.AffineScheme Mathlib.SetTheory.Game.Domineering Mathlib.Algebra.Category.ModuleCat.Algebra Mathlib.Data.Nat.Prime.Basic Mathlib.MeasureTheory.Group.Convolution Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.RingTheory.RootsOfUnity.Complex Mathlib.CategoryTheory.Sites.Equivalence Mathlib.MeasureTheory.MeasurableSpace.Card Mathlib.NumberTheory.Liouville.Basic Mathlib.NumberTheory.Padics.RingHoms Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics Mathlib.MeasureTheory.Constructions.Polish Mathlib.Topology.UniformSpace.UniformConvergence Mathlib.Order.SuccPred.LinearLocallyFinite Mathlib.LinearAlgebra.CliffordAlgebra.Grading Mathlib.Data.Real.Pi.Bounds Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves Mathlib.Data.Nat.Factorization.Root Mathlib.RingTheory.OreLocalization.Ring Mathlib.MeasureTheory.Decomposition.Lebesgue Mathlib.Analysis.NormedSpace.QuaternionExponential Mathlib.Data.Num.Lemmas Mathlib.Data.ZMod.Factorial Mathlib.Algebra.Module.Submodule.Lattice Mathlib.Topology.Algebra.Constructions Mathlib.Topology.UniformSpace.Cauchy Mathlib.Analysis.BoxIntegral.Partition.Filter Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic Mathlib.RingTheory.Valuation.Integers Mathlib.Algebra.Group.PNatPowAssoc Mathlib.Topology.MetricSpace.Perfect Mathlib.RingTheory.Polynomial.SeparableDegree Mathlib.Computability.DFA Mathlib.Topology.MetricSpace.CauSeqFilter Mathlib.Algebra.Category.Grp.Images Mathlib.Order.Height Mathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.GroupTheory.Perm.ClosureSwap Mathlib.Algebra.Category.Grp.ZModuleEquivalence Mathlib.Tactic.NormNum.Eq Mathlib.FieldTheory.Separable Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.Algebra.Module.Submodule.Equiv Mathlib.LinearAlgebra.TensorProduct.Opposite Mathlib.Algebra.Homology.SingleHomology Mathlib.AlgebraicTopology.SimplexCategory Mathlib.Topology.Connected.PathConnected Mathlib.Topology.Order.DenselyOrdered Mathlib.RingTheory.HahnSeries.Summable Mathlib.ModelTheory.Algebra.Field.Basic Mathlib.Dynamics.Ergodic.Ergodic Mathlib.Data.Finite.Card Mathlib.Algebra.Algebra.Quasispectrum Mathlib.Algebra.Module.FinitePresentation Mathlib.NumberTheory.KummerDedekind Mathlib.AlgebraicGeometry.Limits Mathlib.Topology.UniformSpace.Separation Mathlib.Topology.Compactness.Lindelof Mathlib.RingTheory.EisensteinCriterion Mathlib.Algebra.Star.Free Mathlib.Algebra.Order.Hom.Monoid Mathlib.RingTheory.Int.Basic Mathlib.Geometry.Manifold.MFDeriv.Defs Mathlib.SetTheory.Ordinal.CantorNormalForm Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.Analysis.NormedSpace.ENorm Mathlib.RepresentationTheory.FdRep Mathlib.CategoryTheory.Abelian.Homology Mathlib.Algebra.Order.Hom.Ring Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional Mathlib.Algebra.Polynomial.BigOperators Mathlib.Topology.Algebra.Affine Mathlib.MeasureTheory.Measure.OpenPos Mathlib.Logic.Small.Module Mathlib.Topology.Algebra.PontryaginDual Mathlib.MeasureTheory.Function.LocallyIntegrable Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence Mathlib.Analysis.Analytic.Constructions Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra Mathlib.RingTheory.Localization.Basic Mathlib.Topology.MetricSpace.Holder Mathlib.Algebra.MvPolynomial.Monad Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Order Mathlib.Combinatorics.Colex Mathlib.MeasureTheory.Measure.Dirac Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization Mathlib.adomaniLeanUtils.Rev Mathlib.Algebra.Category.Ring.Limits Mathlib.RingTheory.Ideal.Operations Mathlib.LinearAlgebra.CliffordAlgebra.Basic Mathlib.FieldTheory.IsAlgClosed.Spectrum 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.ModelTheory.Order Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.Algebra.Order.Ring.InjSurj Mathlib.LinearAlgebra.Alternating.Basic Mathlib.RingTheory.WittVector.Frobenius Mathlib.Algebra.Order.Module.OrderedSMul Mathlib.Topology.ProperMap Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology 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.Topology.Category.TopCat.Adjunctions Mathlib.Analysis.NormedSpace.DualNumber Mathlib.Data.Rat.Cast.Lemmas Mathlib.Topology.SeparatedMap Mathlib.Topology.Maps Mathlib.CategoryTheory.Monoidal.Subcategory Mathlib.Algebra.CharP.Pi Mathlib.Dynamics.Minimal Mathlib.NumberTheory.Pell Mathlib.Combinatorics.SimpleGraph.Operations Mathlib.Analysis.Calculus.Deriv.Comp Mathlib.Probability.Process.Stopping Mathlib.Algebra.Category.AlgebraCat.Monoidal Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.CategoryTheory.Triangulated.TriangleShift Mathlib.Algebra.Ring.Subsemiring.Order Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.NumberTheory.NumberField.Basic Mathlib.Topology.Algebra.Ring.Ideal Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.Combinatorics.SimpleGraph.Hamiltonian Mathlib.MeasureTheory.Function.SpecialFunctions.Inner Mathlib.Geometry.RingedSpace.Stalks Mathlib.Computability.Encoding Mathlib.Topology.Order.LeftRightNhds Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps Mathlib.NumberTheory.Modular Mathlib.RingTheory.WittVector.Basic Mathlib.Algebra.Homology.TotalComplex Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Restrict 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.Analysis.NormedSpace.Banach Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.Combinatorics.Hindman 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.Algebra.Star.SelfAdjoint Mathlib.Geometry.Manifold.ContMDiff.Defs Mathlib.Data.Multiset.Interval Mathlib.LinearAlgebra.TensorProduct.DirectLimit Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.Algebra.Order.Archimedean Mathlib.Algebra.Order.Antidiag.Finsupp Mathlib.Probability.Kernel.Disintegration.CondCdf 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.Tactic.Linarith.Parsing 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.Analysis.NormedSpace.Span Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed Mathlib.Topology.ContinuousFunction.Compact Mathlib.GroupTheory.Finiteness Mathlib.Analysis.Analytic.Composition Mathlib.FieldTheory.RatFunc.Defs Mathlib.Topology.MetricSpace.Basic Mathlib.Topology.VectorBundle.Basic Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn Mathlib.CategoryTheory.Preadditive.ProjectiveResolution Mathlib.Topology.Sheaves.PresheafOfFunctions Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic Mathlib.Analysis.Calculus.FDeriv.Mul Mathlib.RingTheory.Bezout Mathlib.Analysis.ConstantSpeed Mathlib.Topology.Category.Stonean.Basic 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.Data.ZMod.Defs Mathlib.Algebra.Order.Group.Cone Mathlib.Algebra.Order.Field.Rat 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.LinearAlgebra.Reflection Mathlib.Topology.MetricSpace.HausdorffDistance Mathlib.LinearAlgebra.AnnihilatingPolynomial Mathlib.Algebra.DirectSum.Ring 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.CategoryTheory.EffectiveEpi.Extensive Mathlib.Algebra.Ring.Subsemiring.Pointwise Mathlib.Algebra.Homology.HomologicalComplexAbelian Mathlib.Algebra.Algebra.Prod Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.Algebra.Order.Group.Defs Mathlib.Topology.EMetricSpace.Lipschitz Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.Data.ENNReal.Real Mathlib.Combinatorics.SetFamily.CauchyDavenport Mathlib.NumberTheory.FermatPsp Mathlib.RingTheory.Kaehler.Basic Mathlib.SetTheory.Cardinal.PartENat Mathlib.GroupTheory.Sylow Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.SetTheory.Cardinal.ENat Mathlib.Algebra.Category.MonCat.FilteredColimits Mathlib.Probability.Kernel.MeasureCompProd Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField Mathlib.Order.Filter.Archimedean Mathlib.Tactic.ModCases Mathlib.Topology.Order.OrderClosed Mathlib.Analysis.NormedSpace.Extend Mathlib.Topology.Category.TopCat.Limits.Products Mathlib.AlgebraicTopology.SplitSimplicialObject Mathlib.NumberTheory.VonMangoldt Mathlib.NumberTheory.ZetaValues Mathlib.Topology.Algebra.Order.LiminfLimsup Mathlib.Analysis.Asymptotics.Theta Mathlib.Combinatorics.SimpleGraph.DegreeSum Mathlib.Combinatorics.SimpleGraph.ConcreteColorings Mathlib.Topology.Sets.Compacts Mathlib.Analysis.Convex.Deriv Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.RingTheory.LocalProperties Mathlib.Topology.MetricSpace.Gluing Mathlib.Probability.Independence.Basic Mathlib.MeasureTheory.Function.Egorov Mathlib.Topology.Category.LightProfinite.Basic Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction 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.Algebra.Order.Field.Defs Mathlib.Algebra.Module.Submodule.EqLocus Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves Mathlib.Algebra.Order.Module.Pointwise Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.Topology.Connected.TotallyDisconnected Mathlib.Deprecated.Subring Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.Analysis.BoxIntegral.Partition.Basic Mathlib.Analysis.Fourier.FourierTransform Mathlib.LinearAlgebra.Matrix.Symmetric Mathlib.RingTheory.MatrixAlgebra Mathlib.LinearAlgebra.Dimension.LinearMap Mathlib.Topology.MetricSpace.CantorScheme Mathlib.Algebra.Lie.Derivation.Basic Mathlib.Analysis.Convex.Cone.Basic Mathlib.Combinatorics.Additive.Corner.Defs 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.Computability.Primrec 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.CategoryTheory.Abelian.Exact Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup Mathlib.RepresentationTheory.Action.Continuous Mathlib.RingTheory.GradedAlgebra.Basic Mathlib.Analysis.SpecialFunctions.Pow.Real Mathlib.Dynamics.Flow Mathlib.Topology.Constructions Mathlib.RingTheory.Valuation.ValuationSubring Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion Mathlib.Tactic.Rify Mathlib.Algebra.CharP.Quotient Mathlib.Topology.Bornology.Hom Mathlib.Algebra.MvPolynomial.Cardinal Mathlib.Algebra.MvPolynomial.Division Mathlib.Probability.IdentDistrib Mathlib.RingTheory.Complex Mathlib.Analysis.Convolution Mathlib.Combinatorics.SetFamily.HarrisKleitman Mathlib.AlgebraicGeometry.Scheme Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm Mathlib.MeasureTheory.Covering.Vitali Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle Mathlib.Data.UInt Mathlib.Topology.EMetricSpace.Paracompact Mathlib.Analysis.NormedSpace.ProdLp Mathlib.LinearAlgebra.Matrix.Adjugate Mathlib.Data.Complex.Module Mathlib.Algebra.Order.BigOperators.Group.Finset 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.Algebra.Group.Submonoid.Membership Mathlib.NumberTheory.LucasPrimality Mathlib.Algebra.Homology.QuasiIso Mathlib.Analysis.Analytic.Basic Mathlib.Algebra.BigOperators.Finprod Mathlib.ModelTheory.Bundled Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.Order.Filter.Ring Mathlib.Analysis.Analytic.Uniqueness Mathlib.Condensed.Light.Basic Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.LinearAlgebra.BilinearForm.Basic Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle Mathlib.AlgebraicGeometry.Gluing Mathlib.LinearAlgebra.AffineSpace.Combination Mathlib.Topology.Sheaves.Functors Mathlib.GroupTheory.GroupAction.Quotient Mathlib.LinearAlgebra.QuadraticForm.Isometry Mathlib.Combinatorics.SetFamily.LYM Mathlib.Tactic.Linarith.Datatypes Mathlib.Analysis.Convex.Jensen Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence Mathlib.adomaniLeanUtils.LFTCM_Duesseldorf_2023.S11_Algebraic_Geometry Mathlib.Topology.Instances.Irrational Mathlib.Topology.Algebra.Module.Basic Mathlib.Topology.ContinuousFunction.T0Sierpinski Mathlib.Order.RelSeries Mathlib.ModelTheory.Algebra.Ring.FreeCommRing Mathlib.CategoryTheory.Preadditive.Opposite Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition Mathlib.Analysis.Complex.Arg Mathlib.Analysis.Calculus.Deriv.Support Mathlib.Tactic.FieldSimp Mathlib.Geometry.Manifold.Algebra.Monoid Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv Mathlib.Data.DFinsupp.Notation Mathlib.FieldTheory.Minpoly.Field Mathlib.LinearAlgebra.UnitaryGroup Mathlib.Algebra.AddConstMap.Basic Mathlib.Computability.EpsilonNFA Mathlib.Topology.Algebra.Module.Determinant Mathlib.Computability.Reduce 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.Topology.ContinuousFunction.UniqueCFC Mathlib.Geometry.Manifold.Algebra.Structures Mathlib.Topology.Sheaves.Operations Mathlib.Data.Real.EReal Mathlib.adomaniLeanUtils.LFTCM_Duesseldorf_2023.help Mathlib.Condensed.Light.Module Mathlib.Data.Real.Cardinality Mathlib.Analysis.NormedSpace.LpEquiv Mathlib.RingTheory.AdicCompletion.Algebra Mathlib.GroupTheory.PushoutI Mathlib.ModelTheory.Types Mathlib.Analysis.Convex.Strict Mathlib.RingTheory.Valuation.Quotient Mathlib.Topology.Compactness.SigmaCompact Mathlib.Algebra.Category.Ring.Constructions Mathlib.RingTheory.Polynomial.Eisenstein.Basic Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Data.Finset.Pointwise.Interval Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.LinearAlgebra.Dimension.Free Mathlib.Order.Filter.Cocardinal Mathlib.Dynamics.Ergodic.Function Mathlib.Tactic.CancelDenoms.Core Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian Mathlib.Algebra.CharP.Reduced Mathlib.Algebra.Lie.BaseChange Mathlib.Data.Nat.PartENat Mathlib.Algebra.CharZero.Quotient Mathlib.Analysis.SpecialFunctions.Log.ENNReal Mathlib.Algebra.Algebra.Subalgebra.Unitization Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating Mathlib.LinearAlgebra.Isomorphisms Mathlib.Analysis.Complex.Convex Mathlib.Topology.Separation.NotNormal Mathlib.Topology.DiscreteQuotient Mathlib.Topology.Category.Locale Mathlib.NumberTheory.PrimeCounting Mathlib.Topology.UniformSpace.Pi Mathlib.Data.NNRat.Defs Mathlib.LinearAlgebra.Dual Mathlib.LinearAlgebra.TensorProduct.RightExactness Mathlib.Algebra.Group.Subgroup.Pointwise Mathlib.Algebra.Category.Grp.Limits Mathlib.Analysis.Complex.UpperHalfPlane.Basic Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv Mathlib.Algebra.Lie.CartanMatrix Mathlib.Geometry.Manifold.MFDeriv.Atlas Mathlib.Topology.Compactness.Compact Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm 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.Analysis.NormedSpace.PiLp Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.Combinatorics.SimpleGraph.Hasse Mathlib.Topology.Sets.Opens Mathlib.Algebra.Polynomial.Lifts Mathlib.RingTheory.Finiteness Mathlib.MeasureTheory.Covering.Differentiation Mathlib.NumberTheory.Padics.Hensel Mathlib.Data.Nat.Choose.Multinomial Mathlib.GroupTheory.HNNExtension Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.Testing.SlimCheck.Testable Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.CategoryTheory.Galois.Examples Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.RingTheory.Polynomial.ScaleRoots Mathlib.GroupTheory.SpecificGroups.Alternating Mathlib.Topology.Category.CompHausLike.Limits Mathlib.RingTheory.FractionalIdeal.Operations Mathlib.Data.Nat.ChineseRemainder Mathlib.Analysis.Calculus.FDeriv.Comp Mathlib.Topology.Instances.RealVectorSpace Mathlib.LinearAlgebra.QuadraticForm.TensorProduct Mathlib.Analysis.LocallyConvex.ContinuousOfBounded Mathlib.Analysis.Convex.Hull Mathlib.Data.Rat.Cast.CharZero Mathlib.Algebra.Homology.Linear Mathlib.RingTheory.Fintype Mathlib.Analysis.Complex.Hadamard Mathlib.RingTheory.Etale.Basic Mathlib.Topology.Algebra.Valuation Mathlib.Algebra.MonoidAlgebra.Division Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.Convex.Star Mathlib.Geometry.Manifold.Algebra.LieGroup Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm Mathlib.Tactic.Positivity.Basic Mathlib.Algebra.Lie.UniversalEnveloping Mathlib.Topology.Algebra.Order.Group Mathlib.Topology.Order.Category.AlexDisc 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.Analysis.Analytic.CPolynomial Mathlib.RingTheory.Ideal.Norm Mathlib.Analysis.BoundedVariation Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Topology.Algebra.InfiniteSum.Defs Mathlib.Combinatorics.SimpleGraph.Regularity.Bound Mathlib.Algebra.Homology.HomotopyCategory.ShortExact Mathlib.CategoryTheory.Triangulated.Subcategory Mathlib.RingTheory.Ideal.Pointwise Mathlib.RingTheory.Ideal.Colon Mathlib.Algebra.Order.Group.PiLex 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.Data.Fintype.Perm Mathlib.Analysis.LocallyConvex.WithSeminorms Mathlib.MeasureTheory.Measure.Lebesgue.Basic Mathlib.Tactic.Ring Mathlib.Analysis.Convex.Basic Mathlib.Analysis.Asymptotics.SuperpolynomialDecay Mathlib.RingTheory.Coprime.Basic Mathlib.Combinatorics.Pigeonhole Mathlib.Topology.LocallyConstant.Algebra Mathlib.LinearAlgebra.CliffordAlgebra.Contraction Mathlib.NumberTheory.LSeries.Convergence Mathlib.Analysis.NormedSpace.AddTorsorBases Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.ContinuousFunction.NonUnitalFunctionalCalculus Mathlib.CategoryTheory.Abelian.InjectiveResolution Mathlib.Condensed.Light.Discrete Mathlib.adomaniLeanUtils.posets Mathlib.InformationTheory.Hamming Mathlib.Analysis.Calculus.LocalExtr.Basic Mathlib.Algebra.CharP.Algebra Mathlib.CategoryTheory.Triangulated.TStructure.Basic Mathlib.RingTheory.Localization.Module Mathlib.Algebra.Lie.Subalgebra Mathlib.Probability.Process.Adapted Mathlib.Analysis.Convex.Cone.Proper Mathlib.RingTheory.MvPolynomial.Basic Mathlib.Analysis.Normed.Order.Lattice Mathlib.Topology.GDelta Mathlib.Algebra.Polynomial.Monomial Mathlib.ModelTheory.Basic Mathlib.Algebra.MvPolynomial.PDeriv Mathlib.Topology.ContinuousFunction.Bounded Mathlib.Data.Sign Mathlib.Data.Finsupp.Interval Mathlib.Tactic.Monotonicity.Lemmas Mathlib.NumberTheory.DirichletCharacter.Bounds Mathlib.Algebra.Lie.Sl2 Mathlib.Topology.Algebra.Module.WeakDual Mathlib.adomaniLeanUtils.importTryThis 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.Data.Matrix.RowCol Mathlib.RingTheory.FreeCommRing Mathlib.Tactic.NormNum.IsCoprime Mathlib.RingTheory.PowerSeries.Order Mathlib.FieldTheory.PurelyInseparable Mathlib.Data.ENat.Lattice Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv Mathlib.Dynamics.FixedPoints.Topology Mathlib.Algebra.Category.Grp.Biproducts 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.CategoryTheory.Preadditive.HomOrthogonal Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Convex.Extrema Mathlib.Algebra.Homology.Embedding.Restriction Mathlib.Algebra.Homology.ExactSequence Mathlib.Analysis.NormedSpace.MazurUlam Mathlib.Analysis.Convex.Extreme Mathlib.Probability.Independence.Kernel Mathlib.Analysis.Calculus.FDeriv.Equiv Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.RingTheory.WittVector.IsPoly Mathlib.MeasureTheory.Group.Prod Mathlib.Algebra.Ring.Subsemiring.Basic Mathlib.LinearAlgebra.Dimension.Constructions Mathlib.Order.Category.Frm Mathlib.Topology.Algebra.Localization Mathlib.MeasureTheory.Integral.Pi Mathlib.Algebra.Algebra.Bilinear Mathlib.Algebra.Order.BigOperators.Group.Multiset Mathlib.Data.Real.Basic Mathlib.SetTheory.Ordinal.FixedPoint Mathlib.Combinatorics.SimpleGraph.Prod Mathlib.Data.Nat.Prime.Defs Mathlib.Algebra.Category.Grp.Colimits Mathlib.Analysis.NormedSpace.OperatorNorm.Prod Mathlib.Data.Matrix.DualNumber Mathlib.Data.Matroid.Restrict Mathlib.Combinatorics.SimpleGraph.Subgraph Mathlib.Data.Real.Star Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.Algebra.Lie.Solvable Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.GroupTheory.SpecificGroups.Cyclic Mathlib.NumberTheory.NumberField.Embeddings Mathlib.Topology.Order.T5 Mathlib.CategoryTheory.Abelian.LeftDerived Mathlib.GroupTheory.Coxeter.Length Mathlib.Algebra.Lie.Weights.Cartan Mathlib.MeasureTheory.Measure.Typeclasses Mathlib.Probability.Process.Filtration Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.MeasureTheory.Integral.Periodic Mathlib.Algebra.Homology.Homotopy Mathlib.LinearAlgebra.TensorPower Mathlib.RingTheory.MvPolynomial.NewtonIdentities Mathlib.CategoryTheory.Linear.LinearFunctor Mathlib.Algebra.QuaternionBasis Mathlib.NumberTheory.Harmonic.Bounds Mathlib.NumberTheory.Basic Mathlib.adomaniLeanUtils.move_add_utils Mathlib.NumberTheory.Bernoulli Mathlib.Algebra.Polynomial.UnitTrinomial Mathlib.Data.Finset.Pointwise Mathlib.Algebra.Order.Ring.Prod Mathlib.Algebra.Order.Ring.Pow Mathlib.LinearAlgebra.SymplecticGroup Mathlib.Geometry.Manifold.AnalyticManifold Mathlib.Data.Finsupp.ToDFinsupp Mathlib.Analysis.MellinTransform Mathlib.Topology.Order.Priestley Mathlib.Algebra.Field.Subfield Mathlib.LinearAlgebra.Determinant Mathlib.LinearAlgebra.Matrix.Transvection Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating Mathlib.Analysis.Convex.StrictConvexBetween Mathlib.CategoryTheory.Extensive Mathlib.NumberTheory.LSeries.Linearity Mathlib.Analysis.NormedSpace.Real Mathlib.Testing.SlimCheck.Sampleable Mathlib.Algebra.Algebra.Equiv 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.Data.DFinsupp.Lex Mathlib.Topology.Perfect Mathlib.LinearAlgebra.Dimension.StrongRankCondition Mathlib.Data.Nat.Choose.Bounds Mathlib.Analysis.Convex.SpecificFunctions.Deriv Mathlib.Data.Matrix.Hadamard Mathlib.Analysis.Normed.Group.Submodule Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.Condensed.Discrete Mathlib.ModelTheory.DirectLimit Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.Algebra.Lie.Engel Mathlib.Analysis.Calculus.FDeriv.Symmetric Mathlib.Data.Nat.Fib.Zeckendorf Mathlib.Topology.Sheaves.PUnit Mathlib.RingTheory.WittVector.Defs Mathlib.Algebra.Category.ModuleCat.Free Mathlib.Analysis.Normed.Field.InfiniteSum Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear Mathlib.Algebra.Polynomial.Basic Mathlib.Algebra.Algebra.Subalgebra.Directed Mathlib.Geometry.Euclidean.Inversion.Basic Mathlib.Algebra.MvPolynomial.Polynomial Mathlib.Topology.Algebra.Module.Multilinear.Topology Mathlib.Algebra.Lie.Rank Mathlib.Analysis.Normed.Group.ControlledClosure Mathlib.AlgebraicTopology.MooreComplex Mathlib.Probability.Kernel.Condexp Mathlib.Condensed.Light.Functors Mathlib.NumberTheory.Zsqrtd.Basic Mathlib.Topology.Compactness.Paracompact 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.Topology.Sheaves.Presheaf Mathlib.Analysis.Asymptotics.Asymptotics Mathlib.Data.Nat.Cast.Order.Ring Mathlib.Tactic.mwe Mathlib.Algebra.GeomSum Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.CategoryTheory.Adhesive Mathlib.FieldTheory.PerfectClosure Mathlib.LinearAlgebra.CliffordAlgebra.Prod Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra Mathlib.MeasureTheory.Measure.WithDensity Mathlib.Data.Int.Lemmas 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.Probability.Kernel.Disintegration.CdfToKernel Mathlib.MeasureTheory.Function.SimpleFuncDense Mathlib.Data.Complex.Abs Mathlib.Tactic.GCongr Mathlib.Computability.PartrecCode Mathlib.Algebra.Order.Group.InjSurj 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.Topology.Category.TopCat.Limits.Basic Mathlib.Algebra.Polynomial.Bivariate Mathlib.Analysis.Analytic.Inverse Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.Algebra.Algebra.Defs Mathlib.Analysis.NormedSpace.FunctionSeries Mathlib.Topology.IsLocalHomeomorph Mathlib.Topology.Defs.Filter Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma Mathlib.Geometry.Euclidean.Triangle Mathlib.AlgebraicGeometry.Restrict Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.Topology.Algebra.Module.Alternating.Basic Mathlib.Data.Int.CardIntervalMod Mathlib.RingTheory.MvPowerSeries.Basic Mathlib.Algebra.MonoidAlgebra.Basic Mathlib.SetTheory.Game.Ordinal Mathlib.Analysis.NormedSpace.IndicatorFunction Mathlib.Algebra.Category.ModuleCat.Projective Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Topology.Algebra.Order.Rolle Mathlib.Algebra.Homology.HomotopyCofiber Mathlib.Data.List.Iterate Mathlib.GroupTheory.SpecificGroups.KleinFour Mathlib.RingTheory.Unramified.Derivations Mathlib.Probability.Distributions.Gamma Mathlib.LinearAlgebra.Eigenspace.Zero Mathlib.Algebra.Polynomial.Roots Mathlib.AlgebraicTopology.KanComplex Mathlib.Analysis.Normed.Group.Constructions Mathlib.RingTheory.Ideal.Basic Mathlib.Probability.Martingale.OptionalStopping Mathlib.RingTheory.Flat.Stability Mathlib.Probability.Martingale.BorelCantelli Mathlib.Data.Nat.Choose.Central Mathlib.Analysis.SpecialFunctions.ExpDeriv Mathlib.RingTheory.FiniteType Mathlib.RingTheory.Ideal.Basis Mathlib.adomaniLeanUtils.sittingPuzzle Mathlib.Condensed.Functors Mathlib.Geometry.Manifold.DerivationBundle Mathlib.LinearAlgebra.Eigenspace.Minpoly Mathlib.Computability.Ackermann Mathlib.MeasureTheory.Constructions.Projective Mathlib.Algebra.Category.ModuleCat.Images Mathlib.Analysis.NormedSpace.BallAction Mathlib.MeasureTheory.Measure.MeasureSpace Mathlib.Topology.Category.TopCat.Yoneda Mathlib.MeasureTheory.Measure.MeasureSpaceDef Mathlib.Algebra.CharP.IntermediateField Mathlib.Algebra.Algebra.NonUnitalSubalgebra Mathlib.Data.Int.Range Mathlib.MeasureTheory.Group.Action Mathlib.Probability.Density Mathlib.Dynamics.BirkhoffSum.NormedSpace Mathlib.Topology.UniformSpace.UniformConvergenceTopology Mathlib.Combinatorics.SimpleGraph.Finite Mathlib.SetTheory.Cardinal.ToNat Mathlib.Data.Nat.Factorization.PrimePow Mathlib.Topology.ContinuousFunction.FunctionalCalculus Mathlib.LinearAlgebra.Projectivization.Subspace Mathlib.Topology.Category.TopCommRingCat Mathlib.Analysis.Complex.RealDeriv Mathlib.Analysis.Convex.Caratheodory Mathlib.Data.Finsupp.AList Mathlib.Analysis.Complex.OpenMapping Mathlib.LinearAlgebra.AffineSpace.Slope Mathlib.AlgebraicGeometry.PrimeSpectrum.IsOpenComapC Mathlib.Algebra.BigOperators.WithTop Mathlib.GroupTheory.GroupAction.FixingSubgroup Mathlib.MeasureTheory.OuterMeasure.Basic Mathlib.Probability.ProbabilityMassFunction.Integrals Mathlib.MeasureTheory.Function.AEMeasurableSequence Mathlib.Topology.Order.Bornology Mathlib.Condensed.Equivalence Mathlib.Data.Complex.Orientation Mathlib.RingTheory.Polynomial.RationalRoot Mathlib.Analysis.Convex.Quasiconvex Mathlib.Analysis.Calculus.Dslope Mathlib.RingTheory.WittVector.FrobeniusFractionField Mathlib.Deprecated.Subfield Mathlib.Topology.Algebra.Module.CharacterSpace Mathlib.Data.ENNReal.Basic Mathlib.LinearAlgebra.Matrix.ToLinearEquiv Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Topology.OmegaCompletePartialOrder Mathlib.Topology.Homotopy.Equiv Mathlib.RingTheory.Ideal.Prod Mathlib.Order.Filter.Extr Mathlib.Algebra.Polynomial.CancelLeads Mathlib.Analysis.NormedSpace.Connected Mathlib.Algebra.MvPolynomial.Degrees Mathlib.Topology.Algebra.GroupWithZero Mathlib.Topology.Category.Profinite.Product Mathlib.RingTheory.IntegralDomain Mathlib.Algebra.Algebra.Hom Mathlib.Topology.Homotopy.HSpaces Mathlib.Combinatorics.Optimization.ValuedCSP Mathlib.Algebra.DirectSum.Algebra Mathlib.Topology.Connected.Separation Mathlib.Topology.Category.Profinite.Limits Mathlib.Topology.MetricSpace.Completion Mathlib.Analysis.ODE.PicardLindelof Mathlib.GroupTheory.SpecificGroups.Dihedral Mathlib.Combinatorics.SimpleGraph.IncMatrix Mathlib.Topology.Category.UniformSpace Mathlib.CategoryTheory.Linear.Yoneda Mathlib.RingTheory.RootsOfUnity.Minpoly Mathlib.Topology.Instances.NNReal Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.RingTheory.Localization.Cardinality Mathlib.Topology.Order.ExtrClosure Mathlib.Probability.ConditionalExpectation Mathlib.CategoryTheory.Sites.Coherent.SheafComparison Mathlib.FieldTheory.Tower Mathlib.MeasureTheory.Measure.Haar.Basic Mathlib.MeasureTheory.Integral.SetIntegral Mathlib.RingTheory.HahnSeries.Multiplication Mathlib.Analysis.Calculus.Deriv.Slope Mathlib.Topology.Category.FinTopCat Mathlib.NumberTheory.FLT.Basic Mathlib.adomaniLeanUtils.stubForJunk Mathlib.Algebra.Module.Submodule.Order Mathlib.Analysis.Analytic.Polynomial Mathlib.Algebra.Homology.HomologySequence Mathlib.SetTheory.Cardinal.Finite Mathlib.Analysis.SpecificLimits.RCLike Mathlib.Analysis.InnerProductSpace.ConformalLinearMap Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.Geometry.RingedSpace.PresheafedSpace 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.Topology.UniformSpace.Equicontinuity Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward Mathlib.Algebra.Order.Field.Pi Mathlib.LinearAlgebra.TensorProduct.Graded.Internal Mathlib.LinearAlgebra.Dimension.Finite Mathlib.Analysis.LocallyConvex.BalancedCoreHull Mathlib.SetTheory.Cardinal.Ordinal Mathlib.RingTheory.DedekindDomain.PID Mathlib.Analysis.SpecialFunctions.Pow.NNReal Mathlib.Algebra.Category.Grp.Injective Mathlib.RingTheory.FreeRing Mathlib.MeasureTheory.Constructions.BorelSpace.Order Mathlib.Tactic.Linarith.Verification Mathlib.Algebra.Category.BoolRing Mathlib.FieldTheory.AxGrothendieck Mathlib.Analysis.Convex.StoneSeparation Mathlib.LinearAlgebra.Basis.Bilinear Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.Algebra.Algebra.NonUnitalHom Mathlib.Tactic Mathlib.AlgebraicTopology.SimplicialCategory.Basic Mathlib.Algebra.DualNumber Mathlib.MeasureTheory.Integral.Indicator Mathlib.Algebra.Order.Group.TypeTags Mathlib.Algebra.Module.LocalizedModule Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.Topology.Category.TopCat.EffectiveEpi Mathlib.CategoryTheory.Linear.FunctorCategory Mathlib.Algebra.Star.Unitary Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.Geometry.Euclidean.PerpBisector Mathlib.Tactic.Widget.GCongr Mathlib.Topology.Order.Hom.Basic Mathlib.Topology.Order.IsLUB Mathlib.Topology.Algebra.InfiniteSum.Real Mathlib.Analysis.Normed.Group.Rat Mathlib.Data.Nat.GCD.Basic Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.Topology.MetricSpace.Closeds Mathlib.Algebra.Homology.ShortComplex.ShortExact Mathlib.LinearAlgebra.FiniteSpan Mathlib.Algebra.Order.Ring.Rat Mathlib.SetTheory.Ordinal.FixedPointApproximants Mathlib.MeasureTheory.Group.Integral Mathlib.Topology.ContinuousFunction.StoneWeierstrass Mathlib.LinearAlgebra.LinearPMap Mathlib.Topology.Algebra.ContinuousAffineMap Mathlib.LinearAlgebra.Matrix.IsDiag Mathlib.Analysis.Convex.Radon Mathlib.Algebra.Category.Ring.Adjunctions Mathlib.Algebra.Lie.TensorProduct Mathlib.Algebra.Order.Field.Canonical.Basic Mathlib.Algebra.Homology.HomotopyCategory Mathlib.Data.Int.ModEq Mathlib.FieldTheory.SplittingField.Construction Mathlib.LinearAlgebra.TensorProduct.Basic Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Data.Int.Order.Units Mathlib.LinearAlgebra.Prod Mathlib.Topology.Sheaves.Sheafify Mathlib.LinearAlgebra.TensorProduct.Basis Mathlib.Topology.MetricSpace.DilationEquiv Mathlib.FieldTheory.RatFunc.Basic Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.Topology.Semicontinuous Mathlib.Algebra.Lie.Weights.Linear Mathlib.Algebra.Module.LinearMap.Rat 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.Probability.Integration Mathlib.Analysis.Distribution.SchwartzSpace 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.Data.DFinsupp.Order Mathlib.MeasureTheory.OuterMeasure.AE Mathlib.SetTheory.Surreal.Basic Mathlib.Algebra.Order.Field.Subfield Mathlib.GroupTheory.Schreier Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean Mathlib.RingTheory.NormTrace Mathlib.MeasureTheory.Measure.Complex Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.Data.Matrix.Notation Mathlib.RingTheory.Localization.FractionRing Mathlib.RingTheory.TensorProduct.Basic Mathlib.LinearAlgebra.AffineSpace.Midpoint Mathlib.Algebra.Module.Submodule.LinearMap Mathlib.ModelTheory.ElementaryMaps Mathlib.Combinatorics.SimpleGraph.AdjMatrix Mathlib.RingTheory.IntegrallyClosed Mathlib.Algebra.Module.GradedModule Mathlib.Algebra.Polynomial.Degree.TrailingDegree Mathlib.Tactic.SlimCheck Mathlib.Topology.Order.MonotoneContinuity Mathlib.Topology.Algebra.NormedValued Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Geometry.Manifold.Metrizable Mathlib.Topology.Algebra.Module.Cardinality Mathlib.RingTheory.Valuation.RankOne Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.NumberTheory.LSeries.Convolution Mathlib.Analysis.NormedSpace.Ray Mathlib.MeasureTheory.Function.Floor Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.LinearAlgebra.Dimension.RankNullity Mathlib.Algebra.Algebra.Tower Mathlib.LinearAlgebra.Basis.Flag Mathlib.Algebra.Ring.NegOnePow Mathlib.Analysis.Normed.Group.AddTorsor Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.Combinatorics.Derangements.Finite 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.Topology.Algebra.InfiniteSum.Basic Mathlib.Topology.AlexandrovDiscrete Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Analysis.NormedSpace.SphereNormEquiv Mathlib.Topology.Order.Category.FrameAdjunction Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.Topology.UniformSpace.Equiv Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent Mathlib.FieldTheory.RatFunc.Degree Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.RingTheory.QuotientNoetherian Mathlib.RingTheory.Trace Mathlib.Algebra.Module.Rat Mathlib.RingTheory.RootsOfUnity.Basic Mathlib.Algebra.Lie.CartanExists Mathlib.RingTheory.Localization.Away.AdjoinRoot Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated Mathlib.Algebra.Order.AbsoluteValue Mathlib.Data.Nat.PrimeFin Mathlib.Analysis.SpecialFunctions.Trigonometric.Series Mathlib.Algebra.Polynomial.Module.AEval Mathlib.Tactic.Linarith.Lemmas Mathlib.MeasureTheory.Integral.Average Mathlib.Data.PNat.Factors Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.Analysis.Convex.PartitionOfUnity Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings Mathlib.Combinatorics.SimpleGraph.Matching Mathlib.Algebra.Module.Submodule.Ker Mathlib.LinearAlgebra.FreeModule.Basic Mathlib.Topology.Sheaves.Stalks Mathlib.Tactic.NormNum.GCD Mathlib.Probability.Independence.Conditional Mathlib.Analysis.Complex.AbelLimit Mathlib.Topology.ContinuousOn 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.Algebra.Order.Positive.Ring Mathlib.Algebra.Order.Rearrangement Mathlib.MeasureTheory.Integral.Lebesgue Mathlib.SetTheory.Ordinal.Basic Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.Algebra.ModEq Mathlib.Order.Filter.CardinalInter Mathlib.RingTheory.Perfection Mathlib.Analysis.Normed.Group.Basic Mathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Combinatorics.SimpleGraph.Coloring Mathlib.Data.Nat.PrimeNormNum Mathlib.Algebra.Homology.ConcreteCategory Mathlib.Combinatorics.Enumerative.Partition Mathlib.Data.Real.Pi.Wallis Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Notation Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.FunctionField Mathlib.Algebra.DirectSum.LinearMap Mathlib.Topology.Algebra.InfiniteSum.Constructions Mathlib.Algebra.Homology.Factorizations.Basic Mathlib.Tactic.NormNum Mathlib.Algebra.Group.ConjFinite Mathlib.LinearAlgebra.ExteriorAlgebra.Basic Mathlib.Topology.Baire.CompleteMetrizable Mathlib.MeasureTheory.Function.SimpleFunc Mathlib.Algebra.BigOperators.Module Mathlib.Combinatorics.SimpleGraph.Ends.Properties Mathlib.NumberTheory.DiophantineApproximation Mathlib.Data.Nat.Totient Mathlib.RingTheory.PowerSeries.Basic Mathlib.Algebra.Order.Ring.Cone Mathlib.Data.Int.SuccPred Mathlib.RingTheory.TensorProduct.MvPolynomial Mathlib.LinearAlgebra.TensorProduct.Vanishing Mathlib.Algebra.Module.Submodule.Pointwise Mathlib.Order.Filter.EventuallyConst Mathlib.Algebra.Polynomial.Smeval Mathlib.LinearAlgebra.StdBasis Mathlib.Analysis.Convex.Exposed Mathlib.Order.KrullDimension Mathlib.Topology.MetricSpace.Pseudo.Defs Mathlib.Combinatorics.SimpleGraph.Connectivity Mathlib.Logic.Godel.GodelBetaFunction Mathlib.LinearAlgebra.Matrix.Circulant Mathlib.LinearAlgebra.Matrix.Dual Mathlib.LinearAlgebra.Matrix.Orthogonal Mathlib.Algebra.Order.Group.Basic Mathlib.CategoryTheory.Preadditive.Yoneda.Limits Mathlib.Data.Nat.MaxPowDiv Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.Data.Int.GCD Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.Topology.Instances.Sign Mathlib.Topology.MetricSpace.Pseudo.Constructions Mathlib.LinearAlgebra.AffineSpace.AffineMap Mathlib.LinearAlgebra.Basis.VectorSpace Mathlib.Data.Complex.ExponentialBounds Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.Topology.Instances.ENNReal Mathlib.CategoryTheory.Sites.Coherent.RegularTopology Mathlib.Probability.Martingale.Centering Mathlib.Algebra.Order.Ring.Defs Mathlib.Topology.Category.TopCat.Limits.Pullbacks Mathlib.Algebra.Lie.OfAssociative Mathlib.Topology.Category.Stonean.Limits Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat Mathlib.GroupTheory.FreeAbelianGroup Mathlib.RingTheory.PowerSeries.Inverse Mathlib.LinearAlgebra.AffineSpace.AffineSubspace Mathlib.adomaniLeanUtils.extractDecl Mathlib.Data.Analysis.Filter Mathlib.Topology.Inseparable Mathlib.LinearAlgebra.QuadraticForm.Dual Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.Order.Filter.Interval Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.Topology.Support Mathlib.Topology.Instances.RatLemmas Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.Algebra.Polynomial.Div Mathlib.Topology.MetricSpace.Bounded Mathlib.Logic.Small.Ring Mathlib.LinearAlgebra.Matrix.Block Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.Geometry.Manifold.VectorBundle.SmoothSection Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.Geometry.Manifold.ContMDiff.Product Mathlib.Topology.QuasiSeparated Mathlib.LinearAlgebra.RootSystem.Defs Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.LinearAlgebra.Projectivization.Basic Mathlib.RingTheory.WittVector.MulP Mathlib.LinearAlgebra.Quotient Mathlib.Topology.Algebra.Order.Archimedean Mathlib.Topology.Algebra.ContinuousMonoidHom Mathlib.Topology.MetricSpace.MetricSeparated Mathlib.Data.Nat.Factorial.SuperFactorial	1
Mathlib.Algebra.Order.Group.Unbundled.Basic	179

Technically, the import difference can be displayed.

[mattrobball]

@adomani Can this compute the change in the number of leaves in the import graph over a module?

[adomani]

I am not sure how to read the change in number of leaves from the current data, but the number of leaves can certainly be computed!

In fact, I wonder whether "transitive imports" is really what we should be looking at. Maybe something like "number of covering relations" or "average number of covering relations" might be a better statistic. After all, we would like to distinguish an import system like

0--0--0--0--0

from a complete graph on 5 vertices and I am not sure which statistic would make the two "clearly" different.

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style