chore: adaptations for nightly-2025-05-01

[kim-em]

No description provided.

[github-actions]

PR summary 1b64f60681

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Data.UInt	-483
Mathlib.Algebra.Expr	-40
Mathlib.Tactic.ExtractLets	-39
Mathlib.Data.Num.Basic	-36
Mathlib.Data.Tree.Get Mathlib.Tactic.LiftLets	-34
Mathlib.Algebra.NeZero	-29
Mathlib.Algebra.Order.ZeroLEOne	-23
Mathlib.Data.PNat.Defs Mathlib.Testing.Plausible.Sampleable	-20
9 files Mathlib.Data.PNat.Equiv Mathlib.Data.Set.Insert Mathlib.Data.Set.Subsingleton Mathlib.Logic.Function.FiberPartition Mathlib.Order.Bounded Mathlib.Order.Filter.Defs Mathlib.Order.Interval.Set.Basic Mathlib.Order.Interval.Set.LinearOrder Mathlib.SetTheory.PGame.Basic	-16
191 files Mathlib.Algebra.Order.Nonneg.Lattice Mathlib.Combinatorics.Quiver.Arborescence Mathlib.Combinatorics.SetFamily.Intersecting Mathlib.Control.EquivFunctor.Instances Mathlib.Control.Functor.Multivariate Mathlib.Data.Bool.Set Mathlib.Data.Countable.Small Mathlib.Data.Fin.Basic Mathlib.Data.Fin.Fin2 Mathlib.Data.Fin.FlagRange Mathlib.Data.Fin.Rev Mathlib.Data.Fin.SuccPred Mathlib.Data.Fin.Tuple.Basic Mathlib.Data.Fin.Tuple.Curry Mathlib.Data.Fin.Tuple.Take Mathlib.Data.Fin.VecNotation Mathlib.Data.Finite.Set Mathlib.Data.Finset.Attach Mathlib.Data.Finset.Basic Mathlib.Data.Finset.BooleanAlgebra Mathlib.Data.Finset.Card Mathlib.Data.Finset.Dedup Mathlib.Data.Finset.Defs Mathlib.Data.Finset.Disjoint Mathlib.Data.Finset.Empty Mathlib.Data.Finset.Erase Mathlib.Data.Finset.Filter Mathlib.Data.Finset.Fin Mathlib.Data.Finset.Fold Mathlib.Data.Finset.Image Mathlib.Data.Finset.Insert Mathlib.Data.Finset.Lattice.Basic Mathlib.Data.Finset.Lattice.Lemmas Mathlib.Data.Finset.Order Mathlib.Data.Finset.Piecewise Mathlib.Data.Finset.Range Mathlib.Data.Finset.SDiff Mathlib.Data.Finset.SymmDiff Mathlib.Data.Fintype.Basic Mathlib.Data.Fintype.Card Mathlib.Data.Fintype.Defs Mathlib.Data.Fintype.EquivFin Mathlib.Data.Fintype.Inv Mathlib.Data.Fintype.OfMap Mathlib.Data.Fintype.Sets Mathlib.Data.Fintype.Shrink Mathlib.Data.List.ChainOfFn Mathlib.Data.List.FinRange Mathlib.Data.List.Lemmas Mathlib.Data.List.NodupEquivFin Mathlib.Data.List.OfFn Mathlib.Data.List.Permutation Mathlib.Data.List.Sort Mathlib.Data.List.Sublists Mathlib.Data.MLList.BestFirst Mathlib.Data.Multiset.Dedup Mathlib.Data.Multiset.Filter Mathlib.Data.Multiset.FinsetOps Mathlib.Data.Multiset.Fold Mathlib.Data.Multiset.Lattice Mathlib.Data.Multiset.MapFold Mathlib.Data.Multiset.NatAntidiagonal Mathlib.Data.Multiset.Range Mathlib.Data.Multiset.Sort Mathlib.Data.Multiset.UnionInter Mathlib.Data.Nat.Set Mathlib.Data.Prod.TProd Mathlib.Data.Rel Mathlib.Data.Semiquot Mathlib.Data.Set.Accumulate Mathlib.Data.Set.BooleanAlgebra Mathlib.Data.Set.Constructions Mathlib.Data.Set.Finite.Basic Mathlib.Data.Set.Finite.Range Mathlib.Data.Set.Function Mathlib.Data.Set.Functor Mathlib.Data.Set.Image Mathlib.Data.Set.Lattice.Image Mathlib.Data.Set.Lattice Mathlib.Data.Set.List Mathlib.Data.Set.Monotone Mathlib.Data.Set.NAry Mathlib.Data.Set.Pairwise.Basic Mathlib.Data.Set.Pairwise.Lattice Mathlib.Data.Set.Pairwise.List Mathlib.Data.Set.Piecewise Mathlib.Data.Set.Prod Mathlib.Data.Set.Restrict Mathlib.Data.Set.Sigma Mathlib.Data.Set.Subset Mathlib.Data.Set.UnionLift Mathlib.Data.Setoid.Basic Mathlib.Data.TypeVec Mathlib.Data.Vector3 Mathlib.Logic.Embedding.Set Mathlib.Logic.Equiv.Embedding Mathlib.Logic.Equiv.Fin.Basic Mathlib.Logic.Equiv.Fintype Mathlib.Logic.Equiv.PartialEquiv Mathlib.Logic.Equiv.Set Mathlib.Logic.Function.DependsOn Mathlib.Logic.Function.FromTypes Mathlib.Logic.Function.OfArity Mathlib.Logic.Small.Basic Mathlib.Logic.Small.Set Mathlib.Order.Atoms Mathlib.Order.Bounds.Basic Mathlib.Order.Bounds.Image Mathlib.Order.Bounds.Lattice Mathlib.Order.Bounds.OrderIso Mathlib.Order.Closure Mathlib.Order.Cofinal Mathlib.Order.CompleteBooleanAlgebra Mathlib.Order.CompleteLattice.Basic Mathlib.Order.CompleteLattice.Defs Mathlib.Order.CompleteLattice.Lemmas Mathlib.Order.CompleteLatticeIntervals Mathlib.Order.Concept Mathlib.Order.ConditionallyCompleteLattice.Basic Mathlib.Order.ConditionallyCompleteLattice.Defs Mathlib.Order.ConditionallyCompleteLattice.Indexed Mathlib.Order.Copy Mathlib.Order.Cover Mathlib.Order.DirectedInverseSystem Mathlib.Order.Directed Mathlib.Order.Fin.Basic Mathlib.Order.Fin.Finset Mathlib.Order.Fin.SuccAboveOrderIso Mathlib.Order.Fin.Tuple Mathlib.Order.GaloisConnection.Basic Mathlib.Order.Heyting.Regular Mathlib.Order.Hom.CompleteLattice Mathlib.Order.Hom.Order Mathlib.Order.Hom.Set Mathlib.Order.InitialSeg Mathlib.Order.Interval.Basic Mathlib.Order.Interval.Set.Disjoint Mathlib.Order.Interval.Set.Fin Mathlib.Order.Interval.Set.Image Mathlib.Order.Interval.Set.Infinite Mathlib.Order.Interval.Set.InitialSeg Mathlib.Order.Interval.Set.Limit Mathlib.Order.Interval.Set.Monotone Mathlib.Order.Interval.Set.OrdConnectedComponent Mathlib.Order.Interval.Set.OrdConnected Mathlib.Order.Interval.Set.OrderEmbedding Mathlib.Order.Interval.Set.OrderIso Mathlib.Order.Interval.Set.ProjIcc Mathlib.Order.Interval.Set.SuccOrder Mathlib.Order.Interval.Set.SuccPred Mathlib.Order.Interval.Set.SurjOn Mathlib.Order.Interval.Set.Union Mathlib.Order.Interval.Set.UnorderedInterval Mathlib.Order.Interval.Set.WithBotTop Mathlib.Order.IsNormal Mathlib.Order.LatticeIntervals Mathlib.Order.ModularLattice Mathlib.Order.Monotone.Extension Mathlib.Order.Monotone.Union Mathlib.Order.Nucleus Mathlib.Order.OrdContinuous Mathlib.Order.PiLex Mathlib.Order.Radical Mathlib.Order.Rel.GaloisConnection Mathlib.Order.RelIso.Set Mathlib.Order.ScottContinuity Mathlib.Order.Set Mathlib.Order.Shrink Mathlib.Order.SuccPred.Archimedean Mathlib.Order.SuccPred.Basic Mathlib.Order.SuccPred.CompleteLinearOrder Mathlib.Order.SuccPred.InitialSeg Mathlib.Order.SuccPred.IntervalSucc Mathlib.Order.SuccPred.Limit Mathlib.Order.SuccPred.Relation Mathlib.Order.SuccPred.Tree Mathlib.Order.SuccPred.WithBot Mathlib.Order.TransfiniteIteration Mathlib.Order.UpperLower.Basic Mathlib.Order.UpperLower.Closure Mathlib.Order.UpperLower.CompleteLattice Mathlib.Order.UpperLower.Fibration Mathlib.Order.UpperLower.Hom Mathlib.Order.UpperLower.Principal Mathlib.Order.UpperLower.Prod Mathlib.Order.WellFounded Mathlib.Order.ZornAtoms Mathlib.SetTheory.Cardinal.Defs Mathlib.SetTheory.ZFC.Basic Mathlib.SetTheory.ZFC.PSet Mathlib.Tactic.FinCases	-15
19 files Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations Mathlib.AlgebraicTopology.SimplexCategory.Defs Mathlib.CategoryTheory.FinCategory.AsType Mathlib.CategoryTheory.FinCategory.Basic Mathlib.CategoryTheory.MorphismProperty.Basic Mathlib.CategoryTheory.MorphismProperty.Composition Mathlib.CategoryTheory.MorphismProperty.Factorization Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy Mathlib.CategoryTheory.MorphismProperty.IsSmall Mathlib.CategoryTheory.MorphismProperty.Retract Mathlib.CategoryTheory.PathCategory.MorphismProperty Mathlib.CategoryTheory.Widesubcategory Mathlib.Order.Antichain Mathlib.Order.Chain Mathlib.Order.CompleteLattice.Chain Mathlib.Order.Extension.Linear Mathlib.Order.Minimal Mathlib.Order.Preorder.Chain Mathlib.Order.Zorn	-14
Mathlib.Data.Seq.Computation Mathlib.Data.Stream.Init	-12
Mathlib.Algebra.GCDMonoid.Nat	-11
Mathlib.Data.Int.GCD	-6
Mathlib.Control.LawfulFix	-5
3 files Mathlib.Algebra.Group.WithOne.Basic Mathlib.Data.Set.Enumerate Mathlib.Tactic.NormNum.GCD	-3
111 files Mathlib.Algebra.Algebra.Spectrum.Basic Mathlib.Algebra.Algebra.Spectrum.Pi Mathlib.Algebra.Algebra.Spectrum.Quasispectrum Mathlib.Algebra.Algebra.Subalgebra.Operations Mathlib.Algebra.CharP.Invertible Mathlib.Algebra.CubicDiscriminant Mathlib.Algebra.Divisibility.Basic Mathlib.Algebra.Divisibility.Hom Mathlib.Algebra.Divisibility.Units Mathlib.Algebra.Field.Equiv Mathlib.Algebra.Group.WithOne.Defs Mathlib.Algebra.MvPolynomial.SchwartzZippel Mathlib.Algebra.Polynomial.Degree.CardPowDegree Mathlib.Algebra.Polynomial.Derivation Mathlib.Algebra.Polynomial.FieldDivision Mathlib.Algebra.Polynomial.Laurent Mathlib.Algebra.Polynomial.Module.AEval Mathlib.Algebra.Polynomial.Module.Basic Mathlib.Algebra.Polynomial.PartialFractions Mathlib.Algebra.Polynomial.Roots Mathlib.Algebra.Polynomial.SpecificDegree Mathlib.Algebra.Polynomial.Splits Mathlib.Algebra.Star.Unitary Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology Mathlib.CategoryTheory.Adjunction.FullyFaithful Mathlib.CategoryTheory.Adjunction.Reflective Mathlib.CategoryTheory.Adjunction.Triple Mathlib.CategoryTheory.Bicategory.SingleObj Mathlib.CategoryTheory.Category.Pairwise Mathlib.CategoryTheory.Category.RelCat Mathlib.CategoryTheory.Groupoid.VertexGroup Mathlib.CategoryTheory.Limits.Bicones Mathlib.CategoryTheory.Limits.Shapes.Preorder.Fin Mathlib.CategoryTheory.Limits.Shapes.Preorder.PrincipalSeg Mathlib.CategoryTheory.Monad.Adjunction Mathlib.CategoryTheory.Monoidal.End Mathlib.CategoryTheory.Monoidal.Free.Basic Mathlib.CategoryTheory.Monoidal.Free.Coherence Mathlib.CategoryTheory.Monoidal.Functor Mathlib.CategoryTheory.Monoidal.NaturalTransformation Mathlib.CategoryTheory.Monoidal.Transport Mathlib.CategoryTheory.MorphismProperty.Concrete Mathlib.CategoryTheory.SmallObject.WellOrderInductionData Mathlib.CategoryTheory.Subpresheaf.Basic Mathlib.Combinatorics.Nullstellensatz Mathlib.Data.Int.Sqrt Mathlib.Data.Nat.Factorial.NatCast Mathlib.Data.Rat.Defs Mathlib.Dynamics.PeriodicPts.Lemmas Mathlib.FieldTheory.RatFunc.Basic Mathlib.LinearAlgebra.AffineSpace.MidpointZero Mathlib.LinearAlgebra.AffineSpace.Ordered Mathlib.NumberTheory.FLT.Basic Mathlib.NumberTheory.FLT.MasonStothers Mathlib.NumberTheory.Zsqrtd.Basic Mathlib.NumberTheory.Zsqrtd.GaussianInt Mathlib.RingTheory.Algebraic.Cardinality Mathlib.RingTheory.AlgebraicIndependent.Basic Mathlib.RingTheory.Bezout Mathlib.RingTheory.Bialgebra.MonoidAlgebra Mathlib.RingTheory.Coalgebra.MonoidAlgebra Mathlib.RingTheory.Coprime.Ideal Mathlib.RingTheory.Coprime.Lemmas Mathlib.RingTheory.DividedPowers.Basic Mathlib.RingTheory.DividedPowers.DPMorphism Mathlib.RingTheory.EuclideanDomain Mathlib.RingTheory.Finiteness.Nakayama Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal Mathlib.RingTheory.GradedAlgebra.Radical Mathlib.RingTheory.HahnSeries.Valuation Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra Mathlib.RingTheory.Ideal.Colon Mathlib.RingTheory.Ideal.IdempotentFG Mathlib.RingTheory.Ideal.IsPrincipal Mathlib.RingTheory.Ideal.Maps Mathlib.RingTheory.Ideal.Operations Mathlib.RingTheory.Ideal.Pointwise Mathlib.RingTheory.Ideal.Prod Mathlib.RingTheory.Int.Basic Mathlib.RingTheory.Localization.Away.Basic Mathlib.RingTheory.MvPolynomial.EulerIdentity Mathlib.RingTheory.MvPolynomial.Groebner Mathlib.RingTheory.MvPolynomial.Homogeneous Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex Mathlib.RingTheory.MvPolynomial.MonomialOrder Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain Mathlib.RingTheory.Polynomial.Content Mathlib.RingTheory.Polynomial.HilbertPoly Mathlib.RingTheory.Polynomial.Ideal Mathlib.RingTheory.Polynomial.Radical Mathlib.RingTheory.Polynomial.SmallDegreeVieta Mathlib.RingTheory.Polynomial.Vieta Mathlib.RingTheory.PowerSeries.NoZeroDivisors Mathlib.RingTheory.PrincipalIdealDomainOfPrime Mathlib.RingTheory.PrincipalIdealDomain Mathlib.RingTheory.UniqueFactorizationDomain.Ideal Mathlib.RingTheory.Valuation.Archimedean Mathlib.RingTheory.Valuation.Basic Mathlib.RingTheory.Valuation.Discrete.Basic Mathlib.RingTheory.Valuation.ExtendToLocalization Mathlib.RingTheory.Valuation.Integers Mathlib.RingTheory.Valuation.PrimeMultiplicity Mathlib.RingTheory.Valuation.RankOne Mathlib.RingTheory.Valuation.ValExtension Mathlib.RingTheory.Valuation.ValuationRing Mathlib.Tactic.NormNum.IsCoprime Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology	-2
2195 files Mathlib.Algebra.AddConstMap.Basic Mathlib.Algebra.AddConstMap.Equiv Mathlib.Algebra.AddTorsor.Basic Mathlib.Algebra.Algebra.Basic Mathlib.Algebra.Algebra.Bilinear Mathlib.Algebra.Algebra.Defs Mathlib.Algebra.Algebra.Equiv Mathlib.Algebra.Algebra.Field Mathlib.Algebra.Algebra.Hom.Rat Mathlib.Algebra.Algebra.Hom Mathlib.Algebra.Algebra.NonUnitalHom Mathlib.Algebra.Algebra.NonUnitalSubalgebra Mathlib.Algebra.Algebra.Operations Mathlib.Algebra.Algebra.Opposite Mathlib.Algebra.Algebra.Pi Mathlib.Algebra.Algebra.Prod Mathlib.Algebra.Algebra.Rat Mathlib.Algebra.Algebra.RestrictScalars Mathlib.Algebra.Algebra.Subalgebra.Basic Mathlib.Algebra.Algebra.Subalgebra.Centralizer Mathlib.Algebra.Algebra.Subalgebra.Directed Mathlib.Algebra.Algebra.Subalgebra.Lattice Mathlib.Algebra.Algebra.Subalgebra.MulOpposite 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.Basic Mathlib.Algebra.Azumaya.Defs Mathlib.Algebra.Azumaya.Matrix Mathlib.Algebra.BigOperators.Associated Mathlib.Algebra.BigOperators.Balance Mathlib.Algebra.BigOperators.Expect Mathlib.Algebra.BigOperators.Field Mathlib.Algebra.BigOperators.Fin Mathlib.Algebra.BigOperators.Finprod Mathlib.Algebra.BigOperators.Finsupp.Basic Mathlib.Algebra.BigOperators.Finsupp.Fin Mathlib.Algebra.BigOperators.Group.Finset.Basic Mathlib.Algebra.BigOperators.Group.Finset.Defs Mathlib.Algebra.BigOperators.Group.Finset.Indicator Mathlib.Algebra.BigOperators.Group.Finset.Lemmas Mathlib.Algebra.BigOperators.Group.Finset.Pi Mathlib.Algebra.BigOperators.Group.Finset.Piecewise Mathlib.Algebra.BigOperators.Group.Finset.Powerset Mathlib.Algebra.BigOperators.Group.Finset.Preimage Mathlib.Algebra.BigOperators.Group.Finset.Sigma Mathlib.Algebra.BigOperators.Group.List.Basic Mathlib.Algebra.BigOperators.Group.List.Lemmas Mathlib.Algebra.BigOperators.Group.Multiset.Basic Mathlib.Algebra.BigOperators.Group.Multiset.Defs Mathlib.Algebra.BigOperators.GroupWithZero.Action Mathlib.Algebra.BigOperators.GroupWithZero.Finset Mathlib.Algebra.BigOperators.Intervals Mathlib.Algebra.BigOperators.Module Mathlib.Algebra.BigOperators.NatAntidiagonal Mathlib.Algebra.BigOperators.Option Mathlib.Algebra.BigOperators.Pi Mathlib.Algebra.BigOperators.Ring.Finset Mathlib.Algebra.BigOperators.Ring.List Mathlib.Algebra.BigOperators.Ring.Multiset Mathlib.Algebra.BigOperators.Ring.Nat Mathlib.Algebra.BigOperators.RingEquiv Mathlib.Algebra.BigOperators.Sym Mathlib.Algebra.BigOperators.WithTop Mathlib.Algebra.Category.Grp.Basic Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup Mathlib.Algebra.Category.Grp.FiniteGrp Mathlib.Algebra.Category.Grp.ForgetCorepresentable Mathlib.Algebra.Category.GrpWithZero Mathlib.Algebra.Category.MonCat.Adjunctions Mathlib.Algebra.Category.MonCat.Basic Mathlib.Algebra.Category.MonCat.ForgetCorepresentable Mathlib.Algebra.Category.Ring.Basic Mathlib.Algebra.Category.Semigrp.Basic Mathlib.Algebra.Central.Basic Mathlib.Algebra.Central.Defs Mathlib.Algebra.Central.Matrix Mathlib.Algebra.CharP.Algebra Mathlib.Algebra.CharP.Defs Mathlib.Algebra.CharP.Frobenius Mathlib.Algebra.CharP.IntermediateField Mathlib.Algebra.CharP.Lemmas Mathlib.Algebra.CharP.Pi Mathlib.Algebra.CharP.Reduced Mathlib.Algebra.CharP.Subring Mathlib.Algebra.CharZero.Infinite Mathlib.Algebra.CharZero.Quotient Mathlib.Algebra.Colimit.DirectLimit Mathlib.Algebra.Colimit.Finiteness Mathlib.Algebra.Colimit.Module Mathlib.Algebra.Colimit.TensorProduct Mathlib.Algebra.ContinuedFractions.Basic Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries Mathlib.Algebra.ContinuedFractions.Computation.Approximations Mathlib.Algebra.ContinuedFractions.Computation.Basic Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat Mathlib.Algebra.ContinuedFractions.Computation.Translations Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv Mathlib.Algebra.ContinuedFractions.Determinant Mathlib.Algebra.ContinuedFractions.TerminatedStable Mathlib.Algebra.ContinuedFractions.Translations Mathlib.Algebra.DirectSum.AddChar Mathlib.Algebra.DirectSum.Algebra Mathlib.Algebra.DirectSum.Basic Mathlib.Algebra.DirectSum.Decomposition Mathlib.Algebra.DirectSum.Finsupp Mathlib.Algebra.DirectSum.Internal Mathlib.Algebra.DirectSum.Module Mathlib.Algebra.DirectSum.Ring Mathlib.Algebra.Divisibility.Finite Mathlib.Algebra.Divisibility.Prod Mathlib.Algebra.DualNumber Mathlib.Algebra.Equiv.TransferInstance Mathlib.Algebra.EuclideanDomain.Basic Mathlib.Algebra.Field.Action.ConjAct Mathlib.Algebra.Field.IsField Mathlib.Algebra.Field.MinimalAxioms Mathlib.Algebra.Field.Opposite Mathlib.Algebra.Field.Power Mathlib.Algebra.Field.Rat Mathlib.Algebra.Field.Subfield.Basic Mathlib.Algebra.Field.Subfield.Defs Mathlib.Algebra.FreeAlgebra Mathlib.Algebra.FreeMonoid.Basic Mathlib.Algebra.FreeMonoid.Count Mathlib.Algebra.FreeMonoid.Symbols Mathlib.Algebra.FreeMonoid.UniqueProds Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra Mathlib.Algebra.Free Mathlib.Algebra.GCDMonoid.Basic Mathlib.Algebra.GCDMonoid.Finset Mathlib.Algebra.GCDMonoid.Multiset Mathlib.Algebra.GCDMonoid.PUnit Mathlib.Algebra.GeomSum Mathlib.Algebra.GradedMonoid Mathlib.Algebra.GradedMulAction Mathlib.Algebra.Group.Action.Basic Mathlib.Algebra.Group.Action.End Mathlib.Algebra.Group.Action.Equidecomp Mathlib.Algebra.Group.Action.Pointwise.Finset Mathlib.Algebra.Group.Action.Pointwise.Set.Finite Mathlib.Algebra.Group.Action.Units Mathlib.Algebra.Group.AddChar Mathlib.Algebra.Group.Basic Mathlib.Algebra.Group.Commute.Basic Mathlib.Algebra.Group.Commute.Units Mathlib.Algebra.Group.Conj Mathlib.Algebra.Group.End Mathlib.Algebra.Group.Equiv.Basic Mathlib.Algebra.Group.Equiv.Finite Mathlib.Algebra.Group.EvenFunction Mathlib.Algebra.Group.Fin.Basic Mathlib.Algebra.Group.Fin.Tuple Mathlib.Algebra.Group.FiniteSupport Mathlib.Algebra.Group.ForwardDiff Mathlib.Algebra.Group.Graph Mathlib.Algebra.Group.Hom.Basic Mathlib.Algebra.Group.Hom.End Mathlib.Algebra.Group.Hom.Instances Mathlib.Algebra.Group.Int.Even Mathlib.Algebra.Group.Int.Units Mathlib.Algebra.Group.Invertible.Basic Mathlib.Algebra.Group.Nat.Range Mathlib.Algebra.Group.NatPowAssoc Mathlib.Algebra.Group.PNatPowAssoc Mathlib.Algebra.Group.Pointwise.Finset.Basic Mathlib.Algebra.Group.Pointwise.Finset.BigOperators Mathlib.Algebra.Group.Pointwise.Finset.Density Mathlib.Algebra.Group.Pointwise.Finset.Interval Mathlib.Algebra.Group.Pointwise.Finset.Scalar Mathlib.Algebra.Group.Pointwise.Set.BigOperators Mathlib.Algebra.Group.Pointwise.Set.Finite Mathlib.Algebra.Group.Pointwise.Set.ListOfFn Mathlib.Algebra.Group.Semiconj.Basic Mathlib.Algebra.Group.Semiconj.Units Mathlib.Algebra.Group.Subgroup.Actions Mathlib.Algebra.Group.Subgroup.Basic Mathlib.Algebra.Group.Subgroup.Defs Mathlib.Algebra.Group.Subgroup.Even Mathlib.Algebra.Group.Subgroup.Finsupp Mathlib.Algebra.Group.Subgroup.Ker Mathlib.Algebra.Group.Subgroup.Lattice Mathlib.Algebra.Group.Subgroup.Map Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas Mathlib.Algebra.Group.Subgroup.MulOpposite Mathlib.Algebra.Group.Subgroup.Order Mathlib.Algebra.Group.Subgroup.Pointwise Mathlib.Algebra.Group.Subgroup.ZPowers.Basic Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas Mathlib.Algebra.Group.Submonoid.BigOperators Mathlib.Algebra.Group.Submonoid.Finsupp Mathlib.Algebra.Group.Submonoid.Membership Mathlib.Algebra.Group.Submonoid.Pointwise Mathlib.Algebra.Group.Submonoid.Units Mathlib.Algebra.Group.Translate Mathlib.Algebra.Group.TypeTags.Finite Mathlib.Algebra.Group.UniqueProds.Basic Mathlib.Algebra.Group.Units.Basic Mathlib.Algebra.Group.Units.Equiv Mathlib.Algebra.Group.Units.Hom Mathlib.Algebra.GroupWithZero.Action.Basic Mathlib.Algebra.GroupWithZero.Action.Center Mathlib.Algebra.GroupWithZero.Action.ConjAct Mathlib.Algebra.GroupWithZero.Action.Pi Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set Mathlib.Algebra.GroupWithZero.Associated Mathlib.Algebra.GroupWithZero.Basic Mathlib.Algebra.GroupWithZero.Conj Mathlib.Algebra.GroupWithZero.Divisibility Mathlib.Algebra.GroupWithZero.Equiv Mathlib.Algebra.GroupWithZero.Hom Mathlib.Algebra.GroupWithZero.Int Mathlib.Algebra.GroupWithZero.NonZeroDivisors Mathlib.Algebra.GroupWithZero.Pointwise.Finset Mathlib.Algebra.GroupWithZero.Subgroup Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise Mathlib.Algebra.GroupWithZero.Submonoid.Primal Mathlib.Algebra.GroupWithZero.WithZero Mathlib.Algebra.IsPrimePow Mathlib.Algebra.Lie.Basic Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra Mathlib.Algebra.ModEq Mathlib.Algebra.Module.Basic Mathlib.Algebra.Module.BigOperators Mathlib.Algebra.Module.Bimodule Mathlib.Algebra.Module.Card Mathlib.Algebra.Module.End Mathlib.Algebra.Module.Equiv.Basic Mathlib.Algebra.Module.Equiv.Defs Mathlib.Algebra.Module.Equiv.Opposite Mathlib.Algebra.Module.GradedModule Mathlib.Algebra.Module.Hom Mathlib.Algebra.Module.Injective Mathlib.Algebra.Module.LinearMap.Basic Mathlib.Algebra.Module.LinearMap.Defs Mathlib.Algebra.Module.LinearMap.End Mathlib.Algebra.Module.LinearMap.Prod Mathlib.Algebra.Module.LinearMap.Rat Mathlib.Algebra.Module.LinearMap.Star Mathlib.Algebra.Module.LocalizedModule.AtPrime Mathlib.Algebra.Module.LocalizedModule.Away Mathlib.Algebra.Module.LocalizedModule.Basic Mathlib.Algebra.Module.LocalizedModule.Int Mathlib.Algebra.Module.LocalizedModule.IsLocalization Mathlib.Algebra.Module.NatInt Mathlib.Algebra.Module.Pi Mathlib.Algebra.Module.Projective Mathlib.Algebra.Module.Rat Mathlib.Algebra.Module.Submodule.Basic Mathlib.Algebra.Module.Submodule.Bilinear Mathlib.Algebra.Module.Submodule.Defs Mathlib.Algebra.Module.Submodule.EqLocus Mathlib.Algebra.Module.Submodule.Equiv Mathlib.Algebra.Module.Submodule.Invariant Mathlib.Algebra.Module.Submodule.IterateMapComap Mathlib.Algebra.Module.Submodule.Ker Mathlib.Algebra.Module.Submodule.Lattice Mathlib.Algebra.Module.Submodule.LinearMap Mathlib.Algebra.Module.Submodule.Map Mathlib.Algebra.Module.Submodule.Order Mathlib.Algebra.Module.Submodule.Pointwise Mathlib.Algebra.Module.Submodule.Range Mathlib.Algebra.Module.Submodule.RestrictScalars Mathlib.Algebra.Module.ULift Mathlib.Algebra.MonoidAlgebra.Basic Mathlib.Algebra.MonoidAlgebra.Defs Mathlib.Algebra.MonoidAlgebra.Degree Mathlib.Algebra.MonoidAlgebra.Division Mathlib.Algebra.MonoidAlgebra.Grading Mathlib.Algebra.MonoidAlgebra.Ideal Mathlib.Algebra.MonoidAlgebra.MapDomain Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors Mathlib.Algebra.MonoidAlgebra.Support Mathlib.Algebra.MonoidAlgebra.ToDirectSum Mathlib.Algebra.MvPolynomial.Basic Mathlib.Algebra.MvPolynomial.Cardinal 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.Expand 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.NoZeroSMulDivisors.Basic Mathlib.Algebra.Notation.Lemmas Mathlib.Algebra.Order.AbsoluteValue.Basic Mathlib.Algebra.Order.AbsoluteValue.Euclidean Mathlib.Algebra.Order.Algebra Mathlib.Algebra.Order.Antidiag.Finsupp Mathlib.Algebra.Order.Antidiag.Nat Mathlib.Algebra.Order.Antidiag.Pi Mathlib.Algebra.Order.Antidiag.Prod Mathlib.Algebra.Order.Archimedean.Basic Mathlib.Algebra.Order.Archimedean.Hom Mathlib.Algebra.Order.Archimedean.Submonoid Mathlib.Algebra.Order.BigOperators.Expect Mathlib.Algebra.Order.BigOperators.Group.Finset Mathlib.Algebra.Order.BigOperators.Group.List Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite Mathlib.Algebra.Order.BigOperators.Group.Multiset Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset Mathlib.Algebra.Order.BigOperators.Ring.Finset Mathlib.Algebra.Order.BigOperators.Ring.List Mathlib.Algebra.Order.BigOperators.Ring.Multiset Mathlib.Algebra.Order.CauSeq.Basic Mathlib.Algebra.Order.CauSeq.BigOperators Mathlib.Algebra.Order.CauSeq.Completion Mathlib.Algebra.Order.CompleteField Mathlib.Algebra.Order.Disjointed Mathlib.Algebra.Order.Field.Basic Mathlib.Algebra.Order.Field.Canonical Mathlib.Algebra.Order.Field.Pi Mathlib.Algebra.Order.Field.Power Mathlib.Algebra.Order.Field.Rat Mathlib.Algebra.Order.Field.Subfield Mathlib.Algebra.Order.Floor.Defs Mathlib.Algebra.Order.Floor.Div Mathlib.Algebra.Order.Floor.Ring Mathlib.Algebra.Order.Floor.Semiring Mathlib.Algebra.Order.Floor Mathlib.Algebra.Order.Group.Finset Mathlib.Algebra.Order.Group.Int.Sum Mathlib.Algebra.Order.Group.Multiset Mathlib.Algebra.Order.Group.PiLex Mathlib.Algebra.Order.Group.Pointwise.Interval Mathlib.Algebra.Order.GroupWithZero.Action.Synonym Mathlib.Algebra.Order.GroupWithZero.Canonical Mathlib.Algebra.Order.GroupWithZero.Finset Mathlib.Algebra.Order.GroupWithZero.Unbundled.Defs Mathlib.Algebra.Order.GroupWithZero.WithZero Mathlib.Algebra.Order.Hom.Basic Mathlib.Algebra.Order.Hom.Monoid Mathlib.Algebra.Order.Hom.Ring Mathlib.Algebra.Order.Interval.Basic Mathlib.Algebra.Order.Interval.Finset.Basic Mathlib.Algebra.Order.Interval.Finset.SuccPred Mathlib.Algebra.Order.Interval.Multiset Mathlib.Algebra.Order.Interval.Set.SuccPred Mathlib.Algebra.Order.Invertible Mathlib.Algebra.Order.Module.Algebra Mathlib.Algebra.Order.Module.Defs Mathlib.Algebra.Order.Module.OrderedSMul Mathlib.Algebra.Order.Module.Pointwise Mathlib.Algebra.Order.Module.PositiveLinearMap Mathlib.Algebra.Order.Module.Rat Mathlib.Algebra.Order.Module.Synonym Mathlib.Algebra.Order.Monoid.Associated Mathlib.Algebra.Order.Monoid.Canonical.Basic Mathlib.Algebra.Order.Monoid.ToMulBot Mathlib.Algebra.Order.Monoid.Unbundled.Defs Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual Mathlib.Algebra.Order.Monovary Mathlib.Algebra.Order.Nonneg.Basic Mathlib.Algebra.Order.Nonneg.Field Mathlib.Algebra.Order.Nonneg.Floor Mathlib.Algebra.Order.Nonneg.Module Mathlib.Algebra.Order.Nonneg.Ring Mathlib.Algebra.Order.PartialSups Mathlib.Algebra.Order.Rearrangement Mathlib.Algebra.Order.Ring.Abs Mathlib.Algebra.Order.Ring.Basic Mathlib.Algebra.Order.Ring.Canonical Mathlib.Algebra.Order.Ring.Cast Mathlib.Algebra.Order.Ring.Finset Mathlib.Algebra.Order.Ring.Int Mathlib.Algebra.Order.Ring.IsNonarchimedean Mathlib.Algebra.Order.Ring.Nat Mathlib.Algebra.Order.Ring.Pow Mathlib.Algebra.Order.Ring.Rat Mathlib.Algebra.Order.Ring.Star Mathlib.Algebra.Order.Ring.Unbundled.Rat Mathlib.Algebra.Order.Ring.WithTop Mathlib.Algebra.Order.Round Mathlib.Algebra.Order.Star.Basic Mathlib.Algebra.Order.Star.Conjneg Mathlib.Algebra.Order.Star.Prod Mathlib.Algebra.Order.SuccPred.TypeTags Mathlib.Algebra.Order.SuccPred.WithBot Mathlib.Algebra.Order.SuccPred Mathlib.Algebra.Order.UpperLower Mathlib.Algebra.Order.WithTop.Untop0 Mathlib.Algebra.Pointwise.Stabilizer Mathlib.Algebra.Polynomial.AlgebraMap Mathlib.Algebra.Polynomial.Basic Mathlib.Algebra.Polynomial.Basis Mathlib.Algebra.Polynomial.BigOperators Mathlib.Algebra.Polynomial.CancelLeads Mathlib.Algebra.Polynomial.Cardinal Mathlib.Algebra.Polynomial.CoeffList Mathlib.Algebra.Polynomial.CoeffMem Mathlib.Algebra.Polynomial.Coeff Mathlib.Algebra.Polynomial.Degree.Definitions Mathlib.Algebra.Polynomial.Degree.Domain 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.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.GroupRingAction Mathlib.Algebra.Polynomial.HasseDeriv Mathlib.Algebra.Polynomial.Identities Mathlib.Algebra.Polynomial.Inductions Mathlib.Algebra.Polynomial.Lifts Mathlib.Algebra.Polynomial.Mirror Mathlib.Algebra.Polynomial.Monic Mathlib.Algebra.Polynomial.Monomial Mathlib.Algebra.Polynomial.Reverse Mathlib.Algebra.Polynomial.RingDivision Mathlib.Algebra.Polynomial.Sequence Mathlib.Algebra.Polynomial.Smeval Mathlib.Algebra.Polynomial.SumIteratedDerivative Mathlib.Algebra.Polynomial.Taylor Mathlib.Algebra.Polynomial.UnitTrinomial Mathlib.Algebra.Polynomial.ofFn Mathlib.Algebra.PresentedMonoid.Basic Mathlib.Algebra.Prime.Defs Mathlib.Algebra.Prime.Lemmas Mathlib.Algebra.QuadraticDiscriminant Mathlib.Algebra.Quotient Mathlib.Algebra.Regular.Pow Mathlib.Algebra.Ring.Action.ConjAct Mathlib.Algebra.Ring.Action.End Mathlib.Algebra.Ring.Action.Group Mathlib.Algebra.Ring.Action.Invariant Mathlib.Algebra.Ring.Action.Pointwise.Finset Mathlib.Algebra.Ring.Action.Submonoid Mathlib.Algebra.Ring.Action.Subobjects Mathlib.Algebra.Ring.AddAut Mathlib.Algebra.Ring.Associated Mathlib.Algebra.Ring.Aut Mathlib.Algebra.Ring.Basic Mathlib.Algebra.Ring.BooleanRing Mathlib.Algebra.Ring.Center Mathlib.Algebra.Ring.CentroidHom Mathlib.Algebra.Ring.CharZero Mathlib.Algebra.Ring.Divisibility.Basic Mathlib.Algebra.Ring.Divisibility.Lemmas Mathlib.Algebra.Ring.Fin Mathlib.Algebra.Ring.Hom.Basic Mathlib.Algebra.Ring.Hom.Defs Mathlib.Algebra.Ring.Identities Mathlib.Algebra.Ring.Int.Parity Mathlib.Algebra.Ring.MinimalAxioms Mathlib.Algebra.Ring.NonZeroDivisors Mathlib.Algebra.Ring.Parity Mathlib.Algebra.Ring.Pointwise.Finset Mathlib.Algebra.Ring.Rat Mathlib.Algebra.Ring.Semireal.Defs Mathlib.Algebra.Ring.Subgroup Mathlib.Algebra.Ring.Submonoid.Pointwise Mathlib.Algebra.Ring.Subring.Basic Mathlib.Algebra.Ring.Subring.Defs Mathlib.Algebra.Ring.Subring.IntPolynomial Mathlib.Algebra.Ring.Subring.MulOpposite Mathlib.Algebra.Ring.Subring.Order Mathlib.Algebra.Ring.Subring.Pointwise Mathlib.Algebra.Ring.Subring.Units Mathlib.Algebra.Ring.Subsemiring.Basic Mathlib.Algebra.Ring.Subsemiring.MulOpposite Mathlib.Algebra.Ring.Subsemiring.Pointwise Mathlib.Algebra.Ring.SumsOfSquares Mathlib.Algebra.Ring.WithZero Mathlib.Algebra.RingQuot Mathlib.Algebra.SkewMonoidAlgebra.Basic Mathlib.Algebra.Small.Group Mathlib.Algebra.Small.Module Mathlib.Algebra.Small.Ring Mathlib.Algebra.Squarefree.Basic Mathlib.Algebra.Star.Basic Mathlib.Algebra.Star.BigOperators Mathlib.Algebra.Star.Center Mathlib.Algebra.Star.CentroidHom Mathlib.Algebra.Star.Conjneg Mathlib.Algebra.Star.Free Mathlib.Algebra.Star.Module Mathlib.Algebra.Star.NonUnitalSubalgebra Mathlib.Algebra.Star.NonUnitalSubsemiring Mathlib.Algebra.Star.Pi Mathlib.Algebra.Star.Pointwise Mathlib.Algebra.Star.Prod Mathlib.Algebra.Star.Rat Mathlib.Algebra.Star.RingQuot Mathlib.Algebra.Star.SelfAdjoint Mathlib.Algebra.Star.StarAlgHom Mathlib.Algebra.Star.StarRingHom Mathlib.Algebra.Star.Subalgebra Mathlib.Algebra.Star.Subsemiring Mathlib.Algebra.TrivSqZeroExt Mathlib.Algebra.Tropical.BigOperators Mathlib.Algebra.Vertex.HVertexOperator Mathlib.Algebra.Vertex.VertexOperator Mathlib.AlgebraicTopology.DoldKan.Compatibility Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms Mathlib.Analysis.Asymptotics.Defs Mathlib.Analysis.BoxIntegral.Box.Basic Mathlib.Analysis.BoxIntegral.Partition.Basic Mathlib.Analysis.BoxIntegral.Partition.Split Mathlib.Analysis.BoxIntegral.Partition.Tagged Mathlib.Analysis.Convex.Basic Mathlib.Analysis.Convex.Cone.Basic Mathlib.Analysis.Convex.Cone.Extension Mathlib.Analysis.Convex.Contractible Mathlib.Analysis.Convex.Extrema Mathlib.Analysis.Convex.Extreme Mathlib.Analysis.Convex.Function Mathlib.Analysis.Convex.Hull Mathlib.Analysis.Convex.Join Mathlib.Analysis.Convex.Mul Mathlib.Analysis.Convex.Piecewise Mathlib.Analysis.Convex.Quasiconvex Mathlib.Analysis.Convex.Segment Mathlib.Analysis.Convex.Slope Mathlib.Analysis.Convex.Star Mathlib.Analysis.Convex.Strict Mathlib.Analysis.Normed.Field.Basic Mathlib.Analysis.Normed.Group.AddTorsor Mathlib.Analysis.Normed.Group.Basic Mathlib.Analysis.Normed.Group.Bounded Mathlib.Analysis.Normed.Group.CocompactMap Mathlib.Analysis.Normed.Group.Constructions Mathlib.Analysis.Normed.Group.Continuity Mathlib.Analysis.Normed.Group.Int Mathlib.Analysis.Normed.Group.Rat Mathlib.Analysis.Normed.Group.Seminorm Mathlib.Analysis.Normed.Group.Subgroup Mathlib.Analysis.Normed.Group.Submodule Mathlib.Analysis.Normed.Lp.WithLp Mathlib.Analysis.Normed.Order.Basic Mathlib.Analysis.Normed.Order.Hom.Basic Mathlib.Analysis.Normed.Order.Hom.Ultra Mathlib.Analysis.Normed.Ring.Basic Mathlib.Analysis.Normed.Ring.WithAbs Mathlib.Analysis.NormedSpace.IndicatorFunction Mathlib.Analysis.NormedSpace.MStructure Mathlib.Analysis.Oscillation Mathlib.Analysis.Polynomial.CauchyBound Mathlib.Analysis.Subadditive Mathlib.CategoryTheory.Adjunction.Basic Mathlib.CategoryTheory.Adjunction.Comma Mathlib.CategoryTheory.Adjunction.Evaluation Mathlib.CategoryTheory.Adjunction.Limits Mathlib.CategoryTheory.Adjunction.Mates Mathlib.CategoryTheory.Adjunction.Opposites Mathlib.CategoryTheory.Adjunction.PartialAdjoint Mathlib.CategoryTheory.Adjunction.Restrict Mathlib.CategoryTheory.Adjunction.Unique Mathlib.CategoryTheory.Adjunction.Whiskering Mathlib.CategoryTheory.Balanced Mathlib.CategoryTheory.Bicategory.Adjunction.Basic Mathlib.CategoryTheory.Bicategory.Adjunction.Mate Mathlib.CategoryTheory.Bicategory.Basic Mathlib.CategoryTheory.Bicategory.End Mathlib.CategoryTheory.Bicategory.Extension Mathlib.CategoryTheory.Bicategory.Functor.Prelax Mathlib.CategoryTheory.Bicategory.Kan.Adjunction Mathlib.CategoryTheory.Bicategory.Kan.HasKan Mathlib.CategoryTheory.Bicategory.Kan.IsKan Mathlib.CategoryTheory.Bicategory.LocallyDiscrete Mathlib.CategoryTheory.Bicategory.Strict Mathlib.CategoryTheory.CatCommSq Mathlib.CategoryTheory.Category.Basic Mathlib.CategoryTheory.Category.Bipointed Mathlib.CategoryTheory.Category.Cat.Limit Mathlib.CategoryTheory.Category.Factorisation Mathlib.CategoryTheory.Category.GaloisConnection Mathlib.CategoryTheory.Category.KleisliCat Mathlib.CategoryTheory.Category.PartialFun Mathlib.CategoryTheory.Category.Pointed Mathlib.CategoryTheory.Category.Preorder Mathlib.CategoryTheory.Category.Quiv Mathlib.CategoryTheory.Category.ReflQuiv Mathlib.CategoryTheory.Category.TwoP Mathlib.CategoryTheory.Category.ULift Mathlib.CategoryTheory.Center.Basic Mathlib.CategoryTheory.Closed.Monoidal Mathlib.CategoryTheory.CommSq Mathlib.CategoryTheory.Comma.Arrow Mathlib.CategoryTheory.Comma.Basic Mathlib.CategoryTheory.Comma.LocallySmall Mathlib.CategoryTheory.Comma.Over.Pullback Mathlib.CategoryTheory.Comma.StructuredArrow.Basic Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap Mathlib.CategoryTheory.Comma.StructuredArrow.Small Mathlib.CategoryTheory.ComposableArrows Mathlib.CategoryTheory.ConcreteCategory.Basic Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso Mathlib.CategoryTheory.Conj Mathlib.CategoryTheory.ConnectedComponents Mathlib.CategoryTheory.Core Mathlib.CategoryTheory.Countable Mathlib.CategoryTheory.Discrete.Basic Mathlib.CategoryTheory.Discrete.SumsProducts Mathlib.CategoryTheory.EffectiveEpi.Basic Mathlib.CategoryTheory.EffectiveEpi.Comp Mathlib.CategoryTheory.EffectiveEpi.Coproduct Mathlib.CategoryTheory.EffectiveEpi.Enough Mathlib.CategoryTheory.EffectiveEpi.Preserves Mathlib.CategoryTheory.EffectiveEpi.RegularEpi Mathlib.CategoryTheory.Elementwise Mathlib.CategoryTheory.Endofunctor.Algebra Mathlib.CategoryTheory.Endomorphism Mathlib.CategoryTheory.EpiMono Mathlib.CategoryTheory.EqToHom Mathlib.CategoryTheory.Equivalence Mathlib.CategoryTheory.EssentialImage Mathlib.CategoryTheory.EssentiallySmall Mathlib.CategoryTheory.FiberedCategory.BasedCategory Mathlib.CategoryTheory.FiberedCategory.Cartesian Mathlib.CategoryTheory.FiberedCategory.Cocartesian Mathlib.CategoryTheory.FiberedCategory.Fiber Mathlib.CategoryTheory.FiberedCategory.Fibered Mathlib.CategoryTheory.FiberedCategory.HomLift Mathlib.CategoryTheory.Functor.Basic Mathlib.CategoryTheory.Functor.Category Mathlib.CategoryTheory.Functor.Const Mathlib.CategoryTheory.Functor.CurryingThree Mathlib.CategoryTheory.Functor.Currying Mathlib.CategoryTheory.Functor.Derived.RightDerived Mathlib.CategoryTheory.Functor.EpiMono Mathlib.CategoryTheory.Functor.FullyFaithful Mathlib.CategoryTheory.Functor.Functorial Mathlib.CategoryTheory.Functor.Hom Mathlib.CategoryTheory.Functor.KanExtension.Adjunction Mathlib.CategoryTheory.Functor.KanExtension.Basic Mathlib.CategoryTheory.Functor.KanExtension.Pointwise Mathlib.CategoryTheory.Functor.OfSequence Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced Mathlib.CategoryTheory.Functor.ReflectsIso.Basic Mathlib.CategoryTheory.Functor.Trifunctor Mathlib.CategoryTheory.Functor.TwoSquare Mathlib.CategoryTheory.Groupoid.Basic Mathlib.CategoryTheory.Groupoid.Discrete Mathlib.CategoryTheory.Groupoid.FreeGroupoid Mathlib.CategoryTheory.Groupoid.Subgroupoid Mathlib.CategoryTheory.Groupoid Mathlib.CategoryTheory.HomCongr Mathlib.CategoryTheory.InducedCategory Mathlib.CategoryTheory.IsConnected Mathlib.CategoryTheory.Iso Mathlib.CategoryTheory.Join.Basic Mathlib.CategoryTheory.LiftingProperties.Adjunction Mathlib.CategoryTheory.LiftingProperties.Basic Mathlib.CategoryTheory.Limits.ColimitLimit Mathlib.CategoryTheory.Limits.ConeCategory Mathlib.CategoryTheory.Limits.Cones Mathlib.CategoryTheory.Limits.Connected Mathlib.CategoryTheory.Limits.Constructions.Over.Connected Mathlib.CategoryTheory.Limits.Constructions.Pullbacks Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial Mathlib.CategoryTheory.Limits.Creates Mathlib.CategoryTheory.Limits.Elements Mathlib.CategoryTheory.Limits.EssentiallySmall Mathlib.CategoryTheory.Limits.Fubini Mathlib.CategoryTheory.Limits.FullSubcategory Mathlib.CategoryTheory.Limits.FunctorCategory.Basic Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks Mathlib.CategoryTheory.Limits.FunctorToTypes Mathlib.CategoryTheory.Limits.HasLimits Mathlib.CategoryTheory.Limits.IsLimit Mathlib.CategoryTheory.Limits.Pi Mathlib.CategoryTheory.Limits.Preorder Mathlib.CategoryTheory.Limits.Preserves.Basic Mathlib.CategoryTheory.Limits.Preserves.Grothendieck Mathlib.CategoryTheory.Limits.Preserves.Limits Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal Mathlib.CategoryTheory.Limits.Preserves.Ulift Mathlib.CategoryTheory.Limits.Preserves.Yoneda Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts Mathlib.CategoryTheory.Limits.Shapes.Connected Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct Mathlib.CategoryTheory.Limits.Shapes.End Mathlib.CategoryTheory.Limits.Shapes.Equalizers Mathlib.CategoryTheory.Limits.Shapes.Equivalence Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes Mathlib.CategoryTheory.Limits.Shapes.Grothendieck Mathlib.CategoryTheory.Limits.Shapes.Images Mathlib.CategoryTheory.Limits.Shapes.IsTerminal Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer Mathlib.CategoryTheory.Limits.Shapes.PiProd Mathlib.CategoryTheory.Limits.Shapes.Preorder.Basic Mathlib.CategoryTheory.Limits.Shapes.Products Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone Mathlib.CategoryTheory.Limits.Shapes.RegularMono Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer Mathlib.CategoryTheory.Limits.Shapes.StrictInitial Mathlib.CategoryTheory.Limits.Shapes.StrongEpi Mathlib.CategoryTheory.Limits.Shapes.Terminal Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects Mathlib.CategoryTheory.Limits.Types.Colimits Mathlib.CategoryTheory.Limits.Types.Images Mathlib.CategoryTheory.Limits.Types.Limits Mathlib.CategoryTheory.Limits.Types.Shapes Mathlib.CategoryTheory.Limits.Types.Yoneda Mathlib.CategoryTheory.Limits.Unit Mathlib.CategoryTheory.Limits.Yoneda Mathlib.CategoryTheory.Localization.Adjunction Mathlib.CategoryTheory.Localization.Bifunctor Mathlib.CategoryTheory.Localization.Bousfield Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction Mathlib.CategoryTheory.Localization.CalculusOfFractions Mathlib.CategoryTheory.Localization.Composition Mathlib.CategoryTheory.Localization.Construction Mathlib.CategoryTheory.Localization.Equivalence Mathlib.CategoryTheory.Localization.HasLocalization Mathlib.CategoryTheory.Localization.HomEquiv Mathlib.CategoryTheory.Localization.LocalizerMorphism Mathlib.CategoryTheory.Localization.LocallySmall Mathlib.CategoryTheory.Localization.Monoidal Mathlib.CategoryTheory.Localization.Opposite Mathlib.CategoryTheory.Localization.Predicate Mathlib.CategoryTheory.Localization.Prod Mathlib.CategoryTheory.Localization.Resolution Mathlib.CategoryTheory.Localization.SmallHom Mathlib.CategoryTheory.Localization.StructuredArrow Mathlib.CategoryTheory.Localization.Trifunctor Mathlib.CategoryTheory.Monad.Algebra Mathlib.CategoryTheory.Monad.Basic Mathlib.CategoryTheory.Monad.Kleisli Mathlib.CategoryTheory.Monad.Limits Mathlib.CategoryTheory.Monad.Products Mathlib.CategoryTheory.Monad.Types Mathlib.CategoryTheory.Monoidal.Braided.Basic Mathlib.CategoryTheory.Monoidal.Braided.Opposite Mathlib.CategoryTheory.Monoidal.Category Mathlib.CategoryTheory.Monoidal.Center Mathlib.CategoryTheory.Monoidal.CoherenceLemmas Mathlib.CategoryTheory.Monoidal.Discrete Mathlib.CategoryTheory.Monoidal.FunctorCategory Mathlib.CategoryTheory.Monoidal.OfChosenFiniteProducts.Basic Mathlib.CategoryTheory.Monoidal.Opposite Mathlib.CategoryTheory.Monoidal.Rigid.Basic Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence Mathlib.CategoryTheory.MorphismProperty.Comma Mathlib.CategoryTheory.NatIso Mathlib.CategoryTheory.NatTrans Mathlib.CategoryTheory.ObjectProperty.Basic Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms Mathlib.CategoryTheory.ObjectProperty.FullSubcategory Mathlib.CategoryTheory.Opposites Mathlib.CategoryTheory.PEmpty Mathlib.CategoryTheory.PUnit Mathlib.CategoryTheory.PathCategory.Basic Mathlib.CategoryTheory.Pi.Basic Mathlib.CategoryTheory.Products.Associator Mathlib.CategoryTheory.Products.Basic Mathlib.CategoryTheory.Products.Bifunctor Mathlib.CategoryTheory.Products.Unitor Mathlib.CategoryTheory.Quotient Mathlib.CategoryTheory.Retract Mathlib.CategoryTheory.Sigma.Basic Mathlib.CategoryTheory.Sites.Closed Mathlib.CategoryTheory.Sites.EffectiveEpimorphic Mathlib.CategoryTheory.Sites.EqualizerSheafCondition Mathlib.CategoryTheory.Sites.Grothendieck Mathlib.CategoryTheory.Sites.IsSheafFor Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1 Mathlib.CategoryTheory.Sites.Pretopology Mathlib.CategoryTheory.Sites.SheafOfTypes Mathlib.CategoryTheory.Sites.Sieves Mathlib.CategoryTheory.Square Mathlib.CategoryTheory.Subpresheaf.Sieves Mathlib.CategoryTheory.Sums.Associator Mathlib.CategoryTheory.Sums.Basic Mathlib.CategoryTheory.Sums.Products Mathlib.CategoryTheory.Thin Mathlib.CategoryTheory.Types Mathlib.CategoryTheory.UnivLE Mathlib.CategoryTheory.Whiskering Mathlib.CategoryTheory.WithTerminal.Basic Mathlib.CategoryTheory.Yoneda Mathlib.Combinatorics.Additive.CovBySMul Mathlib.Combinatorics.Additive.Dissociation Mathlib.Combinatorics.Additive.DoublingConst Mathlib.Combinatorics.Additive.ETransform Mathlib.Combinatorics.Additive.Energy Mathlib.Combinatorics.Additive.PluenneckeRuzsa Mathlib.Combinatorics.Additive.SmallTripling Mathlib.Combinatorics.Colex Mathlib.Combinatorics.Derangements.Basic Mathlib.Combinatorics.Derangements.Finite Mathlib.Combinatorics.Digraph.Basic Mathlib.Combinatorics.Digraph.Orientation Mathlib.Combinatorics.Enumerative.Bell Mathlib.Combinatorics.Enumerative.Catalan Mathlib.Combinatorics.Enumerative.Composition Mathlib.Combinatorics.Enumerative.DoubleCounting Mathlib.Combinatorics.Enumerative.DyckWord Mathlib.Combinatorics.Enumerative.IncidenceAlgebra Mathlib.Combinatorics.Enumerative.InclusionExclusion Mathlib.Combinatorics.Enumerative.Partition Mathlib.Combinatorics.HalesJewett Mathlib.Combinatorics.Hall.Finite Mathlib.Combinatorics.Hindman Mathlib.Combinatorics.Optimization.ValuedCSP Mathlib.Combinatorics.Pigeonhole Mathlib.Combinatorics.Quiver.Covering Mathlib.Combinatorics.Quiver.ReflQuiver Mathlib.Combinatorics.Schnirelmann Mathlib.Combinatorics.SetFamily.AhlswedeZhang Mathlib.Combinatorics.SetFamily.Compression.Down Mathlib.Combinatorics.SetFamily.Compression.UV Mathlib.Combinatorics.SetFamily.FourFunctions Mathlib.Combinatorics.SetFamily.HarrisKleitman Mathlib.Combinatorics.SetFamily.Kleitman Mathlib.Combinatorics.SetFamily.KruskalKatona Mathlib.Combinatorics.SetFamily.LYM Mathlib.Combinatorics.SetFamily.Shadow Mathlib.Combinatorics.SetFamily.Shatter Mathlib.Combinatorics.SimpleGraph.Basic Mathlib.Combinatorics.SimpleGraph.Circulant Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp Mathlib.Combinatorics.SimpleGraph.Copy Mathlib.Combinatorics.SimpleGraph.Dart Mathlib.Combinatorics.SimpleGraph.DeleteEdges Mathlib.Combinatorics.SimpleGraph.Density Mathlib.Combinatorics.SimpleGraph.Diam Mathlib.Combinatorics.SimpleGraph.Extremal.Basic Mathlib.Combinatorics.SimpleGraph.Finite Mathlib.Combinatorics.SimpleGraph.Hamiltonian Mathlib.Combinatorics.SimpleGraph.Hasse Mathlib.Combinatorics.SimpleGraph.IncMatrix Mathlib.Combinatorics.SimpleGraph.LineGraph Mathlib.Combinatorics.SimpleGraph.Maps Mathlib.Combinatorics.SimpleGraph.Metric Mathlib.Combinatorics.SimpleGraph.Operations Mathlib.Combinatorics.SimpleGraph.Path Mathlib.Combinatorics.SimpleGraph.Prod Mathlib.Combinatorics.SimpleGraph.Regularity.Energy Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform Mathlib.Combinatorics.SimpleGraph.Subgraph Mathlib.Combinatorics.SimpleGraph.Trails Mathlib.Combinatorics.SimpleGraph.Walk Mathlib.Combinatorics.Young.SemistandardTableau Mathlib.Combinatorics.Young.YoungDiagram Mathlib.Computability.Ackermann Mathlib.Computability.ContextFreeGrammar Mathlib.Computability.DFA Mathlib.Computability.Encoding Mathlib.Computability.EpsilonNFA Mathlib.Computability.Halting Mathlib.Computability.Language Mathlib.Computability.MyhillNerode Mathlib.Computability.NFA Mathlib.Computability.PartrecCode Mathlib.Computability.Partrec Mathlib.Computability.PostTuringMachine Mathlib.Computability.Primrec Mathlib.Computability.Reduce Mathlib.Computability.RegularExpressions Mathlib.Computability.TMComputable Mathlib.Computability.TMConfig Mathlib.Computability.TMToPartrec Mathlib.Computability.Tape Mathlib.Computability.TuringMachine Mathlib.Control.Bifunctor Mathlib.Control.Bitraversable.Basic Mathlib.Control.Bitraversable.Instances Mathlib.Control.Bitraversable.Lemmas Mathlib.Control.Fix Mathlib.Control.Fold Mathlib.Control.Random Mathlib.Control.Traversable.Instances Mathlib.Control.ULiftable Mathlib.Data.Analysis.Filter Mathlib.Data.Analysis.Topology Mathlib.Data.Bool.Count Mathlib.Data.Complex.Basic Mathlib.Data.Complex.BigOperators Mathlib.Data.Countable.Basic Mathlib.Data.DFinsupp.BigOperators Mathlib.Data.DFinsupp.Defs Mathlib.Data.DFinsupp.Encodable Mathlib.Data.DFinsupp.Ext Mathlib.Data.DFinsupp.FiniteInfinite Mathlib.Data.DFinsupp.Interval Mathlib.Data.DFinsupp.Lex Mathlib.Data.DFinsupp.Module Mathlib.Data.DFinsupp.Multiset Mathlib.Data.DFinsupp.NeLocus Mathlib.Data.DFinsupp.Notation Mathlib.Data.DFinsupp.Order Mathlib.Data.DFinsupp.Sigma Mathlib.Data.DFinsupp.Small Mathlib.Data.DFinsupp.Submonoid Mathlib.Data.DFinsupp.WellFounded Mathlib.Data.DList.Instances Mathlib.Data.ENNReal.Action Mathlib.Data.ENNReal.Basic Mathlib.Data.ENNReal.BigOperators Mathlib.Data.ENNReal.Holder Mathlib.Data.ENNReal.Inv Mathlib.Data.ENNReal.Lemmas Mathlib.Data.ENNReal.Operations Mathlib.Data.ENNReal.Order Mathlib.Data.ENNReal.Real Mathlib.Data.ENat.Basic Mathlib.Data.ENat.BigOperators Mathlib.Data.ENat.Lattice Mathlib.Data.EReal.Basic Mathlib.Data.EReal.Inv Mathlib.Data.EReal.Operations Mathlib.Data.Fin.Tuple.BubbleSortInduction Mathlib.Data.Fin.Tuple.Finset Mathlib.Data.Fin.Tuple.NatAntidiagonal Mathlib.Data.Fin.Tuple.Reflection Mathlib.Data.Fin.Tuple.Sort Mathlib.Data.FinEnum.Option Mathlib.Data.FinEnum Mathlib.Data.Finite.Prod Mathlib.Data.Finite.Sigma Mathlib.Data.Finite.Sum Mathlib.Data.Finite.Vector Mathlib.Data.Finmap Mathlib.Data.Finset.CastCard Mathlib.Data.Finset.Density Mathlib.Data.Finset.Finsupp Mathlib.Data.Finset.Functor Mathlib.Data.Finset.Grade Mathlib.Data.Finset.Interval Mathlib.Data.Finset.Lattice.Fold Mathlib.Data.Finset.Lattice.Pi Mathlib.Data.Finset.Lattice.Prod Mathlib.Data.Finset.Lattice.Union Mathlib.Data.Finset.Max Mathlib.Data.Finset.MulAntidiagonal Mathlib.Data.Finset.NAry Mathlib.Data.Finset.NatAntidiagonal Mathlib.Data.Finset.NatDivisors Mathlib.Data.Finset.NoncommProd Mathlib.Data.Finset.Option Mathlib.Data.Finset.PImage Mathlib.Data.Finset.Pairwise Mathlib.Data.Finset.PiInduction Mathlib.Data.Finset.Pi Mathlib.Data.Finset.Powerset Mathlib.Data.Finset.Preimage Mathlib.Data.Finset.Prod Mathlib.Data.Finset.SMulAntidiagonal Mathlib.Data.Finset.Sigma Mathlib.Data.Finset.Slice Mathlib.Data.Finset.Sort Mathlib.Data.Finset.Sum Mathlib.Data.Finset.Sups Mathlib.Data.Finset.Sym Mathlib.Data.Finset.Union Mathlib.Data.Finset.Update Mathlib.Data.Finsupp.AList Mathlib.Data.Finsupp.Antidiagonal Mathlib.Data.Finsupp.Basic Mathlib.Data.Finsupp.BigOperators Mathlib.Data.Finsupp.Defs Mathlib.Data.Finsupp.Encodable Mathlib.Data.Finsupp.Ext Mathlib.Data.Finsupp.Fin Mathlib.Data.Finsupp.Fintype Mathlib.Data.Finsupp.Indicator Mathlib.Data.Finsupp.Interval Mathlib.Data.Finsupp.Lex Mathlib.Data.Finsupp.MonomialOrder.DegLex Mathlib.Data.Finsupp.MonomialOrder Mathlib.Data.Finsupp.Multiset Mathlib.Data.Finsupp.NeLocus Mathlib.Data.Finsupp.Notation Mathlib.Data.Finsupp.Order Mathlib.Data.Finsupp.PWO Mathlib.Data.Finsupp.Pointwise Mathlib.Data.Finsupp.SMulWithZero Mathlib.Data.Finsupp.SMul Mathlib.Data.Finsupp.Single Mathlib.Data.Finsupp.ToDFinsupp Mathlib.Data.Finsupp.Weight Mathlib.Data.Finsupp.WellFounded Mathlib.Data.Fintype.BigOperators Mathlib.Data.Fintype.CardEmbedding Mathlib.Data.Fintype.Fin Mathlib.Data.Fintype.Lattice Mathlib.Data.Fintype.List Mathlib.Data.Fintype.Option Mathlib.Data.Fintype.Order Mathlib.Data.Fintype.Parity Mathlib.Data.Fintype.Perm Mathlib.Data.Fintype.Pi Mathlib.Data.Fintype.Pigeonhole Mathlib.Data.Fintype.Powerset Mathlib.Data.Fintype.Prod Mathlib.Data.Fintype.Quotient Mathlib.Data.Fintype.Sigma Mathlib.Data.Fintype.Sort Mathlib.Data.Fintype.Sum Mathlib.Data.Fintype.Vector Mathlib.Data.FunLike.Fintype Mathlib.Data.Holor Mathlib.Data.Int.AbsoluteValue Mathlib.Data.Int.Associated Mathlib.Data.Int.Bitwise Mathlib.Data.Int.CardIntervalMod Mathlib.Data.Int.Cast.Lemmas Mathlib.Data.Int.CharZero Mathlib.Data.Int.Interval Mathlib.Data.Int.Lemmas Mathlib.Data.Int.Log Mathlib.Data.Int.ModEq Mathlib.Data.Int.NatPrime Mathlib.Data.Int.Order.Lemmas Mathlib.Data.Int.Order.Units Mathlib.Data.Int.Range Mathlib.Data.Int.Star Mathlib.Data.Int.SuccPred Mathlib.Data.Int.WithZero Mathlib.Data.List.AList Mathlib.Data.List.Basic Mathlib.Data.List.Chain Mathlib.Data.List.Count Mathlib.Data.List.Cycle Mathlib.Data.List.Dedup Mathlib.Data.List.Destutter Mathlib.Data.List.DropRight Mathlib.Data.List.Duplicate Mathlib.Data.List.EditDistance.Bounds Mathlib.Data.List.EditDistance.Estimator Mathlib.Data.List.Enum Mathlib.Data.List.Forall2 Mathlib.Data.List.Indexes Mathlib.Data.List.Induction Mathlib.Data.List.Infix Mathlib.Data.List.InsertIdx Mathlib.Data.List.InsertNth Mathlib.Data.List.Intervals Mathlib.Data.List.Lattice Mathlib.Data.List.Lex Mathlib.Data.List.Map2 Mathlib.Data.List.MinMax Mathlib.Data.List.NatAntidiagonal Mathlib.Data.List.Nodup Mathlib.Data.List.Palindrome Mathlib.Data.List.Perm.Basic Mathlib.Data.List.Perm.Lattice Mathlib.Data.List.Perm.Subperm Mathlib.Data.List.Pi Mathlib.Data.List.Prime Mathlib.Data.List.ProdSigma Mathlib.Data.List.Range Mathlib.Data.List.ReduceOption Mathlib.Data.List.Rotate Mathlib.Data.List.Sections Mathlib.Data.List.Shortlex Mathlib.Data.List.Sigma Mathlib.Data.List.SplitBy Mathlib.Data.List.SplitOn Mathlib.Data.List.Sym Mathlib.Data.List.TakeDrop Mathlib.Data.List.ToFinsupp Mathlib.Data.List.Zip Mathlib.Data.LocallyFinsupp Mathlib.Data.Matrix.Auto Mathlib.Data.Matrix.Basic Mathlib.Data.Matrix.Basis Mathlib.Data.Matrix.Bilinear Mathlib.Data.Matrix.Block Mathlib.Data.Matrix.CharP Mathlib.Data.Matrix.ColumnRowPartitioned Mathlib.Data.Matrix.Composition Mathlib.Data.Matrix.ConjTranspose Mathlib.Data.Matrix.Defs Mathlib.Data.Matrix.Diagonal Mathlib.Data.Matrix.DualNumber Mathlib.Data.Matrix.Hadamard Mathlib.Data.Matrix.Invertible Mathlib.Data.Matrix.Mul Mathlib.Data.Matrix.Notation Mathlib.Data.Matrix.PEquiv Mathlib.Data.Matrix.Reflection Mathlib.Data.Matrix.RowCol Mathlib.Data.Multiset.AddSub Mathlib.Data.Multiset.Antidiagonal Mathlib.Data.Multiset.Basic Mathlib.Data.Multiset.Bind Mathlib.Data.Multiset.Count Mathlib.Data.Multiset.Defs Mathlib.Data.Multiset.DershowitzManna Mathlib.Data.Multiset.Fintype Mathlib.Data.Multiset.Functor Mathlib.Data.Multiset.Interval Mathlib.Data.Multiset.OrderedMonoid Mathlib.Data.Multiset.Pairwise Mathlib.Data.Multiset.Pi Mathlib.Data.Multiset.Powerset Mathlib.Data.Multiset.Replicate Mathlib.Data.Multiset.Sections Mathlib.Data.Multiset.Sum Mathlib.Data.Multiset.Sym Mathlib.Data.Multiset.ZeroCons Mathlib.Data.NNRat.BigOperators Mathlib.Data.NNRat.Defs Mathlib.Data.NNRat.Floor Mathlib.Data.NNRat.Lemmas Mathlib.Data.NNRat.Order Mathlib.Data.NNReal.Basic Mathlib.Data.NNReal.Defs Mathlib.Data.NNReal.Star Mathlib.Data.Nat.BitIndices Mathlib.Data.Nat.Bitwise Mathlib.Data.Nat.Cast.Basic Mathlib.Data.Nat.Cast.Field Mathlib.Data.Nat.Cast.Order.Basic Mathlib.Data.Nat.Cast.Order.Field Mathlib.Data.Nat.Cast.Order.Ring Mathlib.Data.Nat.Cast.SetInterval Mathlib.Data.Nat.ChineseRemainder Mathlib.Data.Nat.Choose.Basic Mathlib.Data.Nat.Choose.Bounds Mathlib.Data.Nat.Choose.Cast Mathlib.Data.Nat.Choose.Central Mathlib.Data.Nat.Choose.Dvd Mathlib.Data.Nat.Choose.Factorization Mathlib.Data.Nat.Choose.Mul Mathlib.Data.Nat.Choose.Multinomial Mathlib.Data.Nat.Choose.Sum Mathlib.Data.Nat.Choose.Vandermonde Mathlib.Data.Nat.Count Mathlib.Data.Nat.Digits Mathlib.Data.Nat.Dist Mathlib.Data.Nat.EvenOddRec Mathlib.Data.Nat.Factorial.Basic Mathlib.Data.Nat.Factorial.BigOperators Mathlib.Data.Nat.Factorial.Cast Mathlib.Data.Nat.Factorial.DoubleFactorial Mathlib.Data.Nat.Factorization.Basic Mathlib.Data.Nat.Factorization.Defs Mathlib.Data.Nat.Factorization.Induction Mathlib.Data.Nat.Factorization.PrimePow Mathlib.Data.Nat.Factorization.Root Mathlib.Data.Nat.Factors Mathlib.Data.Nat.Fib.Basic Mathlib.Data.Nat.Fib.Zeckendorf Mathlib.Data.Nat.GCD.Basic Mathlib.Data.Nat.GCD.BigOperators Mathlib.Data.Nat.Hyperoperation Mathlib.Data.Nat.Lattice Mathlib.Data.Nat.MaxPowDiv Mathlib.Data.Nat.ModEq Mathlib.Data.Nat.Multiplicity Mathlib.Data.Nat.Nth Mathlib.Data.Nat.PartENat Mathlib.Data.Nat.Prime.Basic Mathlib.Data.Nat.Prime.Defs Mathlib.Data.Nat.Prime.Factorial Mathlib.Data.Nat.Prime.Infinite Mathlib.Data.Nat.Prime.Int Mathlib.Data.Nat.Prime.Nth Mathlib.Data.Nat.Prime.Pow Mathlib.Data.Nat.PrimeFin Mathlib.Data.Nat.Squarefree Mathlib.Data.Nat.SuccPred Mathlib.Data.Nat.WithBot Mathlib.Data.Num.Bitwise Mathlib.Data.Num.Lemmas Mathlib.Data.Num.Prime Mathlib.Data.Num.ZNum Mathlib.Data.Ordmap.Invariants Mathlib.Data.Ordmap.Ordset Mathlib.Data.PFunctor.Multivariate.Basic Mathlib.Data.PFunctor.Multivariate.M Mathlib.Data.PFunctor.Multivariate.W Mathlib.Data.PFunctor.Univariate.Basic Mathlib.Data.PFunctor.Univariate.M Mathlib.Data.PNat.Basic Mathlib.Data.PNat.Factors Mathlib.Data.PNat.Find Mathlib.Data.PNat.Interval Mathlib.Data.PNat.Prime Mathlib.Data.PNat.Xgcd Mathlib.Data.Pi.Interval Mathlib.Data.QPF.Multivariate.Basic Mathlib.Data.QPF.Multivariate.Constructions.Cofix Mathlib.Data.QPF.Multivariate.Constructions.Comp Mathlib.Data.QPF.Multivariate.Constructions.Const Mathlib.Data.QPF.Multivariate.Constructions.Fix Mathlib.Data.QPF.Multivariate.Constructions.Prj Mathlib.Data.QPF.Multivariate.Constructions.Quot Mathlib.Data.QPF.Multivariate.Constructions.Sigma Mathlib.Data.QPF.Univariate.Basic Mathlib.Data.Rat.BigOperators Mathlib.Data.Rat.Cardinal Mathlib.Data.Rat.Cast.CharZero Mathlib.Data.Rat.Cast.Defs Mathlib.Data.Rat.Cast.Lemmas Mathlib.Data.Rat.Cast.Order Mathlib.Data.Rat.Denumerable Mathlib.Data.Rat.Encodable Mathlib.Data.Rat.Floor Mathlib.Data.Rat.Lemmas Mathlib.Data.Rat.Sqrt Mathlib.Data.Rat.Star Mathlib.Data.Real.Archimedean Mathlib.Data.Real.Basic Mathlib.Data.Real.ConjExponents Mathlib.Data.Real.ENatENNReal Mathlib.Data.Real.EReal Mathlib.Data.Real.Pointwise Mathlib.Data.Real.Sign Mathlib.Data.Real.Star Mathlib.Data.Seq.Parallel Mathlib.Data.Seq.Seq Mathlib.Data.Seq.WSeq Mathlib.Data.Set.Countable Mathlib.Data.Set.Equitable Mathlib.Data.Set.Finite.Lattice Mathlib.Data.Set.Finite.Lemmas Mathlib.Data.Set.Finite.List Mathlib.Data.Set.Finite.Monad Mathlib.Data.Set.Finite.Powerset Mathlib.Data.Set.FunctorToTypes Mathlib.Data.Set.MemPartition Mathlib.Data.Set.MulAntidiagonal Mathlib.Data.Set.Pointwise.Support Mathlib.Data.Set.SMulAntidiagonal Mathlib.Data.Set.Semiring Mathlib.Data.Set.Sups Mathlib.Data.SetLike.Fintype Mathlib.Data.Setoid.Partition Mathlib.Data.Sigma.Interval Mathlib.Data.Sign Mathlib.Data.String.Basic Mathlib.Data.Sum.Interval Mathlib.Data.Sym.Basic Mathlib.Data.Sym.Card Mathlib.Data.Sym.Sym2.Finsupp Mathlib.Data.Sym.Sym2.Order Mathlib.Data.Sym.Sym2 Mathlib.Data.Vector.Basic Mathlib.Data.Vector.Defs Mathlib.Data.Vector.MapLemmas Mathlib.Data.Vector.Mem Mathlib.Data.Vector.Snoc Mathlib.Data.Vector.Zip Mathlib.Data.W.Basic Mathlib.Data.W.Cardinal Mathlib.Data.W.Constructions Mathlib.Data.WSeq.Basic Mathlib.Data.WSeq.Defs Mathlib.Data.WSeq.Productive Mathlib.Data.WSeq.Relation Mathlib.Deprecated.Cardinal.Continuum Mathlib.Deprecated.Cardinal.PartENat Mathlib.Dynamics.BirkhoffSum.Average Mathlib.Dynamics.BirkhoffSum.Basic Mathlib.Dynamics.FixedPoints.Basic Mathlib.Dynamics.FixedPoints.Prufer Mathlib.Dynamics.FixedPoints.Topology Mathlib.Dynamics.Flow Mathlib.Dynamics.Minimal Mathlib.Dynamics.OmegaLimit Mathlib.Dynamics.PeriodicPts.Defs Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage Mathlib.FieldTheory.IntermediateField.Adjoin.Defs Mathlib.FieldTheory.IntermediateField.Basic Mathlib.FieldTheory.RatFunc.Defs Mathlib.Geometry.Group.Growth.LinearLowerBound Mathlib.Geometry.Group.Growth.QuotientInter Mathlib.Geometry.Manifold.ChartedSpace Mathlib.Geometry.Manifold.LocalInvariantProperties Mathlib.GroupTheory.ArchimedeanDensely Mathlib.GroupTheory.Archimedean Mathlib.GroupTheory.Commutator.Basic Mathlib.GroupTheory.Congruence.BigOperators Mathlib.GroupTheory.Coprod.Basic Mathlib.GroupTheory.CoprodI Mathlib.GroupTheory.Coset.Basic Mathlib.GroupTheory.Coset.Defs Mathlib.GroupTheory.Coxeter.Basic Mathlib.GroupTheory.Coxeter.Matrix Mathlib.GroupTheory.Divisible Mathlib.GroupTheory.DoubleCoset Mathlib.GroupTheory.Finiteness Mathlib.GroupTheory.FreeGroup.Basic Mathlib.GroupTheory.FreeGroup.IsFreeGroup Mathlib.GroupTheory.FreeGroup.Reduce Mathlib.GroupTheory.Goursat Mathlib.GroupTheory.GroupAction.Basic Mathlib.GroupTheory.GroupAction.ConjAct Mathlib.GroupTheory.GroupAction.Defs Mathlib.GroupTheory.GroupAction.FixedPoints Mathlib.GroupTheory.GroupAction.FixingSubgroup Mathlib.GroupTheory.GroupAction.Quotient Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise Mathlib.GroupTheory.GroupAction.SubMulAction Mathlib.GroupTheory.GroupAction.Transitive Mathlib.GroupTheory.MonoidLocalization.Away Mathlib.GroupTheory.MonoidLocalization.Basic Mathlib.GroupTheory.MonoidLocalization.Cardinality Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero Mathlib.GroupTheory.MonoidLocalization.Order Mathlib.GroupTheory.NoncommCoprod Mathlib.GroupTheory.OreLocalization.Basic Mathlib.GroupTheory.OreLocalization.Cardinality Mathlib.GroupTheory.Perm.Basic Mathlib.GroupTheory.Perm.ClosureSwap Mathlib.GroupTheory.Perm.List Mathlib.GroupTheory.Perm.Option Mathlib.GroupTheory.Perm.Sign Mathlib.GroupTheory.Perm.Support Mathlib.GroupTheory.Perm.ViaEmbedding Mathlib.GroupTheory.PresentedGroup Mathlib.GroupTheory.QuotientGroup.Basic Mathlib.GroupTheory.QuotientGroup.Defs Mathlib.GroupTheory.Subgroup.Center Mathlib.GroupTheory.Subgroup.Centralizer Mathlib.GroupTheory.Subgroup.Saturated Mathlib.GroupTheory.Subgroup.Simple Mathlib.GroupTheory.Submonoid.Inverses Mathlib.InformationTheory.Hamming Mathlib.LinearAlgebra.AffineSpace.AffineEquiv Mathlib.LinearAlgebra.AffineSpace.AffineMap Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs Mathlib.LinearAlgebra.AffineSpace.Combination Mathlib.LinearAlgebra.AffineSpace.Midpoint Mathlib.LinearAlgebra.AffineSpace.Pointwise Mathlib.LinearAlgebra.AffineSpace.Restrict Mathlib.LinearAlgebra.AffineSpace.Slope Mathlib.LinearAlgebra.Alternating.Basic Mathlib.LinearAlgebra.Basis.Basic Mathlib.LinearAlgebra.Basis.Bilinear Mathlib.LinearAlgebra.Basis.Cardinality Mathlib.LinearAlgebra.Basis.Defs Mathlib.LinearAlgebra.Basis.Fin Mathlib.LinearAlgebra.Basis.Flag Mathlib.LinearAlgebra.Basis.Prod Mathlib.LinearAlgebra.Basis.SMul Mathlib.LinearAlgebra.Basis.Submodule Mathlib.LinearAlgebra.BilinearForm.Basic Mathlib.LinearAlgebra.BilinearForm.Hom Mathlib.LinearAlgebra.BilinearMap Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv Mathlib.LinearAlgebra.Countable Mathlib.LinearAlgebra.DFinsupp Mathlib.LinearAlgebra.DirectSum.Basis Mathlib.LinearAlgebra.DirectSum.Finsupp Mathlib.LinearAlgebra.DirectSum.TensorProduct Mathlib.LinearAlgebra.Dual.Basis Mathlib.LinearAlgebra.Dual.Defs Mathlib.LinearAlgebra.Finsupp.Defs Mathlib.LinearAlgebra.Finsupp.LSum Mathlib.LinearAlgebra.Finsupp.LinearCombination Mathlib.LinearAlgebra.Finsupp.Pi Mathlib.LinearAlgebra.Finsupp.Span Mathlib.LinearAlgebra.Finsupp.SumProd Mathlib.LinearAlgebra.Finsupp.Supported Mathlib.LinearAlgebra.Finsupp.VectorSpace Mathlib.LinearAlgebra.FreeModule.Basic Mathlib.LinearAlgebra.FreeModule.Finite.Basic Mathlib.LinearAlgebra.FreeProduct.Basic Mathlib.LinearAlgebra.GeneralLinearGroup Mathlib.LinearAlgebra.LinearIndependent.Basic Mathlib.LinearAlgebra.LinearIndependent.Defs Mathlib.LinearAlgebra.LinearIndependent.Lemmas Mathlib.LinearAlgebra.LinearPMap Mathlib.LinearAlgebra.Matrix.Circulant Mathlib.LinearAlgebra.Matrix.DotProduct Mathlib.LinearAlgebra.Matrix.Dual Mathlib.LinearAlgebra.Matrix.Orthogonal Mathlib.LinearAlgebra.Matrix.Permanent Mathlib.LinearAlgebra.Matrix.SemiringInverse 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.Pi Mathlib.LinearAlgebra.Multilinear.TensorProduct Mathlib.LinearAlgebra.PiTensorProduct Mathlib.LinearAlgebra.Pi Mathlib.LinearAlgebra.Prod Mathlib.LinearAlgebra.Quotient.Defs Mathlib.LinearAlgebra.Ray Mathlib.LinearAlgebra.SModEq Mathlib.LinearAlgebra.SesquilinearForm Mathlib.LinearAlgebra.Span.Basic Mathlib.LinearAlgebra.Span.Defs Mathlib.LinearAlgebra.StdBasis Mathlib.LinearAlgebra.TensorAlgebra.Basic Mathlib.LinearAlgebra.TensorAlgebra.Grading Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower Mathlib.LinearAlgebra.TensorPower.Basic Mathlib.LinearAlgebra.TensorPower.Pairing Mathlib.LinearAlgebra.TensorProduct.Associator Mathlib.LinearAlgebra.TensorProduct.Basic Mathlib.LinearAlgebra.TensorProduct.Basis Mathlib.LinearAlgebra.TensorProduct.DirectLimit Mathlib.LinearAlgebra.TensorProduct.Finiteness Mathlib.LinearAlgebra.TensorProduct.Opposite Mathlib.LinearAlgebra.TensorProduct.Pi Mathlib.LinearAlgebra.TensorProduct.Prod Mathlib.LinearAlgebra.TensorProduct.Subalgebra Mathlib.LinearAlgebra.TensorProduct.Submodule Mathlib.LinearAlgebra.TensorProduct.Tower Mathlib.Logic.Denumerable Mathlib.Logic.Encodable.Basic Mathlib.Logic.Encodable.Lattice Mathlib.Logic.Encodable.Pi Mathlib.Logic.Equiv.Array Mathlib.Logic.Equiv.Fin.Rotate Mathlib.Logic.Equiv.Finset Mathlib.Logic.Equiv.Functor Mathlib.Logic.Equiv.List Mathlib.Logic.Equiv.Multiset Mathlib.Logic.Godel.GodelBetaFunction Mathlib.Logic.Hydra Mathlib.Logic.Small.List Mathlib.MeasureTheory.Constructions.AddChar Mathlib.MeasureTheory.MeasurableSpace.Basic Mathlib.MeasureTheory.MeasurableSpace.Card Mathlib.MeasureTheory.MeasurableSpace.Defs Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable Mathlib.MeasureTheory.MeasurableSpace.Invariants Mathlib.MeasureTheory.OuterMeasure.Defs Mathlib.MeasureTheory.PiSystem Mathlib.MeasureTheory.SetAlgebra Mathlib.MeasureTheory.SetSemiring Mathlib.ModelTheory.Algebra.Field.Basic Mathlib.ModelTheory.Algebra.Ring.Basic Mathlib.ModelTheory.Basic Mathlib.ModelTheory.Definability Mathlib.ModelTheory.DirectLimit Mathlib.ModelTheory.ElementaryMaps Mathlib.ModelTheory.ElementarySubstructures Mathlib.ModelTheory.Encoding Mathlib.ModelTheory.FinitelyGenerated Mathlib.ModelTheory.LanguageMap Mathlib.ModelTheory.PartialEquiv Mathlib.ModelTheory.Quotients Mathlib.ModelTheory.Semantics Mathlib.ModelTheory.Skolem Mathlib.ModelTheory.Substructures Mathlib.ModelTheory.Syntax Mathlib.ModelTheory.Ultraproducts Mathlib.NumberTheory.ADEInequality Mathlib.NumberTheory.ArithmeticFunction Mathlib.NumberTheory.Basic Mathlib.NumberTheory.ClassNumber.AdmissibleAbs Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue Mathlib.NumberTheory.Dioph Mathlib.NumberTheory.Divisors Mathlib.NumberTheory.EllipticDivisibilitySequence Mathlib.NumberTheory.FactorisationProperties Mathlib.NumberTheory.FrobeniusNumber Mathlib.NumberTheory.Harmonic.Defs Mathlib.NumberTheory.MaricaSchoenheim Mathlib.NumberTheory.Multiplicity Mathlib.NumberTheory.Padics.PadicNorm Mathlib.NumberTheory.Padics.PadicVal.Basic Mathlib.NumberTheory.Padics.PadicVal.Defs Mathlib.NumberTheory.PellMatiyasevic Mathlib.NumberTheory.Primorial Mathlib.NumberTheory.SelbergSieve Mathlib.NumberTheory.SmoothNumbers Mathlib.Order.Atoms.Finite Mathlib.Order.Birkhoff Mathlib.Order.BooleanGenerators Mathlib.Order.BooleanSubalgebra Mathlib.Order.Category.BddDistLat Mathlib.Order.Category.BddLat Mathlib.Order.Category.BddOrd Mathlib.Order.Category.BoolAlg Mathlib.Order.Category.CompleteLat Mathlib.Order.Category.DistLat Mathlib.Order.Category.Frm Mathlib.Order.Category.HeytAlg Mathlib.Order.Category.Lat Mathlib.Order.Category.LinOrd Mathlib.Order.Category.PartOrd Mathlib.Order.Category.Preord Mathlib.Order.Category.Semilat Mathlib.Order.CompactlyGenerated.Basic Mathlib.Order.CompactlyGenerated.Intervals Mathlib.Order.CompleteLattice.Finset Mathlib.Order.CompleteLattice.SetLike Mathlib.Order.CompletePartialOrder Mathlib.Order.CompleteSublattice Mathlib.Order.ConditionallyCompleteLattice.Finset Mathlib.Order.CountableDenseLinearOrder Mathlib.Order.Disjointed Mathlib.Order.Extension.Well Mathlib.Order.Filter.AtTopBot.Archimedean Mathlib.Order.Filter.AtTopBot.BigOperators Mathlib.Order.Filter.AtTopBot.CountablyGenerated Mathlib.Order.Filter.AtTopBot.Finite Mathlib.Order.Filter.AtTopBot.Finset Mathlib.Order.Filter.AtTopBot.Floor Mathlib.Order.Filter.AtTopBot.ModEq Mathlib.Order.Filter.AtTopBot.Prod Mathlib.Order.Filter.Bases.Finite Mathlib.Order.Filter.CardinalInter Mathlib.Order.Filter.Cocardinal Mathlib.Order.Filter.Cofinite Mathlib.Order.Filter.CountableInter Mathlib.Order.Filter.CountableSeparatingOn Mathlib.Order.Filter.CountablyGenerated Mathlib.Order.Filter.ENNReal Mathlib.Order.Filter.EventuallyConst Mathlib.Order.Filter.Extr Mathlib.Order.Filter.FilterProduct Mathlib.Order.Filter.Finite Mathlib.Order.Filter.Germ.Basic Mathlib.Order.Filter.Germ.OrderedMonoid Mathlib.Order.Filter.IndicatorFunction Mathlib.Order.Filter.Interval Mathlib.Order.Filter.IsBounded Mathlib.Order.Filter.Lift Mathlib.Order.Filter.ListTraverse Mathlib.Order.Filter.Pi Mathlib.Order.Filter.Pointwise Mathlib.Order.Filter.Ring Mathlib.Order.Filter.SmallSets Mathlib.Order.Filter.Subsingleton Mathlib.Order.Filter.Ultrafilter.Basic Mathlib.Order.Filter.Ultrafilter.Defs Mathlib.Order.FixedPoints Mathlib.Order.GameAdd Mathlib.Order.Grade Mathlib.Order.Height Mathlib.Order.Heyting.Boundary Mathlib.Order.Ideal Mathlib.Order.Interval.Finset.Basic Mathlib.Order.Interval.Finset.Box Mathlib.Order.Interval.Finset.Defs Mathlib.Order.Interval.Finset.Fin Mathlib.Order.Interval.Finset.Nat Mathlib.Order.Interval.Finset.SuccPred Mathlib.Order.Interval.Multiset Mathlib.Order.Interval.Set.IsoIoo Mathlib.Order.Interval.Set.OrdConnectedLinear Mathlib.Order.Interval.Set.Pi Mathlib.Order.Irreducible Mathlib.Order.JordanHolder Mathlib.Order.KonigLemma Mathlib.Order.KrullDimension Mathlib.Order.LiminfLimsup Mathlib.Order.Monotone.MonovaryOrder Mathlib.Order.OmegaCompletePartialOrder Mathlib.Order.OrderIsoNat Mathlib.Order.PFilter Mathlib.Order.Part Mathlib.Order.PartialSups Mathlib.Order.Partition.Basic Mathlib.Order.Partition.Equipartition Mathlib.Order.Partition.Finpartition Mathlib.Order.PrimeIdeal Mathlib.Order.PrimeSeparator Mathlib.Order.RelSeries Mathlib.Order.Restriction Mathlib.Order.Sublattice Mathlib.Order.SuccPred.LinearLocallyFinite Mathlib.Order.SupClosed Mathlib.Order.SupIndep Mathlib.Order.UpperLower.LocallyFinite Mathlib.Order.WellFoundedSet Mathlib.Order.WellQuasiOrder Mathlib.RingTheory.Adjoin.Basic Mathlib.RingTheory.Adjoin.Polynomial Mathlib.RingTheory.AlgebraTower Mathlib.RingTheory.Algebraic.Defs Mathlib.RingTheory.Algebraic.LinearIndependent Mathlib.RingTheory.Algebraic.Pi Mathlib.RingTheory.AlgebraicIndependent.Defs Mathlib.RingTheory.Bialgebra.Basic Mathlib.RingTheory.Bialgebra.Equiv Mathlib.RingTheory.Bialgebra.Hom Mathlib.RingTheory.Coalgebra.Basic Mathlib.RingTheory.Coalgebra.Equiv Mathlib.RingTheory.Coalgebra.Hom Mathlib.RingTheory.Congruence.BigOperators Mathlib.RingTheory.Coprime.Basic Mathlib.RingTheory.Derivation.Basic Mathlib.RingTheory.Derivation.DifferentialRing Mathlib.RingTheory.FilteredAlgebra.Basic Mathlib.RingTheory.Finiteness.Basic Mathlib.RingTheory.Finiteness.Bilinear Mathlib.RingTheory.Finiteness.Cardinality Mathlib.RingTheory.Finiteness.Defs Mathlib.RingTheory.Finiteness.Lattice Mathlib.RingTheory.Finiteness.Nilpotent Mathlib.RingTheory.Finiteness.Prod Mathlib.RingTheory.Finiteness.Projective Mathlib.RingTheory.Finiteness.Subalgebra Mathlib.RingTheory.GradedAlgebra.Basic Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule Mathlib.RingTheory.HahnSeries.Addition Mathlib.RingTheory.HahnSeries.Basic Mathlib.RingTheory.HahnSeries.HEval Mathlib.RingTheory.HahnSeries.Multiplication Mathlib.RingTheory.HahnSeries.PowerSeries Mathlib.RingTheory.HahnSeries.Summable Mathlib.RingTheory.HopfAlgebra.Basic Mathlib.RingTheory.Ideal.Basic Mathlib.RingTheory.Ideal.Basis Mathlib.RingTheory.Ideal.BigOperators Mathlib.RingTheory.Ideal.Defs Mathlib.RingTheory.Ideal.Lattice Mathlib.RingTheory.Ideal.Maximal Mathlib.RingTheory.Ideal.Nonunits Mathlib.RingTheory.Ideal.Prime Mathlib.RingTheory.Ideal.Quotient.Defs Mathlib.RingTheory.Ideal.Span Mathlib.RingTheory.IntegralClosure.Algebra.Defs Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs Mathlib.RingTheory.IsTensorProduct Mathlib.RingTheory.LocalRing.Basic Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs Mathlib.RingTheory.LocalRing.Subring Mathlib.RingTheory.Localization.BaseChange Mathlib.RingTheory.Localization.Basic Mathlib.RingTheory.Localization.Cardinality Mathlib.RingTheory.Localization.Defs Mathlib.RingTheory.Localization.FractionRing Mathlib.RingTheory.Localization.Integer Mathlib.RingTheory.Localization.Module Mathlib.RingTheory.Localization.NumDen Mathlib.RingTheory.Localization.Pi Mathlib.RingTheory.Multiplicity Mathlib.RingTheory.MvPolynomial.Basic Mathlib.RingTheory.MvPolynomial.Ideal Mathlib.RingTheory.MvPolynomial.Symmetric.Defs Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities Mathlib.RingTheory.MvPolynomial.Tower Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous Mathlib.RingTheory.MvPowerSeries.Basic Mathlib.RingTheory.MvPowerSeries.Inverse Mathlib.RingTheory.MvPowerSeries.LexOrder Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors Mathlib.RingTheory.MvPowerSeries.Order Mathlib.RingTheory.MvPowerSeries.Trunc Mathlib.RingTheory.Nilpotent.Basic Mathlib.RingTheory.Nilpotent.Defs Mathlib.RingTheory.Nilpotent.Exp Mathlib.RingTheory.Noetherian.Defs Mathlib.RingTheory.Noetherian.Filter Mathlib.RingTheory.NonUnitalSubring.Basic Mathlib.RingTheory.NonUnitalSubring.Defs Mathlib.RingTheory.NonUnitalSubsemiring.Basic Mathlib.RingTheory.OreLocalization.Basic Mathlib.RingTheory.OreLocalization.Cardinality Mathlib.RingTheory.OreLocalization.Ring Mathlib.RingTheory.OrzechProperty Mathlib.RingTheory.PiTensorProduct Mathlib.RingTheory.Polynomial.Bernstein Mathlib.RingTheory.Polynomial.Hermite.Basic Mathlib.RingTheory.Polynomial.IntegralNormalization Mathlib.RingTheory.Polynomial.Opposites Mathlib.RingTheory.Polynomial.Pochhammer Mathlib.RingTheory.Polynomial.ScaleRoots Mathlib.RingTheory.Polynomial.Tower Mathlib.RingTheory.Polynomial.Wronskian Mathlib.RingTheory.PolynomialAlgebra Mathlib.RingTheory.PolynomialLaw.Basic Mathlib.RingTheory.PowerSeries.Basic Mathlib.RingTheory.PowerSeries.Order Mathlib.RingTheory.PowerSeries.Trunc Mathlib.RingTheory.PowerSeries.WellKnown Mathlib.RingTheory.Prime Mathlib.RingTheory.Radical Mathlib.RingTheory.SimpleRing.Basic Mathlib.RingTheory.SimpleRing.Congr Mathlib.RingTheory.SimpleRing.Defs Mathlib.RingTheory.SimpleRing.Field Mathlib.RingTheory.Spectrum.Maximal.Basic Mathlib.RingTheory.Spectrum.Maximal.Defs Mathlib.RingTheory.Spectrum.Prime.Defs Mathlib.RingTheory.TensorProduct.Basic Mathlib.RingTheory.TensorProduct.Free Mathlib.RingTheory.TensorProduct.IsBaseChangePi Mathlib.RingTheory.TensorProduct.MvPolynomial Mathlib.RingTheory.TensorProduct.Pi Mathlib.RingTheory.TwoSidedIdeal.Basic Mathlib.RingTheory.TwoSidedIdeal.BigOperators Mathlib.RingTheory.TwoSidedIdeal.Instances Mathlib.RingTheory.TwoSidedIdeal.Kernel Mathlib.RingTheory.TwoSidedIdeal.Lattice Mathlib.RingTheory.TwoSidedIdeal.Operations Mathlib.RingTheory.UniqueFactorizationDomain.Basic Mathlib.RingTheory.UniqueFactorizationDomain.Defs Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet Mathlib.RingTheory.UniqueFactorizationDomain.Finite Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity Mathlib.RingTheory.UniqueFactorizationDomain.Nat Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors Mathlib.SetTheory.Cardinal.Aleph Mathlib.SetTheory.Cardinal.Arithmetic Mathlib.SetTheory.Cardinal.Basic Mathlib.SetTheory.Cardinal.Cofinality Mathlib.SetTheory.Cardinal.Continuum Mathlib.SetTheory.Cardinal.CountableCover Mathlib.SetTheory.Cardinal.Divisibility Mathlib.SetTheory.Cardinal.ENat Mathlib.SetTheory.Cardinal.Finsupp Mathlib.SetTheory.Cardinal.HasCardinalLT Mathlib.SetTheory.Cardinal.Order Mathlib.SetTheory.Cardinal.Ordinal Mathlib.SetTheory.Cardinal.Pigeonhole Mathlib.SetTheory.Cardinal.Regular Mathlib.SetTheory.Cardinal.SchroederBernstein Mathlib.SetTheory.Cardinal.Subfield Mathlib.SetTheory.Cardinal.ToNat Mathlib.SetTheory.Cardinal.UnivLE Mathlib.SetTheory.Descriptive.Tree Mathlib.SetTheory.Game.Basic Mathlib.SetTheory.Game.Birthday Mathlib.SetTheory.Game.Domineering Mathlib.SetTheory.Game.Impartial Mathlib.SetTheory.Game.Nim Mathlib.SetTheory.Game.Ordinal Mathlib.SetTheory.Game.Short Mathlib.SetTheory.Game.State Mathlib.SetTheory.Lists Mathlib.SetTheory.Nimber.Basic Mathlib.SetTheory.Ordinal.Arithmetic Mathlib.SetTheory.Ordinal.Basic Mathlib.SetTheory.Ordinal.CantorNormalForm Mathlib.SetTheory.Ordinal.Enum Mathlib.SetTheory.Ordinal.Exponential Mathlib.SetTheory.Ordinal.Family Mathlib.SetTheory.Ordinal.FixedPointApproximants Mathlib.SetTheory.Ordinal.FixedPoint Mathlib.SetTheory.Ordinal.NaturalOps Mathlib.SetTheory.Ordinal.Notation Mathlib.SetTheory.Ordinal.Principal Mathlib.SetTheory.Ordinal.Rank Mathlib.SetTheory.Ordinal.Topology Mathlib.SetTheory.Ordinal.Veblen Mathlib.SetTheory.PGame.Algebra Mathlib.SetTheory.PGame.Order Mathlib.SetTheory.Surreal.Basic Mathlib.SetTheory.Surreal.Dyadic Mathlib.SetTheory.Surreal.Multiplication Mathlib.SetTheory.ZFC.Class Mathlib.SetTheory.ZFC.Ordinal Mathlib.SetTheory.ZFC.Rank Mathlib.Tactic.Abel Mathlib.Tactic.Algebraize Mathlib.Tactic.Bound Mathlib.Tactic.CancelDenoms Mathlib.Tactic.CategoryTheory.BicategoricalComp Mathlib.Tactic.CategoryTheory.Bicategory.Basic Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes Mathlib.Tactic.CategoryTheory.Bicategory.Normalize Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence Mathlib.Tactic.CategoryTheory.CheckCompositions Mathlib.Tactic.CategoryTheory.Coherence.Basic Mathlib.Tactic.CategoryTheory.Coherence Mathlib.Tactic.CategoryTheory.Elementwise Mathlib.Tactic.CategoryTheory.Monoidal.Basic Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes Mathlib.Tactic.CategoryTheory.Monoidal.Normalize Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence Mathlib.Tactic.CategoryTheory.MonoidalComp Mathlib.Tactic.CategoryTheory.Reassoc Mathlib.Tactic.CategoryTheory.Slice Mathlib.Tactic.Common Mathlib.Tactic.ComputeDegree Mathlib.Tactic.DeriveEncodable Mathlib.Tactic.DeriveFintype Mathlib.Tactic.ENatToNat Mathlib.Tactic.FieldSimp Mathlib.Tactic.Finiteness Mathlib.Tactic.GCongr Mathlib.Tactic.Group Mathlib.Tactic.IntervalCases Mathlib.Tactic.Linarith.Datatypes Mathlib.Tactic.Linarith.Frontend Mathlib.Tactic.Linarith.Lemmas Mathlib.Tactic.Linarith.Oracle.FourierMotzkin Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm Mathlib.Tactic.Linarith.Parsing Mathlib.Tactic.Linarith.Preprocessing Mathlib.Tactic.Linarith.Verification Mathlib.Tactic.Linarith Mathlib.Tactic.LinearCombination' Mathlib.Tactic.LinearCombination.Lemmas Mathlib.Tactic.LinearCombination Mathlib.Tactic.ModCases Mathlib.Tactic.Module Mathlib.Tactic.MoveAdd Mathlib.Tactic.NoncommRing Mathlib.Tactic.NormNum.Basic Mathlib.Tactic.NormNum.BigOperators Mathlib.Tactic.NormNum.DivMod Mathlib.Tactic.NormNum.Eq Mathlib.Tactic.NormNum.Ineq Mathlib.Tactic.NormNum.Inv Mathlib.Tactic.NormNum.NatFactorial Mathlib.Tactic.NormNum.NatFib Mathlib.Tactic.NormNum.NatLog Mathlib.Tactic.NormNum.NatSqrt Mathlib.Tactic.NormNum.OfScientific Mathlib.Tactic.NormNum.PowMod Mathlib.Tactic.NormNum.Pow Mathlib.Tactic.NormNum.Prime Mathlib.Tactic.NormNum Mathlib.Tactic.PNatToNat Mathlib.Tactic.Polyrith Mathlib.Tactic.Positivity.Basic Mathlib.Tactic.Positivity.Core Mathlib.Tactic.Positivity.Finset Mathlib.Tactic.Positivity Mathlib.Tactic.Qify Mathlib.Tactic.RewriteSearch Mathlib.Tactic.Rify Mathlib.Tactic.Ring.Basic Mathlib.Tactic.Ring.Compare Mathlib.Tactic.Ring.PNat Mathlib.Tactic.Ring.RingNF Mathlib.Tactic.Ring Mathlib.Tactic.Widget.CommDiag Mathlib.Tactic.Widget.GCongr Mathlib.Tactic.Widget.StringDiagram Mathlib.Testing.Plausible.Functions Mathlib.Topology.AlexandrovDiscrete Mathlib.Topology.Algebra.Affine Mathlib.Topology.Algebra.Algebra.Rat Mathlib.Topology.Algebra.ConstMulAction Mathlib.Topology.Algebra.Constructions.DomMulAct Mathlib.Topology.Algebra.Constructions Mathlib.Topology.Algebra.ContinuousMonoidHom Mathlib.Topology.Algebra.Equicontinuity Mathlib.Topology.Algebra.Field Mathlib.Topology.Algebra.FilterBasis Mathlib.Topology.Algebra.Group.Basic Mathlib.Topology.Algebra.Group.Compact Mathlib.Topology.Algebra.Group.Defs 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.GroupCompletion Mathlib.Topology.Algebra.GroupWithZero Mathlib.Topology.Algebra.Indicator Mathlib.Topology.Algebra.InfiniteSum.Basic Mathlib.Topology.Algebra.InfiniteSum.Defs Mathlib.Topology.Algebra.InfiniteSum.Field Mathlib.Topology.Algebra.IntermediateField Mathlib.Topology.Algebra.IsUniformGroup.Basic Mathlib.Topology.Algebra.IsUniformGroup.Defs Mathlib.Topology.Algebra.LinearTopology Mathlib.Topology.Algebra.Localization Mathlib.Topology.Algebra.Module.Basic Mathlib.Topology.Algebra.Module.Compact Mathlib.Topology.Algebra.Module.LinearPMap Mathlib.Topology.Algebra.Monoid.AddChar Mathlib.Topology.Algebra.Monoid.Defs Mathlib.Topology.Algebra.Monoid Mathlib.Topology.Algebra.MulAction Mathlib.Topology.Algebra.MvPolynomial Mathlib.Topology.Algebra.NonUnitalAlgebra Mathlib.Topology.Algebra.NonUnitalStarAlgebra 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.Archimedean Mathlib.Topology.Algebra.Order.Field Mathlib.Topology.Algebra.Order.Floor Mathlib.Topology.Algebra.Order.Group Mathlib.Topology.Algebra.Order.LiminfLimsup Mathlib.Topology.Algebra.Order.Module Mathlib.Topology.Algebra.Order.Support Mathlib.Topology.Algebra.Order.UpperLower Mathlib.Topology.Algebra.ProperAction.Basic Mathlib.Topology.Algebra.ProperConstSMul Mathlib.Topology.Algebra.RestrictedProduct Mathlib.Topology.Algebra.Ring.Basic Mathlib.Topology.Algebra.Ring.Ideal Mathlib.Topology.Algebra.Ring.Real Mathlib.Topology.Algebra.Semigroup Mathlib.Topology.Algebra.Star.Real Mathlib.Topology.Algebra.Star Mathlib.Topology.Algebra.Support 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.Algebra.WithZeroTopology Mathlib.Topology.ApproximateUnit Mathlib.Topology.Baire.Lemmas Mathlib.Topology.Baire.LocallyCompactRegular Mathlib.Topology.Bases Mathlib.Topology.Basic Mathlib.Topology.Bornology.Absorbs Mathlib.Topology.Bornology.Basic Mathlib.Topology.Bornology.Constructions Mathlib.Topology.Bornology.Hom Mathlib.Topology.Bornology.Real Mathlib.Topology.Category.Born Mathlib.Topology.Category.CompHausLike.Basic Mathlib.Topology.Category.Sequential Mathlib.Topology.Category.TopCat.Adjunctions Mathlib.Topology.Category.TopCat.Basic Mathlib.Topology.Category.TopCat.EpiMono Mathlib.Topology.Category.TopCat.OpenNhds Mathlib.Topology.Category.TopCat.Opens Mathlib.Topology.Category.TopCat.ULift Mathlib.Topology.Category.TopCommRingCat Mathlib.Topology.ClopenBox Mathlib.Topology.Clopen Mathlib.Topology.Closure Mathlib.Topology.ClusterPt Mathlib.Topology.Coherent Mathlib.Topology.CompactOpen Mathlib.Topology.Compactification.OnePoint Mathlib.Topology.Compactness.Bases Mathlib.Topology.Compactness.Compact Mathlib.Topology.Compactness.Exterior Mathlib.Topology.Compactness.Lindelof Mathlib.Topology.Compactness.LocallyCompact Mathlib.Topology.Compactness.LocallyFinite Mathlib.Topology.Compactness.Paracompact Mathlib.Topology.Compactness.PseudometrizableLindelof Mathlib.Topology.Compactness.SigmaCompact Mathlib.Topology.Connected.Basic Mathlib.Topology.Connected.Clopen Mathlib.Topology.Connected.LocPathConnected Mathlib.Topology.Connected.LocallyConnected Mathlib.Topology.Connected.PathConnected Mathlib.Topology.Connected.Separation Mathlib.Topology.Connected.TotallyDisconnected Mathlib.Topology.Constructible Mathlib.Topology.Constructions.SumProd Mathlib.Topology.Constructions Mathlib.Topology.ContinuousMap.Basic Mathlib.Topology.ContinuousMap.CocompactMap Mathlib.Topology.ContinuousMap.Interval Mathlib.Topology.ContinuousMap.Ordered Mathlib.Topology.ContinuousMap.SecondCountableSpace Mathlib.Topology.ContinuousMap.Sigma Mathlib.Topology.ContinuousMap.T0Sierpinski Mathlib.Topology.ContinuousOn Mathlib.Topology.Continuous Mathlib.Topology.Covering Mathlib.Topology.Defs.Induced Mathlib.Topology.Defs.Ultrafilter Mathlib.Topology.DenseEmbedding Mathlib.Topology.DerivedSet Mathlib.Topology.DiscreteQuotient Mathlib.Topology.DiscreteSubset Mathlib.Topology.EMetricSpace.Basic Mathlib.Topology.EMetricSpace.Defs Mathlib.Topology.EMetricSpace.Diam Mathlib.Topology.EMetricSpace.Lipschitz Mathlib.Topology.EMetricSpace.Paracompact Mathlib.Topology.EMetricSpace.Pi Mathlib.Topology.ExtendFrom Mathlib.Topology.Exterior Mathlib.Topology.ExtremallyDisconnected Mathlib.Topology.FiberBundle.Basic Mathlib.Topology.FiberBundle.Constructions Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle Mathlib.Topology.FiberBundle.Trivialization Mathlib.Topology.FiberPartition Mathlib.Topology.Filter Mathlib.Topology.GDelta.Basic Mathlib.Topology.GDelta.UniformSpace Mathlib.Topology.Hom.ContinuousEvalConst Mathlib.Topology.Hom.ContinuousEval Mathlib.Topology.Hom.Open Mathlib.Topology.Homeomorph.Defs Mathlib.Topology.Homeomorph.Lemmas Mathlib.Topology.Homotopy.Basic Mathlib.Topology.Homotopy.Contractible Mathlib.Topology.Homotopy.Equiv Mathlib.Topology.Homotopy.HSpaces Mathlib.Topology.Homotopy.Path Mathlib.Topology.Homotopy.Product Mathlib.Topology.IndicatorConstPointwise Mathlib.Topology.Inseparable Mathlib.Topology.Instances.CantorSet Mathlib.Topology.Instances.Discrete Mathlib.Topology.Instances.ENat Mathlib.Topology.Instances.Int Mathlib.Topology.Instances.Nat Mathlib.Topology.Instances.PNat Mathlib.Topology.Instances.Rat Mathlib.Topology.Instances.Shrink Mathlib.Topology.Instances.Sign Mathlib.Topology.Instances.ZMultiples Mathlib.Topology.Irreducible Mathlib.Topology.IsClosedRestrict Mathlib.Topology.IsLocalHomeomorph Mathlib.Topology.JacobsonSpace Mathlib.Topology.KrullDimension Mathlib.Topology.List Mathlib.Topology.LocalAtTarget Mathlib.Topology.LocallyClosed Mathlib.Topology.LocallyConstant.Algebra Mathlib.Topology.LocallyConstant.Basic Mathlib.Topology.LocallyFinite Mathlib.Topology.Maps.Basic Mathlib.Topology.Maps.OpenQuotient Mathlib.Topology.Maps.Proper.Basic Mathlib.Topology.Maps.Proper.UniversallyClosed Mathlib.Topology.MetricSpace.Antilipschitz Mathlib.Topology.MetricSpace.Basic Mathlib.Topology.MetricSpace.Bilipschitz Mathlib.Topology.MetricSpace.Bounded Mathlib.Topology.MetricSpace.CauSeqFilter Mathlib.Topology.MetricSpace.Cauchy Mathlib.Topology.MetricSpace.Congruence Mathlib.Topology.MetricSpace.Defs Mathlib.Topology.MetricSpace.DilationEquiv Mathlib.Topology.MetricSpace.Dilation Mathlib.Topology.MetricSpace.Equicontinuity Mathlib.Topology.MetricSpace.Gluing Mathlib.Topology.MetricSpace.Infsep Mathlib.Topology.MetricSpace.IsometricSMul Mathlib.Topology.MetricSpace.Isometry Mathlib.Topology.MetricSpace.Lipschitz Mathlib.Topology.MetricSpace.MetricSeparated Mathlib.Topology.MetricSpace.ProperSpace.Lemmas Mathlib.Topology.MetricSpace.ProperSpace.Real Mathlib.Topology.MetricSpace.ProperSpace Mathlib.Topology.MetricSpace.Pseudo.Basic Mathlib.Topology.MetricSpace.Pseudo.Constructions Mathlib.Topology.MetricSpace.Pseudo.Defs Mathlib.Topology.MetricSpace.Pseudo.Lemmas Mathlib.Topology.MetricSpace.Pseudo.Pi Mathlib.Topology.MetricSpace.Pseudo.Real Mathlib.Topology.MetricSpace.Sequences Mathlib.Topology.MetricSpace.ShrinkingLemma Mathlib.Topology.MetricSpace.Similarity Mathlib.Topology.MetricSpace.Ultra.Basic Mathlib.Topology.MetricSpace.Ultra.Pi Mathlib.Topology.MetricSpace.Ultra.TotallySeparated Mathlib.Topology.Metrizable.Basic Mathlib.Topology.Metrizable.CompletelyMetrizable Mathlib.Topology.Metrizable.ContinuousMap Mathlib.Topology.Metrizable.Real Mathlib.Topology.Metrizable.Uniformity Mathlib.Topology.Neighborhoods Mathlib.Topology.NhdsSet Mathlib.Topology.NoetherianSpace Mathlib.Topology.OmegaCompletePartialOrder Mathlib.Topology.Order.Basic Mathlib.Topology.Order.Bornology Mathlib.Topology.Order.Compact Mathlib.Topology.Order.CountableSeparating Mathlib.Topology.Order.DenselyOrdered Mathlib.Topology.Order.ExtendFrom Mathlib.Topology.Order.ExtrClosure Mathlib.Topology.Order.Filter Mathlib.Topology.Order.Hom.Basic Mathlib.Topology.Order.Hom.Esakia Mathlib.Topology.Order.IntermediateValue Mathlib.Topology.Order.IsLUB Mathlib.Topology.Order.IsLocallyClosed Mathlib.Topology.Order.Lattice Mathlib.Topology.Order.LawsonTopology Mathlib.Topology.Order.LeftRightLim Mathlib.Topology.Order.LeftRightNhds Mathlib.Topology.Order.LeftRight Mathlib.Topology.Order.LocalExtr Mathlib.Topology.Order.LowerUpperTopology Mathlib.Topology.Order.MonotoneContinuity Mathlib.Topology.Order.MonotoneConvergence Mathlib.Topology.Order.Monotone Mathlib.Topology.Order.NhdsSet Mathlib.Topology.Order.OrderClosedExtr Mathlib.Topology.Order.OrderClosed Mathlib.Topology.Order.PartialSups Mathlib.Topology.Order.Priestley Mathlib.Topology.Order.ProjIcc Mathlib.Topology.Order.Real Mathlib.Topology.Order.Rolle Mathlib.Topology.Order.ScottTopology Mathlib.Topology.Order.T5 Mathlib.Topology.Order.UpperLowerSetTopology Mathlib.Topology.Order Mathlib.Topology.PartialHomeomorph Mathlib.Topology.Partial Mathlib.Topology.Path Mathlib.Topology.Perfect Mathlib.Topology.Piecewise Mathlib.Topology.PreorderRestrict Mathlib.Topology.QuasiSeparated Mathlib.Topology.SeparatedMap Mathlib.Topology.Separation.Basic Mathlib.Topology.Separation.Connected Mathlib.Topology.Separation.CountableSeparatingOn Mathlib.Topology.Separation.DisjointCover Mathlib.Topology.Separation.GDelta Mathlib.Topology.Separation.Hausdorff Mathlib.Topology.Separation.Profinite Mathlib.Topology.Separation.Regular Mathlib.Topology.Separation.SeparatedNhds Mathlib.Topology.Sequences Mathlib.Topology.Sets.Closeds Mathlib.Topology.Sets.Compacts Mathlib.Topology.Sets.OpenCover Mathlib.Topology.Sets.Opens Mathlib.Topology.Sets.Order Mathlib.Topology.ShrinkingLemma Mathlib.Topology.Sober Mathlib.Topology.Spectral.Basic Mathlib.Topology.Spectral.Hom Mathlib.Topology.Spectral.Prespectral Mathlib.Topology.StoneCech Mathlib.Topology.Ultrafilter Mathlib.Topology.UniformSpace.AbsoluteValue Mathlib.Topology.UniformSpace.AbstractCompletion Mathlib.Topology.UniformSpace.Ascoli Mathlib.Topology.UniformSpace.Basic Mathlib.Topology.UniformSpace.Cauchy Mathlib.Topology.UniformSpace.CompactConvergence Mathlib.Topology.UniformSpace.Compact Mathlib.Topology.UniformSpace.CompareReals Mathlib.Topology.UniformSpace.CompleteSeparated Mathlib.Topology.UniformSpace.Completion Mathlib.Topology.UniformSpace.Defs Mathlib.Topology.UniformSpace.DiscreteUniformity Mathlib.Topology.UniformSpace.Equicontinuity Mathlib.Topology.UniformSpace.Equiv Mathlib.Topology.UniformSpace.HeineCantor Mathlib.Topology.UniformSpace.LocallyUniformConvergence Mathlib.Topology.UniformSpace.Matrix Mathlib.Topology.UniformSpace.OfCompactT2 Mathlib.Topology.UniformSpace.OfFun Mathlib.Topology.UniformSpace.Pi Mathlib.Topology.UniformSpace.Real Mathlib.Topology.UniformSpace.Separation Mathlib.Topology.UniformSpace.Ultra.Basic Mathlib.Topology.UniformSpace.Ultra.Constructions Mathlib.Topology.UniformSpace.UniformApproximation Mathlib.Topology.UniformSpace.UniformConvergenceTopology Mathlib.Topology.UniformSpace.UniformConvergence Mathlib.Topology.UniformSpace.UniformEmbedding Mathlib.Topology.UnitInterval	-1
525 files Mathlib.Algebra.BrauerGroup.Defs Mathlib.Algebra.Category.FGModuleCat.Basic Mathlib.Algebra.Category.FGModuleCat.Limits Mathlib.Algebra.Category.Grp.AB Mathlib.Algebra.Category.Grp.Abelian Mathlib.Algebra.Category.Grp.Adjunctions Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.Algebra.Category.Grp.Images Mathlib.Algebra.Category.Grp.Injective Mathlib.Algebra.Category.Grp.IsFinite Mathlib.Algebra.Category.Grp.LargeColimits Mathlib.Algebra.Category.Grp.Subobject Mathlib.Algebra.Category.Grp.Ulift Mathlib.Algebra.Category.ModuleCat.AB Mathlib.Algebra.Category.ModuleCat.Abelian Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.Algebra.Category.ModuleCat.ExteriorPower Mathlib.Algebra.Category.ModuleCat.Free Mathlib.Algebra.Category.ModuleCat.Images Mathlib.Algebra.Category.ModuleCat.Injective Mathlib.Algebra.Category.ModuleCat.Kernels Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono Mathlib.Algebra.Category.ModuleCat.Presheaf.Free Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.Algebra.Category.ModuleCat.Projective Mathlib.Algebra.Category.ModuleCat.Pseudofunctor Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.Algebra.Category.Ring.Constructions Mathlib.Algebra.Category.Ring.Epi Mathlib.Algebra.Category.Ring.FinitePresentation Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Algebra.Category.Ring.Under.Basic Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Algebra.Central.TensorProduct Mathlib.Algebra.EuclideanDomain.Int Mathlib.Algebra.Field.ULift Mathlib.Algebra.Group.Action.Hom Mathlib.Algebra.Group.Action.Opposite Mathlib.Algebra.Group.Action.Pointwise.Set.Basic Mathlib.Algebra.Group.Action.Pretransitive Mathlib.Algebra.Group.Action.Prod Mathlib.Algebra.Group.Action.TypeTags Mathlib.Algebra.Group.Equiv.Opposite Mathlib.Algebra.Group.Even Mathlib.Algebra.Group.Irreducible.Lemmas Mathlib.Algebra.Group.Nat.Even Mathlib.Algebra.Group.Opposite Mathlib.Algebra.Group.PUnit Mathlib.Algebra.Group.Pointwise.Set.Basic Mathlib.Algebra.Group.Pointwise.Set.Lattice Mathlib.Algebra.Group.Pointwise.Set.Scalar Mathlib.Algebra.Group.Prod Mathlib.Algebra.Group.Submonoid.DistribMulAction Mathlib.Algebra.Group.Submonoid.MulOpposite Mathlib.Algebra.Group.Submonoid.Operations Mathlib.Algebra.Group.Subsemigroup.Operations Mathlib.Algebra.Group.Units.Opposite Mathlib.Algebra.GroupWithZero.Action.Defs Mathlib.Algebra.GroupWithZero.Action.End Mathlib.Algebra.GroupWithZero.Action.Opposite Mathlib.Algebra.GroupWithZero.Action.Prod Mathlib.Algebra.GroupWithZero.Action.Units Mathlib.Algebra.GroupWithZero.Opposite Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic Mathlib.Algebra.GroupWithZero.Prod Mathlib.Algebra.GroupWithZero.Units.Lemmas Mathlib.Algebra.Homology.BifunctorAssociator Mathlib.Algebra.Homology.BifunctorFlip Mathlib.Algebra.Homology.BifunctorHomotopy Mathlib.Algebra.Homology.BifunctorShift Mathlib.Algebra.Homology.Bifunctor Mathlib.Algebra.Homology.ComplexShapeSigns Mathlib.Algebra.Homology.ConcreteCategory Mathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass Mathlib.Algebra.Homology.DerivedCategory.Fractions Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.Algebra.Homology.Embedding.CochainComplex Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift Mathlib.Algebra.Homology.HomotopyCategory.HomComplex Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor Mathlib.Algebra.Homology.HomotopyCategory.MappingCone Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence Mathlib.Algebra.Homology.HomotopyCategory.Shift Mathlib.Algebra.Homology.HomotopyCategory.ShortExact Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors Mathlib.Algebra.Homology.HomotopyCategory.Triangulated Mathlib.Algebra.Homology.LocalCohomology Mathlib.Algebra.Homology.Monoidal Mathlib.Algebra.Homology.ShortComplex.Ab Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.Algebra.Homology.TotalComplexShift Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.Algebra.Homology.TotalComplex Mathlib.Algebra.Lie.CartanExists Mathlib.Algebra.Lie.CartanSubalgebra Mathlib.Algebra.Lie.Character Mathlib.Algebra.Lie.Derivation.Killing Mathlib.Algebra.Lie.EngelSubalgebra Mathlib.Algebra.Lie.Engel Mathlib.Algebra.Lie.InvariantForm Mathlib.Algebra.Lie.Killing Mathlib.Algebra.Lie.LieTheorem Mathlib.Algebra.Lie.Nilpotent Mathlib.Algebra.Lie.Rank Mathlib.Algebra.Lie.Semisimple.Basic Mathlib.Algebra.Lie.Semisimple.Defs Mathlib.Algebra.Lie.Semisimple.Lemmas Mathlib.Algebra.Lie.Solvable Mathlib.Algebra.Lie.TraceForm Mathlib.Algebra.Lie.Weights.Basic Mathlib.Algebra.Lie.Weights.Cartan Mathlib.Algebra.Lie.Weights.Chain Mathlib.Algebra.Lie.Weights.Killing Mathlib.Algebra.Lie.Weights.Linear Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.Algebra.Module.CharacterModule Mathlib.Algebra.Module.Defs Mathlib.Algebra.Module.MinimalAxioms Mathlib.Algebra.Module.Opposite Mathlib.Algebra.Module.PID Mathlib.Algebra.Module.PUnit Mathlib.Algebra.Module.PointwisePi Mathlib.Algebra.Module.Prod Mathlib.Algebra.Module.RingHom Mathlib.Algebra.NoZeroSMulDivisors.Defs Mathlib.Algebra.NoZeroSMulDivisors.Pi Mathlib.Algebra.NoZeroSMulDivisors.Prod Mathlib.Algebra.Order.AddGroupWithTop Mathlib.Algebra.Order.Field.Pointwise Mathlib.Algebra.Order.Group.Abs Mathlib.Algebra.Order.Group.Action.Flag Mathlib.Algebra.Order.Group.Basic Mathlib.Algebra.Order.Group.Indicator Mathlib.Algebra.Order.Group.MinMax Mathlib.Algebra.Order.Group.Opposite Mathlib.Algebra.Order.Group.Pointwise.Bounds Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice Mathlib.Algebra.Order.Group.PosPart Mathlib.Algebra.Order.Group.Prod Mathlib.Algebra.Order.Group.Unbundled.Abs Mathlib.Algebra.Order.Group.Unbundled.Int Mathlib.Algebra.Order.Interval.Set.Group Mathlib.Algebra.Order.Kleene Mathlib.Algebra.Order.Monoid.Prod Mathlib.Algebra.Order.Monoid.Unbundled.WithTop Mathlib.Algebra.Order.Monoid.WithTop Mathlib.Algebra.Order.PUnit Mathlib.Algebra.Order.Pi Mathlib.Algebra.Order.Ring.Idempotent Mathlib.Algebra.Order.Ring.Opposite Mathlib.Algebra.Order.Ring.Prod Mathlib.Algebra.Order.Sub.Basic Mathlib.Algebra.Order.Sub.WithTop Mathlib.Algebra.Regular.SMul Mathlib.Algebra.Ring.Action.Basic Mathlib.Algebra.Ring.Action.Field Mathlib.Algebra.Ring.Action.Pointwise.Set Mathlib.Algebra.Ring.Action.Rat Mathlib.Algebra.Ring.CompTypeclasses Mathlib.Algebra.Ring.Equiv Mathlib.Algebra.Ring.Opposite Mathlib.Algebra.Ring.PUnit Mathlib.Algebra.Ring.Pi Mathlib.Algebra.Ring.Pointwise.Set Mathlib.Algebra.Ring.Prod Mathlib.Algebra.Ring.Submonoid.Basic Mathlib.Algebra.Ring.ULift Mathlib.Algebra.Tropical.Basic Mathlib.Algebra.Tropical.Lattice Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.AffineSpace Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.Cover.Over Mathlib.AlgebraicGeometry.Fiber Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.IdealSheaf Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.AlgebraicGeometry.Morphisms.AffineAnd Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.AlgebraicGeometry.Morphisms.Flat Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.AlgebraicGeometry.Over Mathlib.AlgebraicGeometry.PointsPi Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.Pullbacks Mathlib.AlgebraicGeometry.RationalMap Mathlib.AlgebraicGeometry.ResidueField Mathlib.AlgebraicGeometry.Restrict Mathlib.AlgebraicGeometry.Scheme Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.AlgebraicGeometry.Sites.Representability Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski Mathlib.AlgebraicGeometry.Sites.Small Mathlib.AlgebraicGeometry.Spec Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.Stalk Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.Analysis.Convex.Birkhoff Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels Mathlib.Analysis.Normed.Group.SemiNormedGrp Mathlib.CategoryTheory.Abelian.Ext Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite Mathlib.CategoryTheory.Abelian.Injective.Basic Mathlib.CategoryTheory.Abelian.Projective.Basic Mathlib.CategoryTheory.Abelian.Projective.Dimension Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Abelian.Yoneda Mathlib.CategoryTheory.Action Mathlib.CategoryTheory.Galois.Action Mathlib.CategoryTheory.Galois.Basic Mathlib.CategoryTheory.Galois.Decomposition Mathlib.CategoryTheory.Galois.EssSurj Mathlib.CategoryTheory.Galois.Examples Mathlib.CategoryTheory.Galois.Full Mathlib.CategoryTheory.Galois.GaloisObjects Mathlib.CategoryTheory.Galois.IsFundamentalgroup Mathlib.CategoryTheory.Galois.Prorepresentability Mathlib.CategoryTheory.Galois.Topology Mathlib.CategoryTheory.Localization.Triangulated Mathlib.CategoryTheory.Preadditive.HomOrthogonal Mathlib.CategoryTheory.Preadditive.Schur Mathlib.CategoryTheory.Preadditive.Yoneda.Injective Mathlib.CategoryTheory.Preadditive.Yoneda.Limits Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.CategoryTheory.Triangulated.Adjunction Mathlib.CategoryTheory.Triangulated.Functor Mathlib.CategoryTheory.Triangulated.HomologicalFunctor Mathlib.CategoryTheory.Triangulated.Opposite.Functor Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated Mathlib.CategoryTheory.Triangulated.Pretriangulated Mathlib.CategoryTheory.Triangulated.Subcategory Mathlib.CategoryTheory.Triangulated.TStructure.Basic Mathlib.CategoryTheory.Triangulated.TriangleShift Mathlib.CategoryTheory.Triangulated.Triangulated Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.Combinatorics.Configuration Mathlib.Condensed.AB Mathlib.Condensed.Basic Mathlib.Condensed.CartesianClosed Mathlib.Condensed.Discrete.Basic Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Colimit Mathlib.Condensed.Discrete.LocallyConstant Mathlib.Condensed.Discrete.Module Mathlib.Condensed.Epi Mathlib.Condensed.Equivalence Mathlib.Condensed.Explicit Mathlib.Condensed.Functors Mathlib.Condensed.Light.AB Mathlib.Condensed.Light.Basic Mathlib.Condensed.Light.CartesianClosed Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.Functors Mathlib.Condensed.Light.Limits Mathlib.Condensed.Light.Module Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.Limits Mathlib.Condensed.Module Mathlib.Condensed.Solid Mathlib.Condensed.TopCatAdjunction Mathlib.Condensed.TopComparison Mathlib.Data.Int.Cast.Prod Mathlib.Data.Nat.Cast.Prod Mathlib.Data.Nat.Cast.WithTop Mathlib.Data.Nat.Upto Mathlib.FieldTheory.AxGrothendieck Mathlib.FieldTheory.Galois.Profinite Mathlib.FieldTheory.LinearDisjoint Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.GroupTheory.Congruence.Basic Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.GroupTheory.FreeGroup.NielsenSchreier Mathlib.GroupTheory.GroupAction.DomAct.ActionHom Mathlib.GroupTheory.GroupAction.DomAct.Basic Mathlib.GroupTheory.GroupAction.Embedding Mathlib.GroupTheory.GroupAction.Hom Mathlib.GroupTheory.GroupAction.Pointwise Mathlib.GroupTheory.GroupAction.Ring Mathlib.GroupTheory.GroupAction.Support Mathlib.GroupTheory.Submonoid.Center Mathlib.GroupTheory.Submonoid.Centralizer Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory Mathlib.LinearAlgebra.LinearDisjoint Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat Mathlib.ModelTheory.Algebra.Field.IsAlgClosed Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.NumberTheory.Cyclotomic.PID Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.NumberTheory.Cyclotomic.Three Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.NumberTheory.FLT.Three Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.NumberTheory.MulChar.Duality Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.ProductFormula Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.NumberTheory.RamificationInertia.Galois Mathlib.Order.Filter.AtTopBot.Field Mathlib.Order.Filter.AtTopBot.Group Mathlib.Order.Filter.AtTopBot.Ring Mathlib.RepresentationTheory.Character Mathlib.RepresentationTheory.FDRep Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.RepresentationTheory.GroupCohomology.Functoriality Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.RepresentationTheory.Invariants Mathlib.RepresentationTheory.Rep Mathlib.RepresentationTheory.Tannaka Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.RingTheory.Congruence.Basic Mathlib.RingTheory.Congruence.Opposite Mathlib.RingTheory.DedekindDomain.Different Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.RingTheory.DedekindDomain.PID Mathlib.RingTheory.Etale.Field Mathlib.RingTheory.Etale.Kaehler Mathlib.RingTheory.Flat.Basic Mathlib.RingTheory.Flat.CategoryTheory Mathlib.RingTheory.Flat.Domain Mathlib.RingTheory.Flat.Equalizer Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra Mathlib.RingTheory.Flat.FaithfullyFlat.Basic Mathlib.RingTheory.Flat.Localization Mathlib.RingTheory.Flat.Stability Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.RingTheory.Frobenius Mathlib.RingTheory.Ideal.GoingDown Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.RingTheory.Invariant Mathlib.RingTheory.LinearDisjoint Mathlib.RingTheory.LocalProperties.Basic Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.RingTheory.LocalProperties.Reduced Mathlib.RingTheory.LocalRing.Module Mathlib.RingTheory.Localization.Finiteness Mathlib.RingTheory.Localization.Free Mathlib.RingTheory.Morita.Basic Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.RingTheory.Regular.RegularSequence Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.RingTheory.RingHom.FiniteType Mathlib.RingTheory.RingHom.Finite Mathlib.RingTheory.RingHom.Flat Mathlib.RingTheory.RingHom.Injective Mathlib.RingTheory.RingHom.Integral Mathlib.RingTheory.RingHom.Locally Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.RingTheory.RingHom.Surjective Mathlib.RingTheory.RingHom.Unramified Mathlib.RingTheory.RingHomProperties Mathlib.RingTheory.RingInvo Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Smooth.Locus Mathlib.RingTheory.Spectrum.Prime.Chevalley Mathlib.RingTheory.Spectrum.Prime.FreeLocus Mathlib.RingTheory.Spectrum.Prime.Homeomorph Mathlib.RingTheory.Spectrum.Prime.Module Mathlib.RingTheory.Support Mathlib.RingTheory.TensorProduct.Nontrivial Mathlib.RingTheory.Trace.Quotient Mathlib.RingTheory.Unramified.Field Mathlib.RingTheory.Unramified.Finite Mathlib.RingTheory.Unramified.LocalRing Mathlib.RingTheory.Unramified.Locus Mathlib.Tactic.Linter.MinImports Mathlib.Tactic.Linter.UpstreamableDecl Mathlib.Tactic.Linter Mathlib.Tactic.MinImports Mathlib.Tactic.Monotonicity.Lemmas Mathlib.Tactic.Monotonicity Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous Mathlib.Topology.CWComplex.Abstract.Basic Mathlib.Topology.Category.CompHaus.Basic Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.Topology.Category.CompHaus.Frm Mathlib.Topology.Category.CompHaus.Limits Mathlib.Topology.Category.CompHaus.Projective Mathlib.Topology.Category.CompactlyGenerated Mathlib.Topology.Category.Compactum Mathlib.Topology.Category.DeltaGenerated Mathlib.Topology.Category.LightProfinite.AsLimit Mathlib.Topology.Category.LightProfinite.Basic Mathlib.Topology.Category.LightProfinite.EffectiveEpi Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Topology.Category.LightProfinite.Limits Mathlib.Topology.Category.LightProfinite.Sequence Mathlib.Topology.Category.Locale Mathlib.Topology.Category.Profinite.AsLimit Mathlib.Topology.Category.Profinite.Basic Mathlib.Topology.Category.Profinite.CofilteredLimit Mathlib.Topology.Category.Profinite.EffectiveEpi Mathlib.Topology.Category.Profinite.Extend Mathlib.Topology.Category.Profinite.Limits Mathlib.Topology.Category.Profinite.Nobeling.Basic Mathlib.Topology.Category.Profinite.Nobeling.Induction Mathlib.Topology.Category.Profinite.Nobeling.Span Mathlib.Topology.Category.Profinite.Nobeling.Successor Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit Mathlib.Topology.Category.Profinite.Nobeling Mathlib.Topology.Category.Profinite.Product Mathlib.Topology.Category.Profinite.Projective Mathlib.Topology.Category.Stonean.Adjunctions Mathlib.Topology.Category.Stonean.Basic Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Topology.Category.Stonean.Limits Mathlib.Topology.Compactness.CompactlyGeneratedSpace Mathlib.Topology.Maps.Proper.CompactlyGenerated Mathlib.Topology.Order.Category.FrameAdjunction Mathlib.Topology.Sheaves.CommRingCat Mathlib.Topology.Sheaves.MayerVietoris	1
Mathlib.Algebra.Ring.GrindInstances (new file)	133

---

Declarations diff

+ CommRing.toGrindCommRing
+ CommRing.toGrindCommRing_ofNat
+ _root_.Lean.SearchPath.relativize
+ instance (X : Type u) [TopologicalSpace X] [Small.{v} X] :
+ instance (α : Type*) [CommRing α] (n : ℕ) [CharP α n] : Lean.Grind.IsCharP α n
+ instance [NormedField 𝕜] [NormedCommRing R] [NormedAlgebra 𝕜 R] :
+ merge_isAssociative
+ merge_isCommutative
+ merge_isId
+ merge_isIdempotent
++-- toAffine
- Lean.Expr.LiftLetsConfig
- Lean.Expr.liftLets
- Lean.MVarId.extractLets
- Lean.MVarId.extractLetsAt
- One
- WellFounded.fixF_eq
- _
- _root_.Lean.LOption.toOption
- a
- add_emod_left
- add_emod_right
- add_eq_left
- add_eq_max_iff
- add_eq_min_iff
- add_eq_one_iff
- add_eq_right
- add_eq_three_iff
- add_eq_two_iff
- add_eq_zero
- add_le_iff_le_sub
- add_le_mul
- add_le_zero_iff_le_neg
- add_le_zero_iff_le_neg'
- add_left_inj
- add_mod_eq_add_mod_left
- add_mod_eq_add_mod_right
- add_mod_eq_ite
- add_mul_emod_self_right
- add_nonnneg_iff_neg_le
- add_nonnneg_iff_neg_le'
- add_pos_iff_pos_or_pos
- add_right_inj
- add_sub_one_le_mul
- add_sub_sub_cancel
- add_succ_lt_add
- add_succ_sub_one
- bind_eq_some_iff
- cast_id
- coe_lcm_dvd
- decidableEqNone
- decidableExistsMem
- decidableForallMem
- default_eq_zero
- div_add_mod'
- div_div_div_eq_div
- div_div_self
- div_dvd_of_dvd
- div_eq_iff_eq_of_dvd_dvd
- div_eq_self
- div_eq_sub_mod_div
- div_eq_zero_iff
- div_le_div
- div_le_div_of_mul_le_mul
- div_le_div_right
- div_le_iff_le_mul_add_pred
- div_le_iff_le_mul_of_dvd
- div_left_inj
- div_lt_div_left
- div_lt_div_of_lt_of_dvd
- div_lt_div_right
- div_lt_one_iff
- div_mod_unique
- div_mul_div_comm
- div_mul_div_le
- div_mul_div_le_div
- div_mul_right_comm
- div_ne_zero_iff
- div_ne_zero_iff_of_dvd
- div_pos_iff
- div_pow
- dvd_add_left
- dvd_add_right
- dvd_coe_gcd
- dvd_div_iff_mul_dvd
- dvd_div_of_mul_dvd
- dvd_gcd
- dvd_iff_div_mul_eq
- dvd_iff_dvd_dvd
- dvd_iff_le_div_mul
- dvd_of_mul_dvd_mul_left
- dvd_of_mul_dvd_mul_right
- dvd_self_sub_of_emod_eq
- dvd_sub_mod
- ediv_dvd_ediv
- ediv_dvd_of_dvd
- eq_div_iff_mul_eq_left
- eq_div_of_mul_eq_left
- eq_div_of_mul_eq_right
- eq_mul_of_div_eq_left
- eq_none_iff_forall_some_ne
- eq_none_or_eq_some
- eq_of_dvd_of_div_eq_one
- eq_of_dvd_of_lt_two_mul
- eq_one_of_mul_eq_one_left
- eq_one_of_mul_eq_one_right
- eq_or_mem_of_mem_cons
- eq_sub_of_add_eq
- eq_sub_of_add_eq'
- eq_zero_of_dvd_of_div_eq_zero
- eq_zero_of_dvd_of_lt
- eq_zero_of_le_div
- eq_zero_of_mul_le
- evalExtractLets
- exists_ne_none
- forall_ne_none
- gcd_assoc
- gcd_comm
- gcd_dvd_gcd_mul_left_right
- gcd_dvd_gcd_mul_right_right
- gcd_dvd_gcd_of_dvd_left
- gcd_dvd_gcd_of_dvd_right
- gcd_eq_left
- gcd_eq_right
- gcd_eq_zero_iff
- gcd_mul_lcm
- gcd_mul_left
- gcd_mul_right
- gcd_natCast_natCast
- gcd_pos_iff
- gcd_pos_of_ne_zero_left
- gcd_pos_of_ne_zero_right
- gcd_self
- gcd_zero_left
- gcd_zero_right
- ge_of_eq
- getLast_cons_cons
- instance (X : Type u) [TopologicalSpace X] [Small.{v} X] : TopologicalSpace (Shrink.{v} X)
- instance (priority := 200) One.ofOfNat1 {α} [OfNat α (nat_lit 1)] : One α
- instance (priority := 300) One.toOfNat1 {α} [One α] : OfNat α (nat_lit 1)
- instance : Pow (BitVec w) ℕ := ⟨fun x n => ofFin <| x.toFin ^ n⟩
- instance [NormedField 𝕜] [NormedCommRing R] [NormedAlgebra 𝕜 R] : NormedSpace 𝕜 C(α, R)₀
- isNone_eq_false_iff
- lawfulIdentity_merge
- lcm_assoc
- lcm_comm
- lcm_dvd
- lcm_dvd_iff
- lcm_dvd_mul
- lcm_one_left
- lcm_one_right
- lcm_pos
- lcm_zero_left
- lcm_zero_right
- le_add_iff_sub_le
- le_add_pred_of_pos
- le_and_le_add_one_iff
- le_antisymm_iff
- le_iff_eq_or_lt
- le_iff_lt_or_eq
- le_iff_ne_zero_of_dvd
- le_mul_self
- le_of_eq
- le_of_lt_add_of_dvd
- le_of_pred_lt
- le_one_iff_eq_zero_or_eq_one
- le_or_le_of_add_eq_add_pred
- le_or_lt
- le_rfl
- le_self_pow
- le_sub_one_iff
- le_succ_iff
- lt_asymm
- lt_div_iff_mul_lt'
- lt_div_iff_mul_lt_of_dvd
- lt_div_mul_add
- lt_iff_add_one_le
- lt_iff_le_pred
- lt_iff_lt_of_mul_eq_mul
- lt_mul_div_succ
- lt_mul_iff_one_lt_left
- lt_mul_iff_one_lt_right
- lt_mul_of_div_lt
- lt_mul_self_iff
- lt_of_div_lt_div
- lt_of_lt_pred
- lt_of_pow_dvd_right
- lt_of_toNat_lt
- lt_one_add_iff
- lt_or_le
- lt_or_lt_of_ne
- lt_pred_iff
- lt_sub_iff_add_lt
- lt_sub_iff_add_lt'
- lt_toNat
- map_eq_none_iff
- map_eq_some_iff
- max_eq_zero_iff
- max_left_comm
- max_right_comm
- mem_some_iff
- min_eq_zero_iff
- min_left_comm
- min_right_comm
- mod_add_div'
- mod_eq_iff_lt
- mod_succ
- mod_succ_eq_iff_lt
- mod_two_ne_one
- mod_two_ne_zero
- mod_two_not_eq_one
- mod_two_not_eq_zero
- mul_add_mod'
- mul_add_mod_of_lt
- mul_add_mul_div_of_dvd
- mul_div_cancel_left'
- mul_div_eq_iff_dvd
- mul_div_le_mul_div_assoc
- mul_div_lt_iff_not_dvd
- mul_div_mul_comm
- mul_div_right_comm
- mul_dvd_mul
- mul_dvd_mul_iff_left
- mul_dvd_mul_iff_right
- mul_dvd_mul_left
- mul_dvd_mul_right
- mul_dvd_of_dvd_div
- mul_eq_left
- mul_eq_right
- mul_le_mul_iff_of_pos_right
- mul_le_mul_left
- mul_le_mul_left_of_neg
- mul_le_mul_right
- mul_le_mul_right_of_neg
- mul_le_of_le_div
- mul_left_inj
- mul_lt_mul''
- mul_lt_mul_left
- mul_lt_mul_left_of_neg
- mul_lt_mul_pow_succ
- mul_lt_mul_right
- mul_lt_mul_right_of_neg
- mul_ne_mul_left
- mul_ne_mul_right
- mul_nonneg_iff_of_pos_right
- mul_right_inj
- mul_self_inj
- mul_self_le_mul_self
- mul_self_le_mul_self_iff
- mul_self_lt_mul_self
- mul_self_lt_mul_self_iff
- mul_sub_div_of_dvd
- mul_sub_mul_div_of_dvd
- natAbs_add_of_nonneg
- natAbs_add_of_nonpos
- natAbs_cast
- natAbs_ediv_of_dvd
- natAbs_eq_of_dvd_dvd
- natAbs_natCast
- natAbs_ofNat'
- natAbs_pow
- natAbs_pow_two
- natAbs_sign_of_ne_zero
- natCast_ediv
- natCast_emod
- natCast_eq_zero
- natCast_inj
- natCast_ne_zero
- natCast_ne_zero_iff_pos
- natCast_nonneg
- natCast_nonpos_iff
- natCast_pos
- natCast_sub
- natCast_succ_pos
- neg_emod_two
- neg_neg_iff_pos
- neg_nonneg
- neg_one_eq_allOnes
- neg_pos
- not_dvd_iff_lt_mul_succ
- not_dvd_of_pos_of_lt
- not_succ_lt_self
- ofNat_add_one_out
- ofNat_add_out
- ofNat_eq_natCast
- ofNat_mul_out
- one_add_le_iff
- one_le_div_iff
- one_le_iff_ne_zero
- one_le_of_lt
- one_le_pow
- one_lt_iff_ne_zero_and_ne_one
- one_lt_mul_iff
- one_lt_pow
- one_lt_pow'
- one_lt_pow_iff
- one_lt_succ_succ
- one_lt_two_pow'
- one_mod
- one_mod_eq_one
- one_ne_zero
- one_nonneg
- one_pos
- pbind_eq_bind
- pbind_eq_some
- pbind_map
- pow_dvd_pow_iff
- pow_eq_one
- pow_eq_self_iff
- pow_eq_zero
- pow_le_one_iff
- pow_le_pow_iff_left
- pow_lt_pow_iff_left
- pow_lt_pow_right
- pow_mod
- pow_pos_iff
- pow_right_inj
- pow_self_mul_pow_self_le
- pow_self_pos
- pow_two_sub_pow_two
- pred_add_self
- pred_eq_of_eq_succ
- pred_eq_self_iff
- pred_eq_succ_iff
- pred_le_iff
- pred_one_add
- pred_sub
- self_add_pred
- self_add_sub_one
- sign_natCast_add_one
- sign_natCast_of_ne_zero
- sub_add_sub_cancel
- sub_emod_right
- sub_eq_of_eq_add'
- sub_lt_iff_lt_add
- sub_lt_iff_lt_add'
- sub_lt_sub_iff_right
- sub_mod_eq_zero_of_mod_eq
- sub_nonneg
- sub_one_add_self
- sub_one_lt_iff
- sub_pos
- sub_sub_sub_cancel_right
- sub_succ'
- succ_add_sub_one
- succ_inj
- succ_le_iff
- succ_mul_pos
- succ_ne_succ
- succ_succ_ne_one
- toNat_natCast
- toNat_natCast_add_one
- toNat_sub_of_le
- two_mul
- two_pow_succ
- zero_eq_mul
-+- div_dvd_iff_dvd_mul
-+-+ iic
-+-+-+-+ colimitCoconeIsColimit
-- lcm_mul_left
-- lcm_mul_right
-- le_add_one_iff
--+ dvd_mul_of_div_dvd

You can run this locally as follows

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

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

The doc-module for script/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (4.00, 0.03)

Current number	Change	Type
125	4	adaptation notes

Current commit 1b64f60681
Reference commit 27c67e7a64

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

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

[jcommelin]

bors d+

[jcommelin]

Suggested change

	require "leanprover-community" / "batteries" @ git "lean-pr-testing-8161"
	require "leanprover-community" / "batteries" @ git "nightly-testing"

[mathlib-bors]

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