feat(Order/WellFoundedSet): a set is finite if both a linear order and its opposite order are well founded on it#39779
Open
Hagb wants to merge 8 commits into
Open
Conversation
…ty_relEmbedding_of_isWellOrder` Resolve leanprover-community#39545 (comment), leanprover-community#39545 (comment), leanprover-community#39545 (comment)
…stricted on the subtype is `WellFounded`
It is a lemma for
```lean
theorem wellFoundedLT_of_monotone_prod
{α β γ : Type*} [LinearOrder α] [LinearOrder β] [WellFoundedLT α] [WellFoundedLT β]
[PartialOrder γ] {f : α × β ≃ γ} (mono : Monotone f) : WellFoundedLT γ
```
…d its opposite order are well founded on it
PR summary 8e24494970
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Order.OrderIsoNat | 581 | 588 | +7 (+1.20%) |
| Mathlib.Order.WellFoundedSet | 590 | 594 | +4 (+0.68%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Algebra.Order.Module.HahnEmbedding Mathlib.RingTheory.HahnSeries.Lex |
1 |
282 filesMathlib.Algebra.Category.AlgCat.Limits Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Limits Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono Mathlib.Algebra.Category.ModuleCat.Presheaf.Free Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal Mathlib.Algebra.Category.ModuleCat.Presheaf.PushforwardZeroMonoidal Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.Algebra.Category.ModuleCat.Pseudofunctor Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.Algebra.Category.ModuleCat.Stalk Mathlib.Algebra.Colimit.Finiteness Mathlib.Algebra.Colimit.Module Mathlib.Algebra.Colimit.Ring Mathlib.Algebra.Colimit.TensorProduct Mathlib.Algebra.Order.Ring.Archimedean Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit Mathlib.AlgebraicTopology.FundamentalGroupoid.Product Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected Mathlib.AlgebraicTopology.SimplicialSet.TopAdj Mathlib.AlgebraicTopology.SingularHomology.Basic Mathlib.AlgebraicTopology.SingularHomology.HomologyZero Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvarianceTopCat Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance Mathlib.AlgebraicTopology.SingularSet Mathlib.AlgebraicTopology.TopologicalSimplex Mathlib.Analysis.Asymptotics.Defs Mathlib.Analysis.CStarAlgebra.Basic Mathlib.Analysis.CStarAlgebra.Module.Synonym Mathlib.Analysis.CStarAlgebra.Unitary.Maps Mathlib.Analysis.Calculus.TangentCone.Basic Mathlib.Analysis.Calculus.TangentCone.DimOne Mathlib.Analysis.Calculus.TangentCone.Pi Mathlib.Analysis.Calculus.TangentCone.Prod Mathlib.Analysis.Calculus.TangentCone.ProperSpace Mathlib.Analysis.Calculus.TangentCone.Real Mathlib.Analysis.Calculus.TangentCone Mathlib.Analysis.Convex.Cone.Basic Mathlib.Analysis.Convex.Cone.Closure Mathlib.Analysis.Convex.ContinuousLinearEquiv Mathlib.Analysis.Convex.Contractible Mathlib.Analysis.Convex.EGauge Mathlib.Analysis.Convex.Exposed Mathlib.Analysis.Convex.Extrema Mathlib.Analysis.Convex.FunctionTopology Mathlib.Analysis.Convex.MetricSpace Mathlib.Analysis.Convex.PathConnected Mathlib.Analysis.Convex.Quasiconvex Mathlib.Analysis.Convex.StdSimplex Mathlib.Analysis.Convex.Strict Mathlib.Analysis.Convex.Topology Mathlib.Analysis.Convex.TotallyBounded Mathlib.Analysis.Fourier.Notation Mathlib.Analysis.LocallyConvex.AbsConvex Mathlib.Analysis.LocallyConvex.BalancedCoreHull Mathlib.Analysis.LocallyConvex.Basic Mathlib.Analysis.LocallyConvex.Bounded Mathlib.Analysis.LocallyConvex.Polar Mathlib.Analysis.LocallyConvex.StrongTopology Mathlib.Analysis.Normed.Affine.AddTorsor Mathlib.Analysis.Normed.Affine.Ceva Mathlib.Analysis.Normed.Affine.Isometry Mathlib.Analysis.Normed.Affine.MazurUlam Mathlib.Analysis.Normed.Affine.Simplex Mathlib.Analysis.Normed.Field.Basic Mathlib.Analysis.Normed.Field.Instances Mathlib.Analysis.Normed.Field.Lemmas Mathlib.Analysis.Normed.Field.TransferInstance Mathlib.Analysis.Normed.Field.UnitBall Mathlib.Analysis.Normed.Group.AddTorsor Mathlib.Analysis.Normed.Group.BallSphere Mathlib.Analysis.Normed.Group.Bounded Mathlib.Analysis.Normed.Group.Completion Mathlib.Analysis.Normed.Group.Continuity Mathlib.Analysis.Normed.Group.HomCompletion Mathlib.Analysis.Normed.Group.Hom Mathlib.Analysis.Normed.Group.Lemmas Mathlib.Analysis.Normed.Group.NullSubmodule Mathlib.Analysis.Normed.Group.Rat Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion Mathlib.Analysis.Normed.Group.SemiNormedGrp Mathlib.Analysis.Normed.Group.SeparationQuotient Mathlib.Analysis.Normed.Group.Uniform Mathlib.Analysis.Normed.Module.Ball.Action Mathlib.Analysis.Normed.Module.Ball.RadialEquiv Mathlib.Analysis.Normed.Module.Basic Mathlib.Analysis.Normed.Module.Extr Mathlib.Analysis.Normed.Module.RCLike.Real Mathlib.Analysis.Normed.Module.Ray Mathlib.Analysis.Normed.Module.Shrink Mathlib.Analysis.Normed.Module.Span Mathlib.Analysis.Normed.Module.TransferInstance Mathlib.Analysis.Normed.MulAction Mathlib.Analysis.Normed.Operator.Compact.Basic Mathlib.Analysis.Normed.Operator.Conformal Mathlib.Analysis.Normed.Operator.ContinuousLinearMap Mathlib.Analysis.Normed.Operator.LinearIsometry Mathlib.Analysis.Normed.Order.Lattice Mathlib.Analysis.Normed.Ring.Basic Mathlib.Analysis.Normed.Ring.Int Mathlib.Analysis.Normed.Ring.Lemmas Mathlib.Analysis.Normed.Ring.TransferInstance Mathlib.Analysis.Normed.Ring.WithAbs Mathlib.Analysis.Oscillation Mathlib.Analysis.Polynomial.CauchyBound Mathlib.Analysis.Seminorm Mathlib.Analysis.Subadditive Mathlib.Geometry.Manifold.ChartedSpace Mathlib.Geometry.Manifold.HasGroupoid Mathlib.Geometry.Manifold.Instances.Quotient Mathlib.Geometry.Manifold.LocalInvariantProperties Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.GroupTheory.DivisibleHull Mathlib.LinearAlgebra.TensorProduct.DirectLimit Mathlib.NumberTheory.Harmonic.Int Mathlib.NumberTheory.Padics.PadicNumbers Mathlib.RingTheory.IdealFilter.Basic Mathlib.RingTheory.IdealFilter.Topology Mathlib.RingTheory.Morita.Basic Mathlib.RingTheory.Morita.Matrix Mathlib.RingTheory.MvPowerSeries.GaussNorm Mathlib.RingTheory.Polynomial.GaussNorm Mathlib.RingTheory.PowerSeries.GaussNorm Mathlib.Topology.Algebra.AffineSubspace Mathlib.Topology.Algebra.Affine Mathlib.Topology.Algebra.Algebra.Equiv Mathlib.Topology.Algebra.Algebra Mathlib.Topology.Algebra.ContinuousAffineEquiv Mathlib.Topology.Algebra.ContinuousAffineMap Mathlib.Topology.Algebra.Equicontinuity Mathlib.Topology.Algebra.Field Mathlib.Topology.Algebra.FilterBasis Mathlib.Topology.Algebra.Group.Basic Mathlib.Topology.Algebra.Group.CompactOpen Mathlib.Topology.Algebra.Group.Compact Mathlib.Topology.Algebra.Group.Extension Mathlib.Topology.Algebra.Group.GroupTopology Mathlib.Topology.Algebra.Group.OpenMapping Mathlib.Topology.Algebra.Group.Pointwise Mathlib.Topology.Algebra.Group.Quotient Mathlib.Topology.Algebra.Group.SubmonoidClosure Mathlib.Topology.Algebra.Group.TopologicalAbelianization Mathlib.Topology.Algebra.Group.Units Mathlib.Topology.Algebra.GroupCompletion Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt Mathlib.Topology.Algebra.InfiniteSum.Field Mathlib.Topology.Algebra.InfiniteSum.UniformOn Mathlib.Topology.Algebra.IntermediateField Mathlib.Topology.Algebra.IsUniformGroup.Basic Mathlib.Topology.Algebra.IsUniformGroup.Constructions Mathlib.Topology.Algebra.IsUniformGroup.Defs Mathlib.Topology.Algebra.IsUniformGroup.Order Mathlib.Topology.Algebra.LinearMapCompletion Mathlib.Topology.Algebra.LinearTopology Mathlib.Topology.Algebra.Localization Mathlib.Topology.Algebra.MetricSpace.Lipschitz Mathlib.Topology.Algebra.Module.Alternating.Basic Mathlib.Topology.Algebra.Module.Alternating.Topology Mathlib.Topology.Algebra.Module.Basic Mathlib.Topology.Algebra.Module.ClosedSubmodule Mathlib.Topology.Algebra.Module.Compact Mathlib.Topology.Algebra.Module.Complement Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict Mathlib.Topology.Algebra.Module.Equiv Mathlib.Topology.Algebra.Module.LinearMapPiProd Mathlib.Topology.Algebra.Module.LinearMap Mathlib.Topology.Algebra.Module.LinearPMap Mathlib.Topology.Algebra.Module.LocallyConvex Mathlib.Topology.Algebra.Module.Multilinear.Basic Mathlib.Topology.Algebra.Module.Multilinear.Bounded Mathlib.Topology.Algebra.Module.Multilinear.Topology Mathlib.Topology.Algebra.Module.PerfectPairing Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM Mathlib.Topology.Algebra.Module.Spaces.WeakBilin Mathlib.Topology.Algebra.Module.Spaces.WeakDual Mathlib.Topology.Algebra.Module.Star Mathlib.Topology.Algebra.Module.StrongTopology Mathlib.Topology.Algebra.Module.TransferInstance Mathlib.Topology.Algebra.Module.UniformConvergence Mathlib.Topology.Algebra.Monoid.FunOnFinite Mathlib.Topology.Algebra.MvPolynomial Mathlib.Topology.Algebra.NonUnitalAlgebra Mathlib.Topology.Algebra.NonUnitalStarAlgebra Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology Mathlib.Topology.Algebra.Nonarchimedean.Bases Mathlib.Topology.Algebra.Nonarchimedean.Basic Mathlib.Topology.Algebra.Nonarchimedean.Completion Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected Mathlib.Topology.Algebra.OpenSubgroup Mathlib.Topology.Algebra.Order.Field Mathlib.Topology.Algebra.Order.LiminfLimsup Mathlib.Topology.Algebra.Order.UpperLower Mathlib.Topology.Algebra.ProperAction.AddTorsor Mathlib.Topology.Algebra.ProperAction.Basic Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace Mathlib.Topology.Algebra.Ring.Basic Mathlib.Topology.Algebra.Ring.Ideal Mathlib.Topology.Algebra.Ring.Real Mathlib.Topology.Algebra.SeparationQuotient.Basic Mathlib.Topology.Algebra.SeparationQuotient.FiniteDimensional Mathlib.Topology.Algebra.SeparationQuotient.Hom Mathlib.Topology.Algebra.SeparationQuotient.Section Mathlib.Topology.Algebra.Star.Unitary Mathlib.Topology.Algebra.StarSubalgebra Mathlib.Topology.Algebra.TopologicallyNilpotent Mathlib.Topology.Algebra.UniformConvergence Mathlib.Topology.Algebra.UniformField Mathlib.Topology.Algebra.UniformFilterBasis Mathlib.Topology.Algebra.UniformMulAction Mathlib.Topology.Algebra.UniformRing Mathlib.Topology.Bornology.BoundedOperation Mathlib.Topology.CWComplex.Classical.Basic Mathlib.Topology.CWComplex.Classical.Finite Mathlib.Topology.CWComplex.Classical.Graph Mathlib.Topology.CWComplex.Classical.Subcomplex Mathlib.Topology.Category.TopCat.Monoidal Mathlib.Topology.Category.TopCommRingCat Mathlib.Topology.Category.TopPair Mathlib.Topology.Connected.LocPathConnected Mathlib.Topology.Connected.PathComponentOne Mathlib.Topology.Connected.PathConnected Mathlib.Topology.ContinuousMap.Algebra Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli Mathlib.Topology.ContinuousMap.Bounded.Basic Mathlib.Topology.ContinuousMap.Lattice Mathlib.Topology.ContinuousMap.LocallyConstant Mathlib.Topology.ContinuousMap.LocallyConvex Mathlib.Topology.ContinuousMap.Star Mathlib.Topology.Covering.Quotient Mathlib.Topology.Homotopy.Affine Mathlib.Topology.Homotopy.Basic Mathlib.Topology.Homotopy.Contractible Mathlib.Topology.Homotopy.Equiv Mathlib.Topology.Homotopy.HSpaces Mathlib.Topology.Homotopy.HomotopyGroup Mathlib.Topology.Homotopy.Lifting Mathlib.Topology.Homotopy.LocallyContractible Mathlib.Topology.Homotopy.Path Mathlib.Topology.Homotopy.Product Mathlib.Topology.Homotopy.TopCat.Basic Mathlib.Topology.Homotopy.TopCat.Path Mathlib.Topology.Homotopy.TopCat.ToSSet Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy Mathlib.Topology.Instances.Rat Mathlib.Topology.Instances.RealVectorSpace Mathlib.Topology.Instances.TrivSqZeroExt Mathlib.Topology.Instances.ZMultiples Mathlib.Topology.LocallyConstant.Algebra Mathlib.Topology.MetricSpace.Algebra Mathlib.Topology.MetricSpace.CauSeqFilter Mathlib.Topology.MetricSpace.Completion Mathlib.Topology.Path Mathlib.Topology.Subpath Mathlib.Topology.UniformSpace.CompareReals Mathlib.Topology.UniformSpace.Dini Mathlib.Topology.UniformSpace.Matrix Mathlib.Topology.UniformSpace.Path Mathlib.Topology.UniformSpace.ProdApproximation Mathlib.Topology.UnitInterval |
3 |
616 filesMathlib.Algebra.AffineMonoid.Basic Mathlib.Algebra.AffineMonoid.Irreducible Mathlib.Algebra.Algebra.Bilinear Mathlib.Algebra.Algebra.NonUnitalSubalgebra Mathlib.Algebra.Algebra.Operations Mathlib.Algebra.Algebra.RestrictScalars Mathlib.Algebra.Algebra.Spectrum.Basic Mathlib.Algebra.Algebra.Spectrum.Pi Mathlib.Algebra.Algebra.Spectrum.Quasispectrum Mathlib.Algebra.Algebra.StrictPositivity Mathlib.Algebra.Algebra.Subalgebra.Basic Mathlib.Algebra.Algebra.Subalgebra.Centralizer Mathlib.Algebra.Algebra.Subalgebra.Directed Mathlib.Algebra.Algebra.Subalgebra.Lattice Mathlib.Algebra.Algebra.Subalgebra.Matrix Mathlib.Algebra.Algebra.Subalgebra.MulOpposite Mathlib.Algebra.Algebra.Subalgebra.Operations Mathlib.Algebra.Algebra.Subalgebra.Order Mathlib.Algebra.Algebra.Subalgebra.Pi Mathlib.Algebra.Algebra.Subalgebra.Pointwise Mathlib.Algebra.Algebra.Subalgebra.Prod Mathlib.Algebra.Algebra.Subalgebra.Tower Mathlib.Algebra.Algebra.Subalgebra.Unitization Mathlib.Algebra.Algebra.Tower Mathlib.Algebra.Algebra.Unitization Mathlib.Algebra.Azumaya.Defs Mathlib.Algebra.Category.AlgCat.Basic Mathlib.Algebra.Category.AlgCat.Monoidal Mathlib.Algebra.Category.AlgCat.Symmetric Mathlib.Algebra.Category.BialgCat.Basic Mathlib.Algebra.Category.BialgCat.Monoidal Mathlib.Algebra.Category.CoalgCat.Basic Mathlib.Algebra.Category.CoalgCat.ComonEquivalence Mathlib.Algebra.Category.CoalgCat.Monoidal Mathlib.Algebra.Category.Grp.Injective Mathlib.Algebra.Category.HopfAlgCat.Basic Mathlib.Algebra.Category.HopfAlgCat.Monoidal Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.Algebra.Category.ModuleCat.Algebra Mathlib.Algebra.Category.ModuleCat.Colimits Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.Algebra.Category.ModuleCat.FilteredColimits Mathlib.Algebra.Category.ModuleCat.Injective Mathlib.Algebra.Category.ModuleCat.LeftResolution Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric Mathlib.Algebra.Category.ModuleCat.Products Mathlib.Algebra.Category.ModuleCat.Projective Mathlib.Algebra.Category.ModuleCat.Tannaka Mathlib.Algebra.Category.Ring.Adjunctions Mathlib.Algebra.Central.Basic Mathlib.Algebra.Central.Defs Mathlib.Algebra.Central.End Mathlib.Algebra.Central.Matrix Mathlib.Algebra.CharP.Algebra Mathlib.Algebra.CharP.IntermediateField Mathlib.Algebra.CharP.Subring Mathlib.Algebra.DirectSum.Algebra Mathlib.Algebra.DirectSum.Decomposition Mathlib.Algebra.DirectSum.Finsupp Mathlib.Algebra.DirectSum.Internal Mathlib.Algebra.DirectSum.Module Mathlib.Algebra.DualNumber Mathlib.Algebra.Exact Mathlib.Algebra.FiveLemma Mathlib.Algebra.FreeAlgebra Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra Mathlib.Algebra.Group.ForwardDiff Mathlib.Algebra.Group.Irreducible.Indecomposable Mathlib.Algebra.Group.Subgroup.Pointwise Mathlib.Algebra.Group.Submonoid.Pointwise Mathlib.Algebra.Group.Submonoid.Support Mathlib.Algebra.Group.Submonoid.Units Mathlib.Algebra.Group.UniqueProds.VectorSpace Mathlib.Algebra.GroupWithZero.Range Mathlib.Algebra.GroupWithZero.Subgroup Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise Mathlib.Algebra.Module.Bimodule Mathlib.Algebra.Module.GradedModule Mathlib.Algebra.Module.Injective Mathlib.Algebra.Module.LocalizedModule.AtPrime Mathlib.Algebra.Module.LocalizedModule.Away Mathlib.Algebra.Module.LocalizedModule.Basic Mathlib.Algebra.Module.LocalizedModule.Exact Mathlib.Algebra.Module.LocalizedModule.Int Mathlib.Algebra.Module.LocalizedModule.IsLocalization Mathlib.Algebra.Module.LocalizedModule.Submodule Mathlib.Algebra.Module.Presentation.Basic Mathlib.Algebra.Module.Presentation.Cokernel Mathlib.Algebra.Module.Presentation.DirectSum Mathlib.Algebra.Module.Presentation.Free Mathlib.Algebra.Module.Presentation.RestrictScalars Mathlib.Algebra.Module.Presentation.Tautological Mathlib.Algebra.Module.Presentation.Tensor Mathlib.Algebra.Module.Projective Mathlib.Algebra.Module.SnakeLemma Mathlib.Algebra.Module.Submodule.Bilinear Mathlib.Algebra.Module.Submodule.Finsupp Mathlib.Algebra.Module.Submodule.Pointwise Mathlib.Algebra.MonoidAlgebra.Basic Mathlib.Algebra.MonoidAlgebra.Degree Mathlib.Algebra.MonoidAlgebra.Grading Mathlib.Algebra.MonoidAlgebra.Ideal Mathlib.Algebra.MonoidAlgebra.Module Mathlib.Algebra.MonoidAlgebra.PointwiseSMul Mathlib.Algebra.MonoidAlgebra.Support Mathlib.Algebra.MonoidAlgebra.ToDirectSum Mathlib.Algebra.MvPolynomial.Basic Mathlib.Algebra.MvPolynomial.Coeff Mathlib.Algebra.MvPolynomial.Comap Mathlib.Algebra.MvPolynomial.CommRing Mathlib.Algebra.MvPolynomial.Counit Mathlib.Algebra.MvPolynomial.Degrees Mathlib.Algebra.MvPolynomial.Derivation Mathlib.Algebra.MvPolynomial.Division Mathlib.Algebra.MvPolynomial.Equiv Mathlib.Algebra.MvPolynomial.Eval Mathlib.Algebra.MvPolynomial.Invertible Mathlib.Algebra.MvPolynomial.Monad Mathlib.Algebra.MvPolynomial.PDeriv Mathlib.Algebra.MvPolynomial.Polynomial Mathlib.Algebra.MvPolynomial.Rename Mathlib.Algebra.MvPolynomial.Supported Mathlib.Algebra.MvPolynomial.Variables Mathlib.Algebra.Order.Group.Ideal Mathlib.Algebra.Order.GroupWithZero.Range Mathlib.Algebra.Polynomial.AlgebraMap Mathlib.Algebra.Polynomial.Basic Mathlib.Algebra.Polynomial.Basis Mathlib.Algebra.Polynomial.BigOperators Mathlib.Algebra.Polynomial.CancelLeads Mathlib.Algebra.Polynomial.CoeffList Mathlib.Algebra.Polynomial.CoeffMem Mathlib.Algebra.Polynomial.Coeff Mathlib.Algebra.Polynomial.Degree.Definitions Mathlib.Algebra.Polynomial.Degree.Defs Mathlib.Algebra.Polynomial.Degree.Domain Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree Mathlib.Algebra.Polynomial.Degree.Lemmas Mathlib.Algebra.Polynomial.Degree.Monomial Mathlib.Algebra.Polynomial.Degree.Operations Mathlib.Algebra.Polynomial.Degree.SmallDegree Mathlib.Algebra.Polynomial.Degree.Support Mathlib.Algebra.Polynomial.Degree.TrailingDegree Mathlib.Algebra.Polynomial.Degree.Units Mathlib.Algebra.Polynomial.DenomsClearable Mathlib.Algebra.Polynomial.Derivation Mathlib.Algebra.Polynomial.Derivative Mathlib.Algebra.Polynomial.Div Mathlib.Algebra.Polynomial.EraseLead Mathlib.Algebra.Polynomial.Eval.Algebra Mathlib.Algebra.Polynomial.Eval.Coeff Mathlib.Algebra.Polynomial.Eval.Defs Mathlib.Algebra.Polynomial.Eval.Degree Mathlib.Algebra.Polynomial.Eval.Irreducible Mathlib.Algebra.Polynomial.Eval.SMul Mathlib.Algebra.Polynomial.Eval.Subring Mathlib.Algebra.Polynomial.HasseDeriv Mathlib.Algebra.Polynomial.Identities Mathlib.Algebra.Polynomial.Inductions Mathlib.Algebra.Polynomial.Laurent Mathlib.Algebra.Polynomial.Lifts Mathlib.Algebra.Polynomial.Mirror Mathlib.Algebra.Polynomial.Module.AEval Mathlib.Algebra.Polynomial.Module.Basic Mathlib.Algebra.Polynomial.Module.TensorProduct Mathlib.Algebra.Polynomial.Monic Mathlib.Algebra.Polynomial.Monomial Mathlib.Algebra.Polynomial.OfFn Mathlib.Algebra.Polynomial.PartialFractions Mathlib.Algebra.Polynomial.Reverse Mathlib.Algebra.Polynomial.RingDivision Mathlib.Algebra.Polynomial.Smeval Mathlib.Algebra.Polynomial.SumIteratedDerivative Mathlib.Algebra.Polynomial.Taylor Mathlib.Algebra.Polynomial.UnitTrinomial Mathlib.Algebra.Ring.Subgroup Mathlib.Algebra.Ring.Submonoid.Pointwise Mathlib.Algebra.Ring.Subring.IntPolynomial Mathlib.Algebra.Ring.Subring.Pointwise Mathlib.Algebra.Ring.Subsemiring.Pointwise Mathlib.Algebra.RingQuot Mathlib.Algebra.SkewMonoidAlgebra.Basic Mathlib.Algebra.SkewMonoidAlgebra.Lift Mathlib.Algebra.SkewMonoidAlgebra.Single Mathlib.Algebra.SkewMonoidAlgebra.Support Mathlib.Algebra.SkewPolynomial.Basic Mathlib.Algebra.Star.Free Mathlib.Algebra.Star.Module Mathlib.Algebra.Star.NonUnitalSubalgebra Mathlib.Algebra.Star.RingQuot Mathlib.Algebra.Star.Subalgebra Mathlib.Algebra.Star.TensorProduct Mathlib.Algebra.Star.UnitaryStarAlgAut Mathlib.Algebra.Star.Unitary Mathlib.Algebra.TrivSqZeroExt.Basic Mathlib.Algebra.TrivSqZeroExt.Ideal Mathlib.Algebra.Vertex.HVertexOperator Mathlib.Algebra.Vertex.VertexOperator Mathlib.AlgebraicTopology.SimplicialComplex.Basic Mathlib.Analysis.Convex.Basic Mathlib.Analysis.Convex.Caratheodory Mathlib.Analysis.Convex.Combination Mathlib.Analysis.Convex.Cone.Extension Mathlib.Analysis.Convex.Extreme Mathlib.Analysis.Convex.Function Mathlib.Analysis.Convex.Hull Mathlib.Analysis.Convex.Independent Mathlib.Analysis.Convex.Jensen Mathlib.Analysis.Convex.Join Mathlib.Analysis.Convex.Mul Mathlib.Analysis.Convex.NNReal Mathlib.Analysis.Convex.Piecewise Mathlib.Analysis.Convex.Segment Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion Mathlib.Analysis.Convex.SimplicialComplex.Basic Mathlib.Analysis.Convex.Slope Mathlib.Analysis.Convex.Star Mathlib.Analysis.Convex.StoneSeparation Mathlib.Analysis.Normed.Lp.WithLp Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Monoidal.Internal.Module Mathlib.CategoryTheory.Preadditive.Yoneda.Injective Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.CategoryTheory.Sites.Spaces Mathlib.Combinatorics.Optimization.ValuedCSP Mathlib.Data.DFinsupp.Lex Mathlib.Data.Finset.MulAntidiagonal Mathlib.Data.Finset.SMulAntidiagonal Mathlib.Data.Finsupp.Lex Mathlib.Data.Finsupp.PWO Mathlib.Data.Finsupp.PointwiseSMul Mathlib.Data.Matrix.Basic Mathlib.Data.Matrix.Basis Mathlib.Data.Matrix.Bilinear Mathlib.Data.Matrix.Block Mathlib.Data.Matrix.ColumnRowPartitioned Mathlib.Data.Matrix.Composition Mathlib.Data.Matrix.DualNumber Mathlib.Data.Matrix.Invertible Mathlib.Data.Matrix.Reflection Mathlib.Data.Nat.Choose.Vandermonde Mathlib.Data.Set.MulAntidiagonal Mathlib.Data.Set.SMulAntidiagonal Mathlib.FieldTheory.IntermediateField.Adjoin.Defs Mathlib.FieldTheory.IntermediateField.Basic Mathlib.FieldTheory.IsRealClosed.Basic Mathlib.FieldTheory.RatFunc.Defs Mathlib.Geometry.Convex.Cone.Basic Mathlib.Geometry.Convex.Cone.DualFinite Mathlib.Geometry.Convex.Cone.Dual Mathlib.Geometry.Convex.Cone.Pointed Mathlib.Geometry.Convex.Cone.Simplicial Mathlib.Geometry.Convex.ConvexSpace.AffineSpace Mathlib.Geometry.Convex.ConvexSpace.Module Mathlib.Geometry.Group.Growth.LinearLowerBound Mathlib.Geometry.Manifold.StructureGroupoid Mathlib.Geometry.RingedSpace.Basic Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits Mathlib.Geometry.RingedSpace.PresheafedSpace Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.Geometry.RingedSpace.Stalks Mathlib.GroupTheory.Coxeter.Basic Mathlib.GroupTheory.Coxeter.Matrix Mathlib.GroupTheory.Divisible Mathlib.GroupTheory.DoubleCoset Mathlib.GroupTheory.Finiteness Mathlib.GroupTheory.IsSubnormal Mathlib.GroupTheory.MonoidLocalization.Finite Mathlib.GroupTheory.QuotientGroup.Basic Mathlib.GroupTheory.Submonoid.Inverses Mathlib.LinearAlgebra.AffineSpace.AffineEquiv Mathlib.LinearAlgebra.AffineSpace.AffineMap Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic Mathlib.LinearAlgebra.AffineSpace.Basis Mathlib.LinearAlgebra.AffineSpace.Centroid Mathlib.LinearAlgebra.AffineSpace.Ceva Mathlib.LinearAlgebra.AffineSpace.Combination Mathlib.LinearAlgebra.AffineSpace.Independent Mathlib.LinearAlgebra.AffineSpace.MidpointZero Mathlib.LinearAlgebra.AffineSpace.Midpoint Mathlib.LinearAlgebra.AffineSpace.Ordered Mathlib.LinearAlgebra.AffineSpace.Pointwise Mathlib.LinearAlgebra.AffineSpace.Restrict Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid Mathlib.LinearAlgebra.AffineSpace.Slope Mathlib.LinearAlgebra.Alternating.Basic Mathlib.LinearAlgebra.Alternating.Curry Mathlib.LinearAlgebra.Basis.Basic Mathlib.LinearAlgebra.Basis.Exact Mathlib.LinearAlgebra.Basis.Fin Mathlib.LinearAlgebra.Basis.Flag Mathlib.LinearAlgebra.Basis.Prod Mathlib.LinearAlgebra.Basis.SMul Mathlib.LinearAlgebra.Basis.Submodule Mathlib.LinearAlgebra.Basis.VectorSpace Mathlib.LinearAlgebra.BilinearForm.Basic Mathlib.LinearAlgebra.BilinearForm.Hom Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv Mathlib.LinearAlgebra.Complex.Module Mathlib.LinearAlgebra.Countable Mathlib.LinearAlgebra.DFinsupp Mathlib.LinearAlgebra.DirectSum.Basis Mathlib.LinearAlgebra.DirectSum.Finite Mathlib.LinearAlgebra.DirectSum.Finsupp Mathlib.LinearAlgebra.DirectSum.TensorProduct Mathlib.LinearAlgebra.Finsupp.Pi Mathlib.LinearAlgebra.Finsupp.Span Mathlib.LinearAlgebra.Finsupp.VectorSpace Mathlib.LinearAlgebra.FreeModule.Basic Mathlib.LinearAlgebra.FreeProduct.Basic Mathlib.LinearAlgebra.Goursat Mathlib.LinearAlgebra.LeftExact Mathlib.LinearAlgebra.LinearIndependent.BaseChange Mathlib.LinearAlgebra.LinearIndependent.Lemmas Mathlib.LinearAlgebra.LinearPMap Mathlib.LinearAlgebra.Matrix.Circulant Mathlib.LinearAlgebra.Matrix.ConjTranspose Mathlib.LinearAlgebra.Matrix.DotProduct Mathlib.LinearAlgebra.Matrix.Dual Mathlib.LinearAlgebra.Matrix.Hadamard Mathlib.LinearAlgebra.Matrix.Module Mathlib.LinearAlgebra.Matrix.Notation Mathlib.LinearAlgebra.Matrix.Permanent Mathlib.LinearAlgebra.Matrix.RowCol Mathlib.LinearAlgebra.Matrix.StdBasis Mathlib.LinearAlgebra.Matrix.Symmetric Mathlib.LinearAlgebra.Matrix.ToLin Mathlib.LinearAlgebra.Matrix.Trace Mathlib.LinearAlgebra.Matrix.Unique Mathlib.LinearAlgebra.Multilinear.Basic Mathlib.LinearAlgebra.Multilinear.Basis Mathlib.LinearAlgebra.Multilinear.Curry Mathlib.LinearAlgebra.Multilinear.DFinsupp Mathlib.LinearAlgebra.Multilinear.DirectSum Mathlib.LinearAlgebra.Multilinear.Finsupp Mathlib.LinearAlgebra.Multilinear.Pi Mathlib.LinearAlgebra.Multilinear.TensorProduct Mathlib.LinearAlgebra.PiTensorProduct.Basis Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp Mathlib.LinearAlgebra.PiTensorProduct.DirectSum Mathlib.LinearAlgebra.PiTensorProduct.Finsupp Mathlib.LinearAlgebra.PiTensorProduct Mathlib.LinearAlgebra.Pi Mathlib.LinearAlgebra.Prod Mathlib.LinearAlgebra.Projection Mathlib.LinearAlgebra.Quotient.Basic Mathlib.LinearAlgebra.Quotient.Bilinear Mathlib.LinearAlgebra.Quotient.Pi Mathlib.LinearAlgebra.Ray Mathlib.LinearAlgebra.SModEq.Basic Mathlib.LinearAlgebra.SModEq.Pointwise Mathlib.LinearAlgebra.SModEq.Pow Mathlib.LinearAlgebra.SModEq Mathlib.LinearAlgebra.SesquilinearForm.Basic Mathlib.LinearAlgebra.Span.Basic Mathlib.LinearAlgebra.StdBasis Mathlib.LinearAlgebra.SymmetricAlgebra.Basic Mathlib.LinearAlgebra.TensorAlgebra.Basic Mathlib.LinearAlgebra.TensorAlgebra.Grading Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower Mathlib.LinearAlgebra.TensorPower.Basic Mathlib.LinearAlgebra.TensorPower.Pairing Mathlib.LinearAlgebra.TensorPower.Symmetric Mathlib.LinearAlgebra.TensorProduct.Associator Mathlib.LinearAlgebra.TensorProduct.Basic Mathlib.LinearAlgebra.TensorProduct.Basis Mathlib.LinearAlgebra.TensorProduct.Decomposition Mathlib.LinearAlgebra.TensorProduct.Defs Mathlib.LinearAlgebra.TensorProduct.Finiteness Mathlib.LinearAlgebra.TensorProduct.Free Mathlib.LinearAlgebra.TensorProduct.Map Mathlib.LinearAlgebra.TensorProduct.Opposite Mathlib.LinearAlgebra.TensorProduct.Pi Mathlib.LinearAlgebra.TensorProduct.Prod Mathlib.LinearAlgebra.TensorProduct.Quotient Mathlib.LinearAlgebra.TensorProduct.RightExactness Mathlib.LinearAlgebra.TensorProduct.Subalgebra Mathlib.LinearAlgebra.TensorProduct.Submodule Mathlib.LinearAlgebra.TensorProduct.Tower Mathlib.LinearAlgebra.TensorProduct.Vanishing Mathlib.Logic.Hydra Mathlib.NumberTheory.Basic Mathlib.NumberTheory.Dioph Mathlib.NumberTheory.FLT.Basic Mathlib.NumberTheory.Multiplicity Mathlib.NumberTheory.PellMatiyasevic Mathlib.NumberTheory.Zsqrtd.Basic Mathlib.NumberTheory.Zsqrtd.GaussianInt Mathlib.Order.WellFoundedSet Mathlib.RingTheory.Adjoin.Basic Mathlib.RingTheory.Adjoin.Polynomial.Basic Mathlib.RingTheory.Adjoin.Polynomial Mathlib.RingTheory.Adjoin.Singleton Mathlib.RingTheory.AlgebraTower Mathlib.RingTheory.Algebraic.Defs Mathlib.RingTheory.Algebraic.LinearIndependent Mathlib.RingTheory.Algebraic.Pi Mathlib.RingTheory.AlgebraicIndependent.Defs Mathlib.RingTheory.Bezout Mathlib.RingTheory.Bialgebra.Basic Mathlib.RingTheory.Bialgebra.Convolution Mathlib.RingTheory.Bialgebra.Equiv Mathlib.RingTheory.Bialgebra.Hom Mathlib.RingTheory.Bialgebra.MonoidAlgebra Mathlib.RingTheory.Bialgebra.SymmetricAlgebra Mathlib.RingTheory.Bialgebra.TensorProduct Mathlib.RingTheory.Coalgebra.Basic Mathlib.RingTheory.Coalgebra.CoassocSimps Mathlib.RingTheory.Coalgebra.Convolution Mathlib.RingTheory.Coalgebra.Equiv Mathlib.RingTheory.Coalgebra.Hom Mathlib.RingTheory.Coalgebra.MonoidAlgebra Mathlib.RingTheory.Coalgebra.MulOpposite Mathlib.RingTheory.Coalgebra.TensorProduct Mathlib.RingTheory.Congruence.Hom Mathlib.RingTheory.Coprime.Ideal Mathlib.RingTheory.Derivation.Basic Mathlib.RingTheory.Derivation.DifferentialRing Mathlib.RingTheory.DividedPowerAlgebra.Init Mathlib.RingTheory.DividedPowers.Basic Mathlib.RingTheory.DividedPowers.DPMorphism Mathlib.RingTheory.DividedPowers.RatAlgebra Mathlib.RingTheory.EuclideanDomain Mathlib.RingTheory.Finiteness.Basic Mathlib.RingTheory.Finiteness.Bilinear Mathlib.RingTheory.Finiteness.Defs Mathlib.RingTheory.Finiteness.Finsupp Mathlib.RingTheory.Finiteness.Ideal Mathlib.RingTheory.Finiteness.Lattice Mathlib.RingTheory.Finiteness.Nakayama Mathlib.RingTheory.Finiteness.Nilpotent Mathlib.RingTheory.Finiteness.Prod Mathlib.RingTheory.Finiteness.Subalgebra Mathlib.RingTheory.FreeCommRing Mathlib.RingTheory.GradedAlgebra.AlgHom Mathlib.RingTheory.GradedAlgebra.Basic Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring Mathlib.RingTheory.GradedAlgebra.Radical Mathlib.RingTheory.GradedAlgebra.RingHom Mathlib.RingTheory.GradedAlgebra.TensorProduct Mathlib.RingTheory.HahnSeries.Addition Mathlib.RingTheory.HahnSeries.Basic Mathlib.RingTheory.HahnSeries.HEval Mathlib.RingTheory.HahnSeries.Multiplication Mathlib.RingTheory.HahnSeries.Summable Mathlib.RingTheory.HahnSeries.Valuation Mathlib.RingTheory.HopfAlgebra.Basic Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra Mathlib.RingTheory.HopfAlgebra.TensorProduct Mathlib.RingTheory.Ideal.Basic Mathlib.RingTheory.Ideal.Basis Mathlib.RingTheory.Ideal.Colon Mathlib.RingTheory.Ideal.IdempotentFG Mathlib.RingTheory.Ideal.IsAugmentation Mathlib.RingTheory.Ideal.IsPrimary Mathlib.RingTheory.Ideal.IsPrincipal Mathlib.RingTheory.Ideal.Maps Mathlib.RingTheory.Ideal.Maximal Mathlib.RingTheory.Ideal.Nonunits Mathlib.RingTheory.Ideal.Oka Mathlib.RingTheory.Ideal.Operations Mathlib.RingTheory.Ideal.Pointwise Mathlib.RingTheory.Ideal.Prod Mathlib.RingTheory.Ideal.Quotient.PowTransition Mathlib.RingTheory.Ideal.Span Mathlib.RingTheory.Int.Basic Mathlib.RingTheory.IntegralClosure.Algebra.Defs Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs Mathlib.RingTheory.IsPrimary Mathlib.RingTheory.IsTensorProduct Mathlib.RingTheory.Jacobson.Radical Mathlib.RingTheory.LocalRing.Basic Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs Mathlib.RingTheory.Localization.Away.Basic Mathlib.RingTheory.Localization.BaseChange Mathlib.RingTheory.Localization.Basic Mathlib.RingTheory.Localization.FractionRing Mathlib.RingTheory.Localization.Module Mathlib.RingTheory.Localization.NumDen Mathlib.RingTheory.Localization.Rat Mathlib.RingTheory.MvPolynomial.FreeCommRing Mathlib.RingTheory.MvPolynomial.Symmetric.Defs Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities Mathlib.RingTheory.MvPolynomial.Tower Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous Mathlib.RingTheory.MvPowerSeries.Basic Mathlib.RingTheory.MvPowerSeries.Order Mathlib.RingTheory.MvPowerSeries.Trunc Mathlib.RingTheory.Nilpotent.Exp Mathlib.RingTheory.Nilpotent.Lemmas Mathlib.RingTheory.Noetherian.Defs Mathlib.RingTheory.Noetherian.Filter Mathlib.RingTheory.Noetherian.Nilpotent Mathlib.RingTheory.Noetherian.OfPrime Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain Mathlib.RingTheory.PiTensorProduct Mathlib.RingTheory.Polynomial.Bernstein Mathlib.RingTheory.Polynomial.Hermite.Basic Mathlib.RingTheory.Polynomial.Ideal Mathlib.RingTheory.Polynomial.Opposites Mathlib.RingTheory.Polynomial.Pochhammer Mathlib.RingTheory.Polynomial.ShiftedLegendre Mathlib.RingTheory.Polynomial.Subring Mathlib.RingTheory.Polynomial.Tower Mathlib.RingTheory.Polynomial.Wronskian Mathlib.RingTheory.PolynomialAlgebra Mathlib.RingTheory.PowerSeries.Basic Mathlib.RingTheory.PowerSeries.Catalan Mathlib.RingTheory.PowerSeries.CoeffMulMem Mathlib.RingTheory.PowerSeries.NoZeroDivisors Mathlib.RingTheory.PowerSeries.Order Mathlib.RingTheory.PowerSeries.Schroder Mathlib.RingTheory.PowerSeries.Trunc Mathlib.RingTheory.PowerSeries.WellKnown Mathlib.RingTheory.PrincipalIdealDomainOfPrime Mathlib.RingTheory.PrincipalIdealDomain Mathlib.RingTheory.QuotSMulTop Mathlib.RingTheory.Radical.NatInt Mathlib.RingTheory.Radical Mathlib.RingTheory.SimpleRing.Principal Mathlib.RingTheory.Spectrum.Maximal.Basic Mathlib.RingTheory.Spectrum.Maximal.Defs Mathlib.RingTheory.TensorProduct.Basic Mathlib.RingTheory.TensorProduct.Free Mathlib.RingTheory.TensorProduct.IsBaseChangeFree Mathlib.RingTheory.TensorProduct.IsBaseChangePi Mathlib.RingTheory.TensorProduct.IsBaseChangeRightExact Mathlib.RingTheory.TensorProduct.Maps Mathlib.RingTheory.TensorProduct.MonoidAlgebra Mathlib.RingTheory.TensorProduct.MvPolynomial Mathlib.RingTheory.TensorProduct.Pi Mathlib.RingTheory.UniqueFactorizationDomain.Ideal Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky Mathlib.RingTheory.Valuation.Basic Mathlib.RingTheory.Valuation.ExtendToLocalization Mathlib.RingTheory.Valuation.Integers Mathlib.RingTheory.Valuation.PrimeMultiplicity Mathlib.RingTheory.Valuation.ValuationRing Mathlib.RingTheory.Valuation.ValuativeRel.Basic Mathlib.RingTheory.Valuation.ValuativeRel.Trivial Mathlib.Tactic.Algebraize Mathlib.Tactic.ComputeDegree Mathlib.Tactic.Module Mathlib.Topology.Algebra.RestrictedProduct.Units Mathlib.Topology.Baire.LocallyCompactRegular Mathlib.Topology.Category.TopCat.OpenNhds Mathlib.Topology.Category.TopCat.Opens Mathlib.Topology.ClopenBox Mathlib.Topology.Compactification.OnePoint.Basic Mathlib.Topology.Constructible Mathlib.Topology.ContinuousMap.T0Sierpinski Mathlib.Topology.Convenient.OpenClosed Mathlib.Topology.Covering.Basic Mathlib.Topology.Covering Mathlib.Topology.DiscreteQuotient Mathlib.Topology.FiberBundle.Basic Mathlib.Topology.FiberBundle.Constructions Mathlib.Topology.FiberBundle.Trivialization Mathlib.Topology.FiberPartition Mathlib.Topology.Germ Mathlib.Topology.Gluing Mathlib.Topology.IsLocalHomeomorph Mathlib.Topology.JacobsonSpace Mathlib.Topology.KrullDimension Mathlib.Topology.LocalAtTarget Mathlib.Topology.LocallyConstant.Basic Mathlib.Topology.NoetherianSpace Mathlib.Topology.OpenPartialHomeomorph.Basic Mathlib.Topology.OpenPartialHomeomorph.Composition Mathlib.Topology.OpenPartialHomeomorph.Constructions Mathlib.Topology.OpenPartialHomeomorph.Continuity Mathlib.Topology.OpenPartialHomeomorph.IsImage Mathlib.Topology.OpenPartialHomeomorph Mathlib.Topology.Order.HullKernel Mathlib.Topology.QuasiSeparated Mathlib.Topology.Separation.DisjointCover Mathlib.Topology.Sets.Closeds Mathlib.Topology.Sets.CompactOpenCovered Mathlib.Topology.Sets.Compacts Mathlib.Topology.Sets.OpenCover Mathlib.Topology.Sets.Opens Mathlib.Topology.Sets.Order Mathlib.Topology.Sets.VietorisTopology Mathlib.Topology.Sheaves.Alexandrov Mathlib.Topology.Sheaves.EtaleSpace Mathlib.Topology.Sheaves.Forget Mathlib.Topology.Sheaves.Functors Mathlib.Topology.Sheaves.Limits Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Topology.Sheaves.Over Mathlib.Topology.Sheaves.PUnit Mathlib.Topology.Sheaves.Points Mathlib.Topology.Sheaves.PresheafOfFunctions Mathlib.Topology.Sheaves.Presheaf Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.Topology.Sheaves.SheafCondition.Sites Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.Topology.Sheaves.Sheaf Mathlib.Topology.Sheaves.Sheafify Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.Sheaves.Stalks Mathlib.Topology.Sober Mathlib.Topology.Spectral.Basic Mathlib.Topology.Spectral.Prespectral Mathlib.Topology.UniformSpace.Closeds |
4 |
7 filesMathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank Mathlib.Data.Nat.Nth Mathlib.Data.Nat.Prime.Nth Mathlib.Order.BooleanGenerators Mathlib.Order.CompactlyGenerated.Basic Mathlib.Order.CompactlyGenerated.Intervals |
5 |
Mathlib.Order.JordanHolder |
6 |
7 filesMathlib.CategoryTheory.Noetherian Mathlib.CategoryTheory.Subobject.ArtinianObject Mathlib.CategoryTheory.Subobject.NoetherianObject Mathlib.Order.KrullDimension Mathlib.Order.OrderIsoNat Mathlib.Order.RelSeries Mathlib.Order.WellQuasiOrder |
7 |
Declarations diff
+ WellFoundedOn.finite_of_wellFoundedOn_swap
+ _root_.IsWellOrder.finite_of_isWellOrder_of_isWellOrder_swap
+ finite_iff_empty_relEmbedding_of_isWellOrder
+ finite_iff_isEmpty_relEmbedding_lt_and_isEmpty_relEmbedding_gt
+ infinite_iff_nonempty_relEmbedding_lt_or_nonempty_relEmbedding_gt
+ infinite_iff_nonempty_relEmbedding_of_isWellOrder
+ instance (priority := low) _root_.instFiniteOfWellFoundedLTOfWellFoundedGT
+ subtype_iff
+ subtype_iff'
You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.
No changes to strong technical debt.
No changes to weak technical debt.
3 tasks
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
Hagb
marked this pull request as ready for review
May 24, 2026 17:57
mathlib-merge-conflicts
Bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
github-actions
Bot
removed
the
merge-conflict
mathlib-merge-conflicts
Bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
It is a corollary of #39545 on
WellFoundedOn.It was a lemmas for #39781, which has been closed since there would be a better proof.
((· < ·) : ℕ → ℕ → Prop) ↪r r#39545WellFoundedon subtype iff the relation restricted on the subtype isWellFounded#39774