[Merged by Bors] - chore(Data/Multiset/Basic): move the `sub`, `union`, `inter` sections lower #19863

YaelDillies · 2024-12-10T11:59:30Z

Move the sections about sub, union and inter under the sections about count and filter
Multiset.countP_sub now has a different argument order to match List.countP_diff
Golf List.count_sub
Name the instances and declare them using where notation
Define Multiset.card using Quotient.lift, not Quotient.liftOn

depends on: [Merged by Bors] - chore(Multiset): make all arguments to inter_le_left, etc... implicit #20045

github-actions · 2024-12-10T12:00:24Z

PR summary df14c3cf54

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Multiset.Basic	370	371	+1 (+0.27%)

Import changes for all files

Files	Import difference
2142 files `Mathlib.Algebra.Homology.ShortComplex.Ab` `Mathlib.Data.Matroid.Basic` `Mathlib.Algebra.Ring.Subring.MulOpposite` `Mathlib.Order.Partition.Equipartition` `Mathlib.CategoryTheory.Preadditive.Yoneda.Projective` `Mathlib.Algebra.Polynomial.FieldDivision` `Mathlib.Topology.Algebra.Monoid` `Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing` `Mathlib.Algebra.Star.Module` `Mathlib.RingTheory.Localization.Away.Lemmas` `Mathlib.Algebra.Module.Submodule.Bilinear` `Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology` `Mathlib.Algebra.Polynomial.Degree.Support` `Mathlib.CategoryTheory.Generator.Sheaf` `Mathlib.Algebra.Star.NonUnitalSubalgebra` `Mathlib.Topology.Order.LawsonTopology` `Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian` `Mathlib.Topology.Algebra.InfiniteSum.Group` `Mathlib.LinearAlgebra.Countable` `Mathlib.CategoryTheory.Limits.Constructions.Filtered` `Mathlib.Combinatorics.Additive.ETransform` `Mathlib.Algebra.BigOperators.Sym` `Mathlib.LinearAlgebra.BilinearMap` `Mathlib.Data.Nat.Choose.Cast` `Mathlib.Data.DFinsupp.Defs` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer` `Mathlib.Order.Filter.AtTopBot.ModEq` `Mathlib.Data.Multiset.Sum` `Mathlib.RingTheory.Henselian` `Mathlib.RingTheory.Algebraic.LinearIndependent` `Mathlib.RingTheory.HahnSeries.Basic` `Mathlib.NumberTheory.Padics.PadicNorm` `Mathlib.Topology.Instances.Nat` `Mathlib.CategoryTheory.Sites.Pullback` `Mathlib.Combinatorics.SetFamily.FourFunctions` `Mathlib.RingTheory.Finiteness.Bilinear` `Mathlib.RingTheory.Polynomial.Content` `Mathlib.Topology.Algebra.Semigroup` `Mathlib.RingTheory.Localization.AtPrime` `Mathlib.MeasureTheory.MeasurableSpace.Embedding` `Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs` `Mathlib.Topology.CompactOpen` `Mathlib.Algebra.Symmetrized` `Mathlib.RingTheory.Ideal.Span` `Mathlib.Algebra.Lie.Normalizer` `Mathlib.GroupTheory.Coset.Card` `Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative` `Mathlib.LinearAlgebra.Span.Basic` `Mathlib.ModelTheory.Ultraproducts` `Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject` `Mathlib.Data.Multiset.Nodup` `Mathlib.CategoryTheory.Abelian.RightDerived` `Mathlib.RingTheory.AlgebraTower` `Mathlib.Data.Matrix.Auto` `Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits` `Mathlib.Combinatorics.Enumerative.InclusionExclusion` `Mathlib.CategoryTheory.Shift.InducedShiftSequence` `Mathlib.CategoryTheory.Sites.Coherent.Comparison` `Mathlib.Topology.IndicatorConstPointwise` `Mathlib.Data.Finset.PiInduction` `Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four` `Mathlib.LinearAlgebra.DirectSum.Finsupp` `Mathlib.Algebra.Category.ModuleCat.Limits` `Mathlib.GroupTheory.Submonoid.Inverses` `Mathlib.Algebra.Homology.ShortComplex.RightHomology` `Mathlib.Topology.ContinuousMap.Ordered` `Mathlib.Algebra.BigOperators.Finsupp` `Mathlib.Algebra.BigOperators.RingEquiv` `Mathlib.Data.Finset.Interval` `Mathlib.CategoryTheory.Abelian.Pseudoelements` `Mathlib.Topology.MetricSpace.Antilipschitz` `Mathlib.RingTheory.Noetherian.Orzech` `Mathlib.GroupTheory.CoprodI` `Mathlib.Data.Fintype.Fin` `Mathlib.Combinatorics.SimpleGraph.Maps` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square` `Mathlib.RingTheory.SimpleModule` `Mathlib.Algebra.Category.FGModuleCat.Limits` `Mathlib.RingTheory.IsPrimary` `Mathlib.CategoryTheory.Limits.Shapes.KernelPair` `Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph` `Mathlib.Data.Fintype.Sum` `Mathlib.SetTheory.Ordinal.NaturalOps` `Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue` `Mathlib.Data.Multiset.NatAntidiagonal` `Mathlib.Order.Disjointed` `Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem` `Mathlib.CategoryTheory.FintypeCat` `Mathlib.Analysis.Polynomial.CauchyBound` `Mathlib.Algebra.GradedMonoid` `Mathlib.Data.Fintype.Powerset` `Mathlib.Algebra.Polynomial.Degree.Definitions` `Mathlib.Algebra.IsPrimePow` `Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms` `Mathlib.RingTheory.Polynomial.Ideal` `Mathlib.Data.W.Cardinal` `Mathlib.RingTheory.Lasker` `Mathlib.NumberTheory.Multiplicity` `Mathlib.Topology.DerivedSet` `Mathlib.RingTheory.PowerSeries.WellKnown` `Mathlib.Combinatorics.Enumerative.DoubleCounting` `Mathlib.Algebra.Polynomial.Degree.Operations` `Mathlib.Data.Multiset.Sym` `Mathlib.LinearAlgebra.Projection` `Mathlib.Combinatorics.Enumerative.DyckWord` `Mathlib.Algebra.Order.GroupWithZero.Finset` `Mathlib.Algebra.Category.Grp.EpiMono` `Mathlib.Algebra.Homology.Opposite` `Mathlib.CategoryTheory.Adjunction.Additive` `Mathlib.Algebra.Module.Bimodule` `Mathlib.Algebra.Module.Submodule.Invariant` `Mathlib.Deprecated.Cardinal.PartENat` `Mathlib.LinearAlgebra.SModEq` `Mathlib.Data.NNRat.BigOperators` `Mathlib.Algebra.Order.Interval.Basic` `Mathlib.CategoryTheory.Sites.SheafHom` `Mathlib.Order.Filter.SmallSets` `Mathlib.Algebra.Category.Grp.Subobject` `Mathlib.CategoryTheory.Action.Continuous` `Mathlib.Order.Filter.CountablyGenerated` `Mathlib.Algebra.Star.Pointwise` `Mathlib.Algebra.Category.Grp.AB` `Mathlib.Order.OrderIsoNat` `Mathlib.Data.Finset.Grade` `Mathlib.Tactic.Positivity.Finset` `Mathlib.Topology.DiscreteSubset` `Mathlib.Combinatorics.Additive.DoublingConst` `Mathlib.Topology.Compactification.OnePoint` `Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct` `Mathlib.Topology.Instances.PNat` `Mathlib.Analysis.Normed.Lp.WithLp` `Mathlib.Combinatorics.SimpleGraph.LineGraph` `Mathlib.CategoryTheory.Sites.MorphismProperty` `Mathlib.Topology.DenseEmbedding` `Mathlib.LinearAlgebra.AffineSpace.Ordered` `Mathlib.Algebra.Homology.Functor` `Mathlib.Topology.UniformSpace.OfCompactT2` `Mathlib.Algebra.Colimit.TensorProduct` `Mathlib.Algebra.Module.Submodule.Basic` `Mathlib.NumberTheory.Primorial` `Mathlib.Algebra.Homology.ShortComplex.SnakeLemma` `Mathlib.Deprecated.Cardinal.Finite` `Mathlib.Tactic.IntervalCases` `Mathlib.Order.BooleanSubalgebra` `Mathlib.Algebra.Category.Ring.Instances` `Mathlib.LinearAlgebra.Finsupp.Supported` `Mathlib.Data.Nat.Nth` `Mathlib.Order.Filter.Bases` `Mathlib.Data.NNReal.Basic` `Mathlib.Data.Set.Finite.List` `Mathlib.Data.Finsupp.Basic` `Mathlib.Algebra.Lie.Quotient` `Mathlib.RingTheory.AlgebraicIndependent.Transcendental` `Mathlib.Algebra.Category.CoalgebraCat.ComonEquivalence` `Mathlib.LinearAlgebra.Dimension.DivisionRing` `Mathlib.Data.DFinsupp.Multiset` `Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts` `Mathlib.LinearAlgebra.FreeModule.StrongRankCondition` `Mathlib.Algebra.Module.Presentation.Tensor` `Mathlib.Topology.UniformSpace.Ascoli` `Mathlib.LinearAlgebra.BilinearForm.DualLattice` `Mathlib.Topology.UniformSpace.Compact` `Mathlib.Algebra.Category.ModuleCat.Abelian` `Mathlib.Topology.MetricSpace.ShrinkingLemma` `Mathlib.Data.SetLike.Fintype` `Mathlib.Combinatorics.SimpleGraph.Clique` `Mathlib.RingTheory.Ideal.IsPrincipal` `Mathlib.CategoryTheory.Limits.TypesFiltered` `Mathlib.Topology.Order.Lattice` `Mathlib.Algebra.Order.BigOperators.Ring.Finset` `Mathlib.CategoryTheory.Abelian.Ext` `Mathlib.Algebra.Category.ModuleCat.AB` `Mathlib.Topology.Sheaves.Sheaf` `Mathlib.Data.W.Constructions` `Mathlib.Data.Set.Countable` `Mathlib.Data.FinEnum` `Mathlib.Algebra.Polynomial.Degree.Monomial` `Mathlib.Data.Multiset.Antidiagonal` `Mathlib.Topology.Partial` `Mathlib.Algebra.Homology.Additive` `Mathlib.RingTheory.GradedAlgebra.Noetherian` `Mathlib.Order.CountableDenseLinearOrder` `Mathlib.MeasureTheory.MeasurableSpace.Defs` `Mathlib.Data.Vector3` `Mathlib.CategoryTheory.Sites.ChosenFiniteProducts` `Mathlib.Combinatorics.SimpleGraph.StronglyRegular` `Mathlib.Algebra.Ring.Subring.Pointwise` `Mathlib.SetTheory.Cardinal.Arithmetic` `Mathlib.RingTheory.HahnSeries.Addition` `Mathlib.Data.Nat.Factorial.DoubleFactorial` `Mathlib.CategoryTheory.Abelian.FunctorCategory` `Mathlib.RingTheory.QuotSMulTop` `Mathlib.RingTheory.TwoSidedIdeal.BigOperators` `Mathlib.Topology.Algebra.Group.OpenMapping` `Mathlib.Data.Fin.Tuple.Finset` `Mathlib.Data.QPF.Multivariate.Basic` `Mathlib.Data.Finsupp.PWO` `Mathlib.Algebra.Category.ModuleCat.Kernels` `Mathlib.Algebra.Homology.Embedding.HomEquiv` `Mathlib.RingTheory.Valuation.ExtendToLocalization` `Mathlib.LinearAlgebra.Dimension.Localization` `Mathlib.LinearAlgebra.Finsupp.VectorSpace` `Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage` `Mathlib.Data.Finset.Option` `Mathlib.Data.Fintype.Quotient` `Mathlib.ModelTheory.PartialEquiv` `Mathlib.RingTheory.AdicCompletion.Basic` `Mathlib.CategoryTheory.Localization.FiniteProducts` `Mathlib.Data.Matrix.Invertible` `Mathlib.Topology.Instances.Int` `Mathlib.Data.Finset.Lattice.Fold` `Mathlib.Algebra.Ring.Subring.IntPolynomial` `Mathlib.Geometry.Group.Growth.QuotientInter` `Mathlib.RingTheory.TensorProduct.Finite` `Mathlib.RingTheory.Prime` `Mathlib.Topology.MetricSpace.Pseudo.Real` `Mathlib.Logic.Hydra` `Mathlib.LinearAlgebra.Coevaluation` `Mathlib.CategoryTheory.Subobject.Limits` `Mathlib.Algebra.Lie.Submodule` `Mathlib.CategoryTheory.Monoidal.Linear` `Mathlib.AlgebraicTopology.SimplicialSet.Basic` `Mathlib.Data.Matrix.Composition` `Mathlib.RingTheory.Ideal.Maps` `Mathlib.Algebra.DirectSum.Module` `Mathlib.GroupTheory.DoubleCoset` `Mathlib.CategoryTheory.Quotient.Preadditive` `Mathlib.Order.CompleteSublattice` `Mathlib.GroupTheory.Perm.Sign` `Mathlib.Topology.Algebra.Ring.Basic` `Mathlib.Topology.FiberBundle.Constructions` `Mathlib.LinearAlgebra.Matrix.Diagonal` `Mathlib.Data.Matrix.Basic` `Mathlib.Combinatorics.Hall.Basic` `Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal` `Mathlib.RingTheory.Multiplicity` `Mathlib.RingTheory.Derivation.Lie` `Mathlib.RingTheory.Polynomial.Pochhammer` `Mathlib.Data.Matrix.Basis` `Mathlib.RingTheory.MvPowerSeries.LexOrder` `Mathlib.RingTheory.Algebraic.MvPolynomial` `Mathlib.Topology.Sets.Closeds` `Mathlib.Algebra.Polynomial.SpecificDegree` `Mathlib.Algebra.MvPolynomial.Counit` `Mathlib.LinearAlgebra.Eigenspace.Matrix` `Mathlib.Algebra.Ring.Subsemiring.MulOpposite` `Mathlib.Topology.Order.ScottTopology` `Mathlib.Data.Multiset.Functor` `Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid` `Mathlib.RingTheory.FractionalIdeal.Extended` `Mathlib.Algebra.Module.BigOperators` `Mathlib.Algebra.Homology.Embedding.IsSupported` `Mathlib.RingTheory.Finiteness.Nakayama` `Mathlib.Algebra.MvPolynomial.Basic` `Mathlib.SetTheory.Ordinal.Notation` `Mathlib.Algebra.Category.ModuleCat.ChangeOfRings` `Mathlib.NumberTheory.ArithmeticFunction` `Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures` `Mathlib.GroupTheory.Coxeter.Matrix` `Mathlib.LinearAlgebra.AffineSpace.Pointwise` `Mathlib.Algebra.ContinuedFractions.Computation.Approximations` `Mathlib.Topology.Instances.ZMod` `Mathlib.Topology.Order.OrderClosedExtr` `Mathlib.Data.Finset.Defs` `Mathlib.Algebra.Polynomial.AlgebraMap` `Mathlib.RingTheory.Polynomial.Quotient` `Mathlib.Topology.ExtremallyDisconnected` `Mathlib.CategoryTheory.MorphismProperty.Representable` `Mathlib.Topology.Category.TopCat.EpiMono` `Mathlib.Order.Interval.Finset.Fin` `Mathlib.Algebra.CharP.LocalRing` `Mathlib.Algebra.Category.ModuleCat.Adjunctions` `Mathlib.Topology.Sheaves.SheafCondition.Sites` `Mathlib.CategoryTheory.Abelian.Transfer` `Mathlib.Combinatorics.Additive.SmallTripling` `Mathlib.Data.Matroid.Map` `Mathlib.CategoryTheory.Monad.Monadicity` `Mathlib.Algebra.Polynomial.Eval.Irreducible` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits` `Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits` `Mathlib.Data.Finsupp.Notation` `Mathlib.CategoryTheory.SingleObj` `Mathlib.Combinatorics.Enumerative.Composition` `Mathlib.CategoryTheory.ConcreteCategory.EpiMono` `Mathlib.Algebra.BigOperators.GroupWithZero.Action` `Mathlib.Analysis.Normed.Group.CocompactMap` `Mathlib.Algebra.MvPolynomial.Funext` `Mathlib.ModelTheory.Algebra.Ring.Basic` `Mathlib.CategoryTheory.Galois.GaloisObjects` `Mathlib.RingTheory.TwoSidedIdeal.Operations` `Mathlib.GroupTheory.Perm.List` `Mathlib.LinearAlgebra.AffineSpace.AffineEquiv` `Mathlib.Data.W.Basic` `Mathlib.RingTheory.Algebraic.Defs` `Mathlib.LinearAlgebra.DFinsupp` `Mathlib.Data.Fintype.Option` `Mathlib.Algebra.Homology.ShortComplex.PreservesHomology` `Mathlib.Algebra.Algebra.Subalgebra.Operations` `Mathlib.NumberTheory.Divisors` `Mathlib.Algebra.Module.Submodule.Map` `Mathlib.RingTheory.LocalRing.ResidueField.Ideal` `Mathlib.LinearAlgebra.Finsupp.Pi` `Mathlib.SetTheory.Game.Short` `Mathlib.Topology.Compactification.OnePointEquiv` `Mathlib.Algebra.Ring.Divisibility.Lemmas` `Mathlib.Tactic.Positivity` `Mathlib.CategoryTheory.Preadditive.Yoneda.Basic` `Mathlib.CategoryTheory.Limits.FinallySmall` `Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel` `Mathlib.Data.Analysis.Topology` `Mathlib.LinearAlgebra.TensorAlgebra.Grading` `Mathlib.SetTheory.Cardinal.Finsupp` `Mathlib.Data.Finsupp.Encodable` `Mathlib.RingTheory.UniqueFactorizationDomain.Basic` `Mathlib.RingTheory.Bialgebra.Hom` `Mathlib.RingTheory.UniqueFactorizationDomain.Nat` `Mathlib.CategoryTheory.GlueData` `Mathlib.GroupTheory.GroupAction.ConjAct` `Mathlib.Algebra.Polynomial.HasseDeriv` `Mathlib.Topology.Compactness.LocallyCompact` `Mathlib.Data.Matrix.PEquiv` `Mathlib.Algebra.RingQuot` `Mathlib.RingTheory.RingHom.FiniteType` `Mathlib.CategoryTheory.Sites.Subsheaf` `Mathlib.Data.Finset.Insert` `Mathlib.CategoryTheory.GradedObject.Monoidal` `Mathlib.CategoryTheory.Enriched.Basic` `Mathlib.RingTheory.Artinian.Ring` `Mathlib.CategoryTheory.Limits.Preserves.Opposites` `Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows` `Mathlib.Topology.Order.Compact` `Mathlib.RingTheory.Algebraic.Cardinality` `Mathlib.CategoryTheory.Dialectica.Basic` `Mathlib.Data.ENNReal.Inv` `Mathlib.CategoryTheory.Sites.Whiskering` `Mathlib.CategoryTheory.Filtered.Final` `Mathlib.Topology.MetricSpace.Sequences` `Mathlib.Data.Set.Finite.Basic` `Mathlib.Topology.Algebra.Group.Basic` `Mathlib.Data.PFunctor.Univariate.M` `Mathlib.Combinatorics.SimpleGraph.Sum` `Mathlib.Topology.ShrinkingLemma` `Mathlib.CategoryTheory.Sites.Preserves` `Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric` `Mathlib.RingTheory.Localization.BaseChange` `Mathlib.SetTheory.Cardinal.Basic` `Mathlib.Algebra.Group.Submonoid.BigOperators` `Mathlib.Algebra.Lie.Nilpotent` `Mathlib.Algebra.Order.Group.Finset` `Mathlib.RingTheory.Ideal.Quotient.Noetherian` `Mathlib.SetTheory.Cardinal.UnivLE` `Mathlib.RingTheory.DiscreteValuationRing.Basic` `Mathlib.AlgebraicTopology.DoldKan.Homotopies` `Mathlib.Tactic.RewriteSearch` `Mathlib.AlgebraicTopology.SimplicialSet.KanComplex` `Mathlib.Topology.Order.ExtendFrom` `Mathlib.GroupTheory.FreeAbelianGroupFinsupp` `Mathlib.RingTheory.Congruence.BigOperators` `Mathlib.Topology.Sheaves.MayerVietoris` `Mathlib.Algebra.Category.Grp.Abelian` `Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing` `Mathlib.Algebra.MonoidAlgebra.ToDirectSum` `Mathlib.RingTheory.KrullDimension.Field` `Mathlib.Dynamics.OmegaLimit` `Mathlib.CategoryTheory.Action.Limits` `Mathlib.NumberTheory.ADEInequality` `Mathlib.Data.Real.ConjExponents` `Mathlib.RingTheory.Localization.Ideal` `Mathlib.RingTheory.Polynomial.Opposites` `Mathlib.Topology.Category.CompHausLike.EffectiveEpi` `Mathlib.SetTheory.Cardinal.Divisibility` `Mathlib.RingTheory.Polynomial.Tower` `Mathlib.Data.Finset.Dedup` `Mathlib.CategoryTheory.Sites.EpiMono` `Mathlib.Algebra.Vertex.VertexOperator` `Mathlib.GroupTheory.Abelianization` `Mathlib.GroupTheory.Perm.Support` `Mathlib.Data.Finset.SMulAntidiagonal` `Mathlib.AlgebraicTopology.CechNerve` `Mathlib.Algebra.Homology.Single` `Mathlib.CategoryTheory.Abelian.Opposite` `Mathlib.Order.Filter.FilterProduct` `Mathlib.Order.Filter.AtTopBot.BigOperators` `Mathlib.Algebra.Category.AlgebraCat.Limits` `Mathlib.Order.Filter.Ultrafilter` `Mathlib.Topology.Filter` `Mathlib.Order.JordanHolder` `Mathlib.Topology.Order.PartialSups` `Mathlib.RingTheory.Coalgebra.Basic` `Mathlib.MeasureTheory.Constructions.AddChar` `Mathlib.Combinatorics.SetFamily.AhlswedeZhang` `Mathlib.Algebra.Quaternion` `Mathlib.Data.Finsupp.Fin` `Mathlib.Algebra.Polynomial.Splits` `Mathlib.Algebra.Algebra.Subalgebra.Tower` `Mathlib.RingTheory.Localization.AsSubring` `Mathlib.Analysis.BoxIntegral.Box.Basic` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits` `Mathlib.Data.Fin.Parity` `Mathlib.Topology.UniformSpace.CompactConvergence` `Mathlib.RingTheory.Localization.Finiteness` `Mathlib.AlgebraicTopology.Quasicategory.StrictSegal` `Mathlib.CategoryTheory.Limits.Indization.LocallySmall` `Mathlib.Deprecated.Submonoid` `Mathlib.CategoryTheory.Preadditive.EilenbergMoore` `Mathlib.FieldTheory.Minpoly.Basic` `Mathlib.Data.Nat.GCD.BigOperators` `Mathlib.GroupTheory.Solvable` `Mathlib.Algebra.Category.Grp.Kernels` `Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet` `Mathlib.RingTheory.Bialgebra.TensorProduct` `Mathlib.CategoryTheory.Closed.Ideal` `Mathlib.Topology.Sheaves.Forget` `Mathlib.Algebra.Ring.Semireal.Defs` `Mathlib.SetTheory.Game.Nim` `Mathlib.Algebra.MvPolynomial.Expand` `Mathlib.Order.Filter.Subsingleton` `Mathlib.Analysis.Oscillation` `Mathlib.Algebra.Homology.HomologicalComplex` `Mathlib.Data.PFunctor.Multivariate.M` `Mathlib.Algebra.DualQuaternion` `Mathlib.Order.Interval.Multiset` `Mathlib.Data.PFunctor.Multivariate.W` `Mathlib.Topology.LocallyFinite` `Mathlib.ModelTheory.Substructures` `Mathlib.Algebra.Group.EvenFunction` `Mathlib.Topology.Order.LocalExtr` `Mathlib.LinearAlgebra.Dimension.Finrank` `Mathlib.Topology.Algebra.ProperAction.Basic` `Mathlib.CategoryTheory.Preadditive.Projective` `Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex` `Mathlib.Algebra.BigOperators.Group.Finset` `Mathlib.RingTheory.Artinian.Module` `Mathlib.ModelTheory.FinitelyGenerated` `Mathlib.CategoryTheory.Sites.Continuous` `Mathlib.RingTheory.Noetherian.Filter` `Mathlib.Algebra.Exact` `Mathlib.Algebra.Order.Floor.Div` `Mathlib.Data.DFinsupp.WellFounded` `Mathlib.Topology.Order` `Mathlib.Data.Nat.Squarefree` `Mathlib.Deprecated.Cardinal.Continuum` `Mathlib.Data.Finset.SDiff` `Mathlib.CategoryTheory.Localization.Pi` `Mathlib.Data.Nat.Factorization.Induction` `Mathlib.Algebra.Category.ModuleCat.Injective` `Mathlib.Data.Fintype.Parity` `Mathlib.Algebra.Ring.SumsOfSquares` `Mathlib.Algebra.Module.Presentation.Tautological` `Mathlib.LinearAlgebra.TensorProduct.Prod` `Mathlib.Data.Finset.Image` `Mathlib.RingTheory.OreLocalization.Cardinality` `Mathlib.NumberTheory.ClassNumber.AdmissibleAbs` `Mathlib.Algebra.TrivSqZeroExt` `Mathlib.Algebra.Category.ModuleCat.Sheaf` `Mathlib.Algebra.Module.Submodule.Range` `Mathlib.CategoryTheory.Monad.Equalizer` `Mathlib.Combinatorics.Additive.AP.Three.Defs` `Mathlib.Data.Matroid.Dual` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic` `Mathlib.Algebra.Star.Subalgebra` `Mathlib.Topology.LocalAtTarget` `Mathlib.Combinatorics.SimpleGraph.Circulant` `Mathlib.Algebra.BigOperators.Pi` `Mathlib.Algebra.Order.Ring.Finset` `Mathlib.Data.Finsupp.Weight` `Mathlib.Algebra.Quandle` `Mathlib.Data.Fintype.Order` `Mathlib.Order.Birkhoff` `Mathlib.CategoryTheory.Filtered.Basic` `Mathlib.LinearAlgebra.Multilinear.Basic` `Mathlib.CategoryTheory.Triangulated.Basic` `Mathlib.NumberTheory.Harmonic.Defs` `Mathlib.CategoryTheory.Localization.SmallShiftedHom` `Mathlib.ModelTheory.Complexity` `Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular` `Mathlib.Data.Finset.Fin` `Mathlib.RingTheory.Polynomial.Hermite.Basic` `Mathlib.LinearAlgebra.Multilinear.Basis` `Mathlib.Algebra.Ring.Subring.Basic` `Mathlib.CategoryTheory.Abelian.ProjectiveResolution` `Mathlib.LinearAlgebra.Finsupp.SumProd` `Mathlib.Combinatorics.SimpleGraph.Triangle.Counting` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Free` `Mathlib.AlgebraicTopology.Quasicategory.Nerve` `Mathlib.Data.Finset.Sum` `Mathlib.Topology.LocallyConstant.Basic` `Mathlib.GroupTheory.Divisible` `Mathlib.Algebra.MonoidAlgebra.Support` `Mathlib.Algebra.CubicDiscriminant` `Mathlib.Topology.Order.ProjIcc` `Mathlib.RingTheory.NonUnitalSubsemiring.Basic` `Mathlib.Combinatorics.SimpleGraph.Density` `Mathlib.RingTheory.PrincipalIdealDomain` `Mathlib.RingTheory.Ideal.MinimalPrime` `Mathlib.CategoryTheory.Limits.Constructions.Over.Products` `Mathlib.Data.Set.MemPartition` `Mathlib.Topology.MetricSpace.Cauchy` `Mathlib.RingTheory.Bialgebra.Basic` `Mathlib.Topology.EMetricSpace.Defs` `Mathlib.Topology.Order.Hom.Esakia` `Mathlib.CategoryTheory.Limits.Presheaf` `Mathlib.Algebra.Lie.Free` `Mathlib.Data.DFinsupp.Sigma` `Mathlib.CategoryTheory.Subobject.FactorThru` `Mathlib.Data.Rat.Denumerable` `Mathlib.Order.Interval.Set.Infinite` `Mathlib.Topology.MetricSpace.Lipschitz` `Mathlib.LinearAlgebra.BilinearForm.Orthogonal` `Mathlib.GroupTheory.Coxeter.Basic` `Mathlib.Data.Finsupp.Defs` `Mathlib.Data.Finset.Pi` `Mathlib.RingTheory.Polynomial.IrreducibleRing` `Mathlib.Data.DFinsupp.NeLocus` `Mathlib.Data.Finset.Powerset` `Mathlib.Order.Category.OmegaCompletePartialOrder` `Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory` `Mathlib.RingTheory.UniqueFactorizationDomain.Finite` `Mathlib.Algebra.Group.Pointwise.Finset.Basic` `Mathlib.Combinatorics.Additive.CovBySMul` `Mathlib.RingTheory.RingHom.Finite` `Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors` `Mathlib.Combinatorics.Additive.Energy` `Mathlib.Topology.Baire.LocallyCompactRegular` `Mathlib.RingTheory.AlgebraicIndependent.Defs` `Mathlib.RingTheory.EssentialFiniteness` `Mathlib.Algebra.Order.Interval.Multiset` `Mathlib.Algebra.Polynomial.Inductions` `Mathlib.CategoryTheory.Closed.Functor` `Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive` `Mathlib.Topology.Instances.Discrete` `Mathlib.Algebra.Homology.ShortComplex.ModuleCat` `Mathlib.Algebra.DirectSum.Basic` `Mathlib.RingTheory.MvPolynomial.Symmetric.Defs` `Mathlib.RingTheory.PowerSeries.Derivative` `Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts` `Mathlib.Data.Set.Equitable` `Mathlib.Algebra.GCDMonoid.Multiset` `Mathlib.Topology.Spectral.Hom` `Mathlib.Algebra.Central.Defs` `Mathlib.Topology.PreorderRestrict` `Mathlib.Topology.PartialHomeomorph` `Mathlib.Algebra.Group.Pointwise.Set.BigOperators` `Mathlib.Computability.ContextFreeGrammar` `Mathlib.Topology.ClopenBox` `Mathlib.GroupTheory.Coprod.Basic` `Mathlib.RingTheory.NonUnitalSubring.Basic` `Mathlib.CategoryTheory.Sites.LocallySurjective` `Mathlib.Data.Int.Interval` `Mathlib.RingTheory.Coprime.Lemmas` `Mathlib.Topology.Sheaves.LocalPredicate` `Mathlib.Algebra.Star.BigOperators` `Mathlib.Algebra.Homology.Square` `Mathlib.Data.Finset.Sups` `Mathlib.Data.Finset.Sym` `Mathlib.Algebra.Lie.CartanSubalgebra` `Mathlib.Topology.MetricSpace.Pseudo.Basic` `Mathlib.RingTheory.Polynomial.Radical` `Mathlib.Data.Finset.Piecewise` `Mathlib.Algebra.Polynomial.DenomsClearable` `Mathlib.LinearAlgebra.FreeModule.PID` `Mathlib.Algebra.Ring.Pointwise.Finset` `Mathlib.Algebra.Vertex.HVertexOperator` `Mathlib.Algebra.Lie.IdealOperations` `Mathlib.SetTheory.Game.Basic` `Mathlib.CategoryTheory.Enriched.FunctorCategory` `Mathlib.SetTheory.Ordinal.Arithmetic` `Mathlib.CategoryTheory.Sites.LocallyFullyFaithful` `Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers` `Mathlib.Algebra.Algebra.Subalgebra.Rank` `Mathlib.Algebra.Category.ModuleCat.Products` `Mathlib.Algebra.GroupWithZero.NonZeroDivisors` `Mathlib.Data.Fin.Tuple.NatAntidiagonal` `Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform` `Mathlib.Topology.Sequences` `Mathlib.Algebra.Order.BigOperators.Ring.Multiset` `Mathlib.Analysis.Convex.Slope` `Mathlib.Topology.Order.Monotone` `Mathlib.Order.LiminfLimsup` `Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover` `Mathlib.Topology.Algebra.WithZeroTopology` `Mathlib.Algebra.GroupWithZero.Pointwise.Set.Card` `Mathlib.Algebra.Module.Presentation.Free` `Mathlib.CategoryTheory.Sites.PreservesSheafification` `Mathlib.Order.Restriction` `Mathlib.Algebra.Group.Translate` `Mathlib.Algebra.Order.Antidiag.Pi` `Mathlib.Combinatorics.SimpleGraph.Triangle.Basic` `Mathlib.Combinatorics.SetFamily.Kleitman` `Mathlib.LinearAlgebra.Matrix.FiniteDimensional` `Mathlib.Algebra.Algebra.Basic` `Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities` `Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor` `Mathlib.Data.Finset.Functor` `Mathlib.Data.Nat.Factorization.Defs` `Mathlib.Data.Set.Constructions` `Mathlib.Order.Monotone.MonovaryOrder` `Mathlib.Algebra.Polynomial.Eval.Algebra` `Mathlib.CategoryTheory.Monoidal.Types.Basic` `Mathlib.CategoryTheory.Sites.IsSheafOneHypercover` `Mathlib.CategoryTheory.Sites.Abelian` `Mathlib.RingTheory.Derivation.Basic` `Mathlib.RingTheory.Localization.Away.Basic` `Mathlib.Topology.Algebra.Order.Field` `Mathlib.Topology.Algebra.InfiniteSum.NatInt` `Mathlib.Algebra.Polynomial.RingDivision` `Mathlib.Order.CompleteLattice.Finset` `Mathlib.Algebra.Category.ModuleCat.Simple` `Mathlib.Data.Nat.Fib.Basic` `Mathlib.Topology.Bornology.Absorbs` `Mathlib.Topology.UniformSpace.OfFun` `Mathlib.Data.Finset.Lattice.Basic` `Mathlib.Combinatorics.Derangements.Basic` `Mathlib.Analysis.Normed.Field.Basic` `Mathlib.Algebra.Category.MonCat.Limits` `Mathlib.Algebra.Algebra.Operations` `Mathlib.Topology.Order.LowerUpperTopology` `Mathlib.Data.Finset.Erase` `Mathlib.Order.Category.FinBoolAlg` `Mathlib.Order.Filter.Pointwise` `Mathlib.Combinatorics.Digraph.Orientation` `Mathlib.Data.Set.Finite.Range` `Mathlib.Data.Finset.NatAntidiagonal` `Mathlib.RingTheory.DualNumber` `Mathlib.Algebra.Star.StarAlgHom` `Mathlib.CategoryTheory.Abelian.Basic` `Mathlib.Algebra.Lie.Basic` `Mathlib.Data.Finset.Update` `Mathlib.RingTheory.Noetherian.Basic` `Mathlib.CategoryTheory.Limits.Constructions.EpiMono` `Mathlib.Order.Filter.IndicatorFunction` `Mathlib.Algebra.BigOperators.Option` `Mathlib.Tactic.FinCases` `Mathlib.Topology.Defs.Induced` `Mathlib.Algebra.Algebra.Subalgebra.Prod` `Mathlib.Tactic.NormNum.NatFib` `Mathlib.CategoryTheory.Preadditive.OfBiproducts` `Mathlib.Algebra.Colimit.Finiteness` `Mathlib.AlgebraicTopology.DoldKan.GammaCompN` `Mathlib.CategoryTheory.Sites.Localization` `Mathlib.LinearAlgebra.Matrix.Ideal` `Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion` `Mathlib.Tactic.NormNum.BigOperators` `Mathlib.Algebra.Module.Presentation.Cokernel` `Mathlib.Algebra.Polynomial.Taylor` `Mathlib.Topology.UniformSpace.AbstractCompletion` `Mathlib.Topology.Category.TopCat.Basic` `Mathlib.SetTheory.Ordinal.Principal` `Mathlib.Data.Finsupp.SMulWithZero` `Mathlib.Algebra.Lie.Derivation.AdjointAction` `Mathlib.Data.Rat.BigOperators` `Mathlib.LinearAlgebra.Quotient.Pi` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks` `Mathlib.CategoryTheory.Enriched.Opposite` `Mathlib.Topology.Maps.Proper.Basic` `Mathlib.NumberTheory.FrobeniusNumber` `Mathlib.RingTheory.Finiteness.Lattice` `Mathlib.Data.Pi.Interval` `Mathlib.RingTheory.Polynomial.IntegralNormalization` `Mathlib.Combinatorics.Additive.Dissociation` `Mathlib.ModelTheory.Graph` `Mathlib.Topology.Clopen` `Mathlib.Order.Filter.CountableInter` `Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems` `Mathlib.CategoryTheory.Sites.ConstantSheaf` `Mathlib.RingTheory.Algebraic.Basic` `Mathlib.Order.CompactlyGenerated.Intervals` `Mathlib.Topology.MetricSpace.Dilation` `Mathlib.CategoryTheory.Preadditive.Yoneda.Injective` `Mathlib.RingTheory.Noetherian.Nilpotent` `Mathlib.CategoryTheory.Countable` `Mathlib.NumberTheory.PellMatiyasevic` `Mathlib.Algebra.Lie.Character` `Mathlib.Topology.Algebra.Group.SubmonoidClosure` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf` `Mathlib.CategoryTheory.Filtered.Small` `Mathlib.Algebra.Module.LocalizedModule.Int` `Mathlib.Algebra.Group.AddChar` `Mathlib.Topology.Sober` `Mathlib.ModelTheory.LanguageMap` `Mathlib.RingTheory.Finiteness.Basic` `Mathlib.Data.Finset.Pairwise` `Mathlib.Topology.Defs.Sequences` `Mathlib.ModelTheory.Encoding` `Mathlib.CategoryTheory.Sites.CompatiblePlus` `Mathlib.Topology.ExtendFrom` `Mathlib.Algebra.Algebra.Hom.Rat` `Mathlib.Algebra.Lie.DirectSum` `Mathlib.GroupTheory.Perm.Option` `Mathlib.Topology.UniformSpace.CompleteSeparated` `Mathlib.Order.Filter.AtTopBot.CountablyGenerated` `Mathlib.RingTheory.Coalgebra.TensorProduct` `Mathlib.Algebra.Order.BigOperators.Expect` `Mathlib.RingTheory.MvPolynomial.Homogeneous` `Mathlib.Algebra.Category.Ring.Epi` `Mathlib.Data.DFinsupp.Module` `Mathlib.Algebra.Category.ModuleCat.Pseudofunctor` `Mathlib.RingTheory.Coprime.Ideal` `Mathlib.Data.Finsupp.Antidiagonal` `Mathlib.Algebra.Squarefree.Basic` `Mathlib.Algebra.Polynomial.Expand` `Mathlib.RingTheory.FractionalIdeal.Basic` `Mathlib.CategoryTheory.Limits.Preserves.Presheaf` `Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves` `Mathlib.LinearAlgebra.Finsupp.LSum` `Mathlib.Topology.MetricSpace.ProperSpace` `Mathlib.Algebra.Homology.ShortComplex.Homology` `Mathlib.LinearAlgebra.FiniteDimensional` `Mathlib.RingTheory.MvPolynomial.Ideal` `Mathlib.Topology.Category.TopCat.Limits.Cofiltered` `Mathlib.RingTheory.Polynomial.Vieta` `Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings` `Mathlib.Combinatorics.Additive.PluenneckeRuzsa` `Mathlib.CategoryTheory.Monad.Comonadicity` `Mathlib.Topology.Order.Filter` `Mathlib.Topology.Bases` `Mathlib.Algebra.BigOperators.Ring.Nat` `Mathlib.Data.Holor` `Mathlib.Algebra.BigOperators.Ring.Multiset` `Mathlib.Algebra.Category.ModuleCat.Biproducts` `Mathlib.Algebra.DirectSum.Internal` `Mathlib.Data.Matrix.Block` `Mathlib.RingTheory.Derivation.ToSquareZero` `Mathlib.Data.Fintype.Sort` `Mathlib.RingTheory.Valuation.ValuationRing` `Mathlib.Algebra.BigOperators.Balance` `Mathlib.ModelTheory.Definability` `Mathlib.LinearAlgebra.Matrix.ToLin` `Mathlib.CategoryTheory.ChosenFiniteProducts.Cat` `Mathlib.Topology.Algebra.Star` `Mathlib.RingTheory.FinitePresentation` `Mathlib.Analysis.Convex.SimplicialComplex.Basic` `Mathlib.Algebra.DirectSum.Idempotents` `Mathlib.RingTheory.IntegralClosure.Algebra.Defs` `Mathlib.Topology.Separation.CountableSeparatingOn` `Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal` `Mathlib.Algebra.Group.Pointwise.Set.Card` `Mathlib.Order.Filter.Cofinite` `Mathlib.Combinatorics.HalesJewett` `Mathlib.CategoryTheory.Shift.ShiftedHomOpposite` `Mathlib.Data.Fintype.Card` `Mathlib.AlgebraicTopology.SimplicialSet.Path` `Mathlib.CategoryTheory.ChosenFiniteProducts.FunctorCategory` `Mathlib.RingTheory.Finiteness.Subalgebra` `Mathlib.LinearAlgebra.FreeModule.Finite.Basic` `Mathlib.RingTheory.Ideal.Maximal` `Mathlib.RingTheory.DividedPowers.Basic` `Mathlib.Data.Set.MulAntidiagonal` `Mathlib.CategoryTheory.Triangulated.Opposite.Triangle` `Mathlib.Topology.ContinuousMap.SecondCountableSpace` `Mathlib.AlgebraicTopology.SimplicialSet.Monoidal` `Mathlib.Data.Setoid.Partition` `Mathlib.Algebra.Algebra.Subalgebra.Order` `Mathlib.Topology.Order.Basic` `Mathlib.Order.Category.NonemptyFinLinOrd` `Mathlib.Topology.Algebra.Equicontinuity` `Mathlib.SetTheory.Ordinal.Topology` `Mathlib.Order.Interval.Finset.Basic` `Mathlib.CategoryTheory.Generator.Basic` `Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset` `Mathlib.Algebra.Category.ModuleCat.Subobject` `Mathlib.RingTheory.PiTensorProduct` `Mathlib.Data.Multiset.Bind` `Mathlib.Data.Finset.Disjoint` `Mathlib.Algebra.Algebra.Opposite` `Mathlib.CategoryTheory.Monoidal.Internal.Types` `Mathlib.CategoryTheory.Action.Basic` `Mathlib.Topology.Instances.ENat` `Mathlib.Topology.Homeomorph` `Mathlib.GroupTheory.Perm.DomMulAct` `Mathlib.Topology.ContinuousMap.Basic` `Mathlib.Combinatorics.SimpleGraph.Ends.Defs` `Mathlib.RingTheory.Coalgebra.Hom` `Mathlib.Topology.Separation.SeparatedNhds` `Mathlib.RingTheory.RingHom.Injective` `Mathlib.RingTheory.Ideal.Quotient.Nilpotent` `Mathlib.RingTheory.MvPolynomial.Localization` `Mathlib.CategoryTheory.Sites.CartesianClosed` `Mathlib.RingTheory.Localization.LocalizationLocalization` `Mathlib.Combinatorics.Additive.RuzsaCovering` `Mathlib.Topology.Basic` `Mathlib.Topology.List` `Mathlib.LinearAlgebra.TensorProduct.Quotient` `Mathlib.RingTheory.LocalRing.Basic` `Mathlib.CategoryTheory.Monoidal.Types.Coyoneda` `Mathlib.LinearAlgebra.TensorAlgebra.Basic` `Mathlib.RingTheory.Localization.Submodule` `Mathlib.RingTheory.Radical` `Mathlib.Combinatorics.SimpleGraph.Diam` `Mathlib.RingTheory.Localization.Integer` `Mathlib.LinearAlgebra.TensorAlgebra.Basis` `Mathlib.CategoryTheory.Sites.Coherent.Basic` `Mathlib.GroupTheory.ClassEquation` `Mathlib.Algebra.Module.LocalizedModule.Basic` `Mathlib.Topology.Algebra.UniformGroup.Defs` `Mathlib.GroupTheory.MonoidLocalization.Away` `Mathlib.CategoryTheory.Sites.LocallyInjective` `Mathlib.Order.Filter.AtTopBot.Field` `Mathlib.SetTheory.Ordinal.Exponential` `Mathlib.Data.Fintype.Basic` `Mathlib.Data.Finset.Slice` `Mathlib.RingTheory.Adjoin.Tower` `Mathlib.Geometry.RingedSpace.OpenImmersion` `Mathlib.Algebra.Small.Module` `Mathlib.Combinatorics.SimpleGraph.Regularity.Energy` `Mathlib.CategoryTheory.Limits.Shapes.Diagonal` `Mathlib.CategoryTheory.Limits.Shapes.SingleObj` `Mathlib.Deprecated.Subgroup` `Mathlib.CategoryTheory.Limits.Indization.Category` `Mathlib.Data.Finset.Finsupp` `Mathlib.NumberTheory.Zsqrtd.GaussianInt` `Mathlib.RingTheory.PolynomialAlgebra` `Mathlib.RingTheory.Localization.Defs` `Mathlib.Topology.ContinuousMap.CocompactMap` `Mathlib.RingTheory.Polynomial.HilbertPoly` `Mathlib.LinearAlgebra.Finsupp.LinearCombination` `Mathlib.Algebra.Category.CoalgebraCat.Basic` `Mathlib.Topology.MetricSpace.IsometricSMul` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits` `Mathlib.Topology.Algebra.UniformMulAction` `Mathlib.LinearAlgebra.BilinearForm.Properties` `Mathlib.Algebra.Homology.ImageToKernel` `Mathlib.RingTheory.MvPolynomial.FreeCommRing` `Mathlib.LinearAlgebra.AffineSpace.MidpointZero` `Mathlib.Algebra.Module.Card` `Mathlib.Topology.NhdsSet` `Mathlib.Algebra.Polynomial.Mirror` `Mathlib.Topology.Algebra.Indicator` `Mathlib.LinearAlgebra.TensorProduct.Finiteness` `Mathlib.Algebra.Algebra.Unitization` `Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise` `Mathlib.Algebra.Group.ForwardDiff` `Mathlib.Topology.MetricSpace.Pseudo.Pi` `Mathlib.LinearAlgebra.FiniteDimensional.Defs` `Mathlib.Topology.MetricSpace.Equicontinuity` `Mathlib.LinearAlgebra.DirectSum.TensorProduct` `Mathlib.Topology.Gluing` `Mathlib.Algebra.DirectSum.Decomposition` `Mathlib.Algebra.Equiv.TransferInstance` `Mathlib.Topology.LocallyClosed` `Mathlib.CategoryTheory.Preadditive.Mat` `Mathlib.RingTheory.Nilpotent.Lemmas` `Mathlib.Topology.Connected.LocallyConnected` `Mathlib.Algebra.Homology.HomologicalComplexLimits` `Mathlib.RingTheory.Jacobson.Ideal` `Mathlib.Topology.UniformSpace.Basic` `Mathlib.RingTheory.Polynomial.Bernstein` `Mathlib.Topology.Sets.Order` `Mathlib.CategoryTheory.Abelian.Refinements` `Mathlib.Algebra.LinearRecurrence` `Mathlib.Data.BitVec` `Mathlib.Order.Filter.AtTopBot.Archimedean` `Mathlib.Data.Set.Finite.Powerset` `Mathlib.LinearAlgebra.TensorProduct.Subalgebra` `Mathlib.CategoryTheory.Quotient.Linear` `Mathlib.Algebra.MonoidAlgebra.Degree` `Mathlib.Combinatorics.SetFamily.Compression.UV` `Mathlib.Topology.MetricSpace.Ultra.Basic` `Mathlib.Analysis.Convex.Cone.Extension` `Mathlib.Algebra.Polynomial.PartialFractions` `Mathlib.Algebra.MonoidAlgebra.Ideal` `Mathlib.Topology.MetricSpace.Isometry` `Mathlib.Data.Finset.Max` `Mathlib.LinearAlgebra.BilinearForm.Hom` `Mathlib.Algebra.MvPolynomial.Rename` `Mathlib.LinearAlgebra.AffineSpace.Basis` `Mathlib.Algebra.Polynomial.Degree.SmallDegree` `Mathlib.Algebra.Algebra.Pi` `Mathlib.Algebra.Order.Antidiag.Nat` `Mathlib.SetTheory.Game.Birthday` `Mathlib.Computability.Halting` `Mathlib.LinearAlgebra.Matrix.DotProduct` `Mathlib.Algebra.Homology.ShortComplex.Abelian` `Mathlib.Combinatorics.Additive.FreimanHom` `Mathlib.Algebra.Category.Grp.FilteredColimits` `Mathlib.Algebra.Polynomial.Monic` `Mathlib.Data.Matrix.Reflection` `Mathlib.Algebra.Polynomial.Degree.Domain` `Mathlib.RingTheory.Nilpotent.Defs` `Mathlib.Order.SupIndep` `Mathlib.Algebra.Module.Projective` `Mathlib.Data.DFinsupp.Interval` `Mathlib.CategoryTheory.Noetherian` `Mathlib.Algebra.FreeMonoid.Symbols` `Mathlib.Data.Nat.Choose.Vandermonde` `Mathlib.RingTheory.Adjoin.FG` `Mathlib.Testing.Plausible.Functions` `Mathlib.CategoryTheory.GuitartExact.Basic` `Mathlib.Logic.Equiv.Array` `Mathlib.CategoryTheory.Abelian.Injective` `Mathlib.Topology.Hom.Open` `Mathlib.Dynamics.Newton` `Mathlib.RingTheory.FiniteStability` `Mathlib.RingTheory.Localization.InvSubmonoid` `Mathlib.Topology.Algebra.MulAction` `Mathlib.Computability.TuringMachine` `Mathlib.Order.Irreducible` `Mathlib.LinearAlgebra.Basis.Defs` `Mathlib.Algebra.BigOperators.Intervals` `Mathlib.CategoryTheory.Generator.Abelian` `Mathlib.Analysis.Convex.Join` `Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject` `Mathlib.GroupTheory.QuotientGroup.Basic` `Mathlib.Algebra.Polynomial.Coeff` `Mathlib.CategoryTheory.Monoidal.Tor` `Mathlib.Algebra.Algebra.Subalgebra.Pointwise` `Mathlib.Order.Filter.AtTopBot.Ring` `Mathlib.CategoryTheory.Preadditive.AdditiveFunctor` `Mathlib.GroupTheory.Coset.Basic` `Mathlib.Data.Multiset.FinsetOps` `Mathlib.Algebra.Order.Floor.Prime` `Mathlib.NumberTheory.SmoothNumbers` `Mathlib.LinearAlgebra.Matrix.StdBasis` `Mathlib.Algebra.MvPolynomial.Derivation` `Mathlib.Data.Sym.Basic` `Mathlib.Algebra.Homology.Embedding.Extend` `Mathlib.Algebra.Category.Ring.FilteredColimits` `Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower` `Mathlib.Order.ConditionallyCompleteLattice.Finset` `Mathlib.CategoryTheory.Filtered.Grothendieck` `Mathlib.Topology.Category.TopCat.OpenNhds` `Mathlib.Algebra.CharP.Subring` `Mathlib.Algebra.Category.Grp.Adjunctions` `Mathlib.Algebra.MvPolynomial.Variables` `Mathlib.RepresentationTheory.Basic` `Mathlib.Combinatorics.SimpleGraph.Finsubgraph` `Mathlib.CategoryTheory.Galois.Decomposition` `Mathlib.Combinatorics.Hall.Finite` `Mathlib.RingTheory.Filtration` `Mathlib.RingTheory.Nakayama` `Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic` `Mathlib.Topology.MetricSpace.Infsep` `Mathlib.CategoryTheory.Generator.Coproduct` `Mathlib.CategoryTheory.Abelian.Projective` `Mathlib.CategoryTheory.Sites.Limits` `Mathlib.LinearAlgebra.FreeModule.Finite.Matrix` `Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors` `Mathlib.Algebra.Polynomial.Derivation` `Mathlib.SetTheory.Cardinal.Cofinality` `Mathlib.Topology.Order.NhdsSet` `Mathlib.Algebra.Module.LocalizedModule.IsLocalization` `Mathlib.Data.Fintype.BigOperators` `Mathlib.CategoryTheory.ComposableArrows` `Mathlib.RingTheory.Valuation.RamificationGroup` `Mathlib.Algebra.Module.SnakeLemma` `Mathlib.Tactic.ComputeDegree` `Mathlib.RingTheory.MvPolynomial` `Mathlib.SetTheory.Surreal.Dyadic` `Mathlib.Data.DFinsupp.FiniteInfinite` `Mathlib.Topology.Category.CompHausLike.Basic` `Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity` `Mathlib.Computability.Partrec` `Mathlib.Algebra.MvPolynomial.Supported` `Mathlib.RingTheory.MvPolynomial.Tower` `Mathlib.Geometry.RingedSpace.Basic` `Mathlib.Order.Extension.Well` `Mathlib.Data.Finsupp.MonomialOrder` `Mathlib.Combinatorics.SimpleGraph.Girth` `Mathlib.LinearAlgebra.Pi` `Mathlib.Topology.Algebra.InfiniteSum.Ring` `Mathlib.LinearAlgebra.Dimension.Basic` `Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts` `Mathlib.Data.Finsupp.Multiset` `Mathlib.Algebra.Homology.HomologicalComplexBiprod` `Mathlib.Combinatorics.SimpleGraph.Metric` `Mathlib.Topology.Order.LeftRightLim` `Mathlib.CategoryTheory.Sites.LeftExact` `Mathlib.RingTheory.Finiteness.TensorProduct` `Mathlib.Algebra.DirectSum.Finsupp` `Mathlib.Data.Fintype.Units` `Mathlib.Algebra.Ring.CentroidHom` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology` `Mathlib.LinearAlgebra.LinearIndependent` `Mathlib.LinearAlgebra.AffineSpace.Restrict` `Mathlib.Analysis.Convex.Between` `Mathlib.Topology.FiberPartition` `Mathlib.LinearAlgebra.AffineSpace.Independent` `Mathlib.Analysis.LocallyConvex.Polar` `Mathlib.Algebra.Small.Ring` `Mathlib.Algebra.AlgebraicCard` `Mathlib.Algebra.Order.Star.Conjneg` `Mathlib.Analysis.Normed.Order.Hom.Basic` `Mathlib.SetTheory.Cardinal.Aleph` `Mathlib.Algebra.Homology.HomologicalBicomplex` `Mathlib.Topology.Compactness.PseudometrizableLindelof` `Mathlib.Data.Complex.BigOperators` `Mathlib.Data.Multiset.Basic` `Mathlib.Topology.Connected.Clopen` `Mathlib.CategoryTheory.Galois.Basic` `Mathlib.Algebra.Tropical.BigOperators` `Mathlib.CategoryTheory.Idempotents.SimplicialObject` `Mathlib.CategoryTheory.Linear.Basic` `Mathlib.Order.Filter.AtTopBot` `Mathlib.Data.TypeVec` `Mathlib.Data.Fintype.CardEmbedding` `Mathlib.LinearAlgebra.Contraction` `Mathlib.Data.FinEnum.Option` `Mathlib.Combinatorics.Additive.VerySmallDoubling` `Mathlib.SetTheory.Cardinal.Continuum` `Mathlib.Algebra.Algebra.Spectrum` `Mathlib.RingTheory.MvPolynomial.EulerIdentity` `Mathlib.Topology.Order.MonotoneConvergence` `Mathlib.Data.Nat.Multiplicity` `Mathlib.RingTheory.Binomial` `Mathlib.Algebra.Module.Submodule.RestrictScalars` `Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive` `Mathlib.Algebra.Category.Grp.Preadditive` `Mathlib.Data.Nat.Factorial.BigOperators` `Mathlib.Order.Category.FinBddDistLat` `Mathlib.Algebra.Regular.Pow` `Mathlib.Algebra.Polynomial.Laurent` `Mathlib.Algebra.Category.ModuleCat.Tannaka` `Mathlib.LinearAlgebra.Multilinear.FiniteDimensional` `Mathlib.MeasureTheory.MeasurableSpace.NCard` `Mathlib.LinearAlgebra.Multilinear.Pi` `Mathlib.ModelTheory.Quotients` `Mathlib.Data.Matroid.Closure` `Mathlib.Topology.Algebra.MvPolynomial` `Mathlib.CategoryTheory.Sites.Sheaf` `Mathlib.Algebra.Polynomial.Module.Basic` `Mathlib.Algebra.Star.NonUnitalSubsemiring` `Mathlib.Data.Finset.Order` `Mathlib.RingTheory.MvPolynomial.Groebner` `Mathlib.Algebra.Order.Interval.Finset` `Mathlib.Topology.Order.LeftRight` `Mathlib.Algebra.Homology.ShortComplex.Linear` `Mathlib.CategoryTheory.Shift.Opposite` `Mathlib.Topology.Maps.OpenQuotient` `Mathlib.CategoryTheory.Limits.Opposites` `Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence` `Mathlib.SetTheory.Game.Impartial` `Mathlib.Analysis.NormedSpace.MStructure` `Mathlib.Computability.Language` `Mathlib.Computability.TMComputable` `Mathlib.Algebra.Lie.Semisimple.Defs` `Mathlib.Topology.ContinuousMap.Sigma` `Mathlib.Analysis.BoxIntegral.Partition.Tagged` `Mathlib.Algebra.Polynomial.Degree.CardPowDegree` `Mathlib.Topology.Algebra.ProperConstSMul` `Mathlib.Data.Nat.Count` `Mathlib.Algebra.Category.ModuleCat.FilteredColimits` `Mathlib.Data.ENat.BigOperators` `Mathlib.Data.Fin.Fin2` `Mathlib.CategoryTheory.Limits.Constructions.Over.Basic` `Mathlib.RingTheory.MvPowerSeries.Inverse` `Mathlib.Topology.Algebra.UniformConvergence` `Mathlib.Topology.Bornology.Basic` `Mathlib.RingTheory.SurjectiveOnStalks` `Mathlib.Data.Finsupp.Fintype` `Mathlib.CategoryTheory.Generator.Preadditive` `Mathlib.Analysis.Convex.Independent` `Mathlib.Combinatorics.SimpleGraph.Trails` `Mathlib.Topology.Order.Rolle` `Mathlib.RingTheory.ChainOfDivisors` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory` `Mathlib.Topology.Algebra.ConstMulAction` `Mathlib.CategoryTheory.Triangulated.Rotate` `Mathlib.Data.Matrix.ColumnRowPartitioned` `Mathlib.LinearAlgebra.Projectivization.Independence` `Mathlib.RingTheory.Noetherian.Defs` `Mathlib.Topology.Bornology.Constructions` `Mathlib.CategoryTheory.Preadditive.Basic` `Mathlib.Algebra.Category.ModuleCat.Colimits` `Mathlib.RingTheory.LocalProperties.Exactness` `Mathlib.Topology.NoetherianSpace` `Mathlib.CategoryTheory.Preadditive.SingleObj` `Mathlib.CategoryTheory.Galois.Topology` `Mathlib.LinearAlgebra.InvariantBasisNumber` `Mathlib.Combinatorics.SimpleGraph.Turan` `Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic` `Mathlib.Algebra.Category.BialgebraCat.Basic` `Mathlib.Topology.Category.Born` `Mathlib.Algebra.Polynomial.Derivative` `Mathlib.Data.Finsupp.Indicator` `Mathlib.Data.Fintype.Sigma` `Mathlib.Topology.Algebra.Field` `Mathlib.Combinatorics.SetFamily.Shadow` `Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective` `Mathlib.Algebra.Small.Group` `Mathlib.RingTheory.OrzechProperty` `Mathlib.Topology.Algebra.InfiniteSum.Field` `Mathlib.LinearAlgebra.Matrix.Trace` `Mathlib.Algebra.MvPolynomial.SchwartzZippel` `Mathlib.Topology.MetricSpace.Pseudo.Lemmas` `Mathlib.SetTheory.Ordinal.Enum` `Mathlib.SetTheory.Game.State` `Mathlib.MeasureTheory.Measure.AddContent` `Mathlib.RingTheory.Polynomial.Basic` `Mathlib.Combinatorics.SimpleGraph.Partition` `Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass` `Mathlib.Algebra.Lie.Abelian` `Mathlib.LinearAlgebra.SesquilinearForm` `Mathlib.Data.Nat.Choose.Factorization` `Mathlib.RingTheory.HopfAlgebra` `Mathlib.Data.DFinsupp.Encodable` `Mathlib.Data.Nat.Choose.Sum` `Mathlib.Topology.EMetricSpace.Basic` `Mathlib.LinearAlgebra.TensorProduct.Submodule` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf` `Mathlib.Algebra.Algebra.Subalgebra.Basic` `Mathlib.RingTheory.LocalRing.ResidueField.Defs` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators` `Mathlib.RingTheory.UniqueFactorizationDomain.Defs` `Mathlib.Algebra.Category.Grp.Ulift` `Mathlib.Analysis.Normed.Group.Bounded` `Mathlib.CategoryTheory.Limits.Indization.Products` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian` `Mathlib.Topology.Category.TopCat.Opens` `Mathlib.Data.Set.Sups` `Mathlib.Algebra.Star.RingQuot` `Mathlib.Data.Matroid.Constructions` `Mathlib.CategoryTheory.CofilteredSystem` `Mathlib.AlgebraicTopology.DoldKan.Notations` `Mathlib.Data.QPF.Multivariate.Constructions.Quot` `Mathlib.Algebra.Homology.Refinements` `Mathlib.Algebra.Group.Submonoid.Units` `Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal` `Mathlib.RingTheory.ReesAlgebra` `Mathlib.RingTheory.IsTensorProduct` `Mathlib.CategoryTheory.Closed.FunctorCategory.Complete` `Mathlib.Algebra.MvPolynomial.Comap` `Mathlib.Topology.Algebra.Algebra.Rat` `Mathlib.RingTheory.Ideal.AssociatedPrime` `Mathlib.Algebra.Polynomial.Eval.Degree` `Mathlib.CategoryTheory.Limits.IsConnected` `Mathlib.Topology.Covering` `Mathlib.RingTheory.Polynomial.Wronskian` `Mathlib.LinearAlgebra.Matrix.Permanent` `Mathlib.Algebra.Category.AlgebraCat.Symmetric` `Mathlib.FieldTheory.Finiteness` `Mathlib.Combinatorics.SimpleGraph.Path` `Mathlib.Topology.UniformSpace.UniformEmbedding` `Mathlib.CategoryTheory.Limits.Comma` `Mathlib.Order.SupClosed` `Mathlib.Combinatorics.Schnirelmann` `Mathlib.Data.Sigma.Interval` `Mathlib.CategoryTheory.Sites.Spaces` `Mathlib.Algebra.Pointwise.Stabilizer` `Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries` `Mathlib.Algebra.Algebra.RestrictScalars` `Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts` `Mathlib.NumberTheory.MaricaSchoenheim` `Mathlib.Topology.UniformSpace.Completion` `Mathlib.Topology.Category.TopCat.Limits.Konig` `Mathlib.GroupTheory.Commutator.Finite` `Mathlib.CategoryTheory.Sites.Coherent.Equivalence` `Mathlib.Data.QPF.Multivariate.Constructions.Fix` `Mathlib.Algebra.CharP.ExpChar` `Mathlib.AlgebraicTopology.DoldKan.Normalized` `Mathlib.Topology.Metrizable.Basic` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images` `Mathlib.LinearAlgebra.FreeAlgebra` `Mathlib.CategoryTheory.Sites.Sheafification` `Mathlib.AlgebraicTopology.SimplicialNerve` `Mathlib.CategoryTheory.Limits.Indization.IndObject` `Mathlib.RingTheory.Nilpotent.Basic` `Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting` `Mathlib.Data.Finset.NatDivisors` `Mathlib.ModelTheory.Syntax` `Mathlib.Algebra.BigOperators.Associated` `Mathlib.CategoryTheory.Sites.Coverage` `Mathlib.Combinatorics.SimpleGraph.Walk` `Mathlib.RingTheory.Finiteness.Finsupp` `Mathlib.Algebra.Group.UniqueProds.Basic` `Mathlib.Data.Sum.Interval` `Mathlib.Data.Fintype.Shrink` `Mathlib.Algebra.Category.ModuleCat.Basic` `Mathlib.CategoryTheory.Limits.Final.ParallelPair` `Mathlib.Computability.TMToPartrec` `Mathlib.CategoryTheory.Limits.Filtered` `Mathlib.Topology.FiberBundle.Trivialization` `Mathlib.Data.Nat.Digits` `Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber` `Mathlib.Data.Finite.Sigma` `Mathlib.Combinatorics.Enumerative.IncidenceAlgebra` `Mathlib.Algebra.Polynomial.Eval.SMul` `Mathlib.Topology.Sheaves.Limits` `Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology` `Mathlib.Algebra.Homology.ShortComplex.QuasiIso` `Mathlib.CategoryTheory.Limits.Shapes.Countable` `Mathlib.Data.Finset.Fold` `Mathlib.Data.Matrix.Bilinear` `Mathlib.Geometry.RingedSpace.SheafedSpace` `Mathlib.LinearAlgebra.Ray` `Mathlib.Combinatorics.Young.YoungDiagram` `Mathlib.Analysis.Normed.Group.Int` `Mathlib.Analysis.Convex.Mul` `Mathlib.CategoryTheory.Dialectica.Monoidal` `Mathlib.Logic.Equiv.List` `Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp` `Mathlib.CategoryTheory.Galois.Prorepresentability` `Mathlib.Algebra.Star.Conjneg` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed` `Mathlib.Algebra.Module.Submodule.IterateMapComap` `Mathlib.Data.Finset.Filter` `Mathlib.Topology.Algebra.Group.Compact` `Mathlib.RingTheory.LocalRing.Subring` `Mathlib.Topology.StoneCech` `Mathlib.Dynamics.BirkhoffSum.Basic` `Mathlib.CategoryTheory.Abelian.Subobject` `Mathlib.Analysis.Convex.Segment` `Mathlib.SetTheory.Ordinal.Rank` `Mathlib.AlgebraicTopology.DoldKan.Faces` `Mathlib.CategoryTheory.Monoidal.Preadditive` `Mathlib.Data.DFinsupp.BigOperators` `Mathlib.Algebra.Module.Injective` `Mathlib.Topology.FiberBundle.Basic` `Mathlib.CategoryTheory.Limits.SmallComplete` `Mathlib.Topology.Separation.Profinite` `Mathlib.Algebra.Star.Center` `Mathlib.GroupTheory.Congruence.BigOperators` `Mathlib.ModelTheory.Skolem` `Mathlib.Algebra.Category.FGModuleCat.Basic` `Mathlib.RingTheory.Algebraic.Pi` `Mathlib.Algebra.Module.Presentation.DirectSum` `Mathlib.Algebra.Homology.Localization` `Mathlib.Topology.Baire.Lemmas` `Mathlib.Data.Set.SMulAntidiagonal` `Mathlib.Topology.Sheaves.SheafOfFunctions` `Mathlib.Topology.ContinuousMap.Interval` `Mathlib.RingTheory.Localization.Free` `Mathlib.Algebra.Group.Submonoid.Pointwise` `Mathlib.Algebra.Homology.ShortComplex.Preadditive` `Mathlib.CategoryTheory.Simple` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace` `Mathlib.LinearAlgebra.Eigenspace.Basic` `Mathlib.Topology.JacobsonSpace` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator` `Mathlib.Algebra.Homology.ShortComplex.Exact` `Mathlib.Algebra.Lie.EngelSubalgebra` `Mathlib.SetTheory.ZFC.Ordinal` `Mathlib.Algebra.Algebra.Subalgebra.MulOpposite` `Mathlib.CategoryTheory.Preadditive.Injective` `Mathlib.Topology.Algebra.Group.TopologicalAbelianization` `Mathlib.LinearAlgebra.TensorProduct.Tower` `Mathlib.Topology.Specialization` `Mathlib.Topology.Connected.Basic` `Mathlib.GroupTheory.ArchimedeanDensely` `Mathlib.Topology.Sheaves.LocallySurjective` `Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs` `Mathlib.NumberTheory.Padics.PadicVal.Basic` `Mathlib.Data.Finite.Vector` `Mathlib.NumberTheory.Dioph` `Mathlib.LinearAlgebra.TensorProduct.Pi` `Mathlib.AlgebraicTopology.DoldKan.Equivalence` `Mathlib.ModelTheory.Semantics` `Mathlib.Topology.Irreducible` `Mathlib.CategoryTheory.Idempotents.Basic` `Mathlib.MeasureTheory.MeasurableSpace.Basic` `Mathlib.Algebra.Jordan.Basic` `Mathlib.SetTheory.Cardinal.Subfield` `Mathlib.RingTheory.HahnSeries.Valuation` `Mathlib.Topology.Order.UpperLowerSetTopology` `Mathlib.Data.Finsupp.WellFounded` `Mathlib.RingTheory.EuclideanDomain` `Mathlib.CategoryTheory.Idempotents.FunctorExtension` `Mathlib.SetTheory.Game.Domineering` `Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq` `Mathlib.Algebra.Category.ModuleCat.Algebra` `Mathlib.RingTheory.Adjoin.Polynomial` `Mathlib.CategoryTheory.Limits.Shapes.Reflexive` `Mathlib.CategoryTheory.Limits.ExactFunctor` `Mathlib.CategoryTheory.Sites.Equivalence` `Mathlib.MeasureTheory.MeasurableSpace.Card` `Mathlib.Combinatorics.Enumerative.Bell` `Mathlib.CategoryTheory.GuitartExact.VerticalComposition` `Mathlib.Data.Multiset.Fold` `Mathlib.Data.Finite.Powerset` `Mathlib.LinearAlgebra.Quotient.Basic` `Mathlib.Algebra.Order.Antidiag.Prod` `Mathlib.Topology.UniformSpace.UniformConvergence` `Mathlib.RingTheory.LocalRing.ResidueField.Basic` `Mathlib.Order.SuccPred.LinearLocallyFinite` `Mathlib.Data.Nat.Factorization.Root` `Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves` `Mathlib.RingTheory.OreLocalization.Ring` `Mathlib.Algebra.Module.Submodule.Lattice` `Mathlib.Topology.Algebra.Constructions` `Mathlib.Topology.UniformSpace.Cauchy` `Mathlib.RingTheory.Valuation.Integers` `Mathlib.Topology.GDelta.UniformSpace` `Mathlib.Computability.DFA` `Mathlib.Order.Interval.Finset.Defs` `Mathlib.Combinatorics.Young.SemistandardTableau` `Mathlib.Algebra.DirectSum.AddChar` `Mathlib.RingTheory.KrullDimension.Basic` `Mathlib.Topology.MetricSpace.CauSeqFilter` `Mathlib.Algebra.Category.Grp.Images` `Mathlib.Order.Height` `Mathlib.Data.Multiset.Range` `Mathlib.AlgebraicTopology.DoldKan.Decomposition` `Mathlib.Algebra.Category.Grp.ZModuleEquivalence` `Mathlib.Algebra.Module.Submodule.Equiv` `Mathlib.Data.Finsupp.Pointwise` `Mathlib.LinearAlgebra.TensorProduct.Opposite` `Mathlib.Algebra.Homology.SingleHomology` `Mathlib.AlgebraicTopology.SimplexCategory` `Mathlib.Topology.EMetricSpace.Diam` `Mathlib.Topology.Order.DenselyOrdered` `Mathlib.RingTheory.HahnSeries.Summable` `Mathlib.FieldTheory.MvRatFunc.Rank` `Mathlib.NumberTheory.FactorisationProperties` `Mathlib.CategoryTheory.Sites.Canonical` `Mathlib.CategoryTheory.Subobject.Comma` `Mathlib.ModelTheory.Algebra.Field.Basic` `Mathlib.Data.Finite.Card` `Mathlib.Algebra.Algebra.Quasispectrum` `Mathlib.CategoryTheory.Closed.Types` `Mathlib.Algebra.Module.FinitePresentation` `Mathlib.RingTheory.AlgebraicIndependent.Basic` `Mathlib.Data.Multiset.OrderedMonoid` `Mathlib.Data.Fin.Tuple.BubbleSortInduction` `Mathlib.Topology.UniformSpace.Separation` `Mathlib.Topology.Compactness.Lindelof` `Mathlib.Combinatorics.SetFamily.Shatter` `Mathlib.RingTheory.EisensteinCriterion` `Mathlib.Algebra.Star.Free` `Mathlib.Topology.Hom.ContinuousEval` `Mathlib.RingTheory.Int.Basic` `Mathlib.SetTheory.Ordinal.CantorNormalForm` `Mathlib.AlgebraicTopology.DoldKan.PInfty` `Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional` `Mathlib.Algebra.Polynomial.BigOperators` `Mathlib.CategoryTheory.Sites.CoversTop` `Mathlib.Topology.Algebra.Affine` `Mathlib.Data.Finite.Set` `Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra` `Mathlib.RingTheory.Localization.Basic` `Mathlib.GroupTheory.QuotientGroup.Finite` `Mathlib.Algebra.MvPolynomial.Monad` `Mathlib.Combinatorics.Colex` `Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization` `Mathlib.Algebra.Category.Ring.Limits` `Mathlib.RingTheory.Ideal.Operations` `Mathlib.Data.Finset.PImage` `Mathlib.Algebra.Group.Pointwise.Set.Finite` `Mathlib.MeasureTheory.SetAlgebra` `Mathlib.AlgebraicTopology.SimplicialSet.Nerve` `Mathlib.SetTheory.Game.PGame` `Mathlib.Algebra.BigOperators.Group.Multiset` `Mathlib.CategoryTheory.Sites.ConcreteSheafification` `Mathlib.Topology.Algebra.Order.UpperLower` `Mathlib.SetTheory.Cardinal.CountableCover` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits` `Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant` `Mathlib.ModelTheory.Order` `Mathlib.Data.Finset.Sort` `Mathlib.LinearAlgebra.Alternating.Basic` `Mathlib.Algebra.GroupWithZero.Pointwise.Finset` `Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology` `Mathlib.LinearAlgebra.Span.Defs` `Mathlib.Order.WellFoundedSet` `Mathlib.Algebra.Colimit.Module` `Mathlib.RingTheory.Localization.NumDen` `Mathlib.Topology.Category.TopCat.Adjunctions` `Mathlib.Topology.SeparatedMap` `Mathlib.CategoryTheory.Monoidal.Subcategory` `Mathlib.Data.Finset.Empty` `Mathlib.Dynamics.Minimal` `Mathlib.Combinatorics.SimpleGraph.Operations` `Mathlib.Algebra.Category.AlgebraCat.Monoidal` `Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous` `Mathlib.Data.Finset.Card` `Mathlib.AlgebraicTopology.DoldKan.FunctorGamma` `Mathlib.CategoryTheory.Limits.Preserves.Filtered` `Mathlib.RingTheory.SimpleRing.Matrix` `Mathlib.Algebra.Order.Monoid.Canonical.Basic` `Mathlib.Control.EquivFunctor.Instances` `Mathlib.Geometry.RingedSpace.Stalks` `Mathlib.Computability.Encoding` `Mathlib.Topology.Order.LeftRightNhds` `Mathlib.CategoryTheory.FinCategory.AsType` `Mathlib.CategoryTheory.MorphismProperty.LiftingProperty` `Mathlib.Topology.UniformSpace.AbsoluteValue` `Mathlib.CategoryTheory.Adjunction.Lifting.Left` `Mathlib.Data.Finsupp.BigOperators` `Mathlib.Dynamics.BirkhoffSum.Average` `Mathlib.Data.Finset.Basic` `Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits` `Mathlib.Topology.GDelta.Basic` `Mathlib.Combinatorics.Hindman` `Mathlib.Algebra.Module.Presentation.Basic` `Mathlib.RingTheory.HahnSeries.PowerSeries` `Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic` `Mathlib.ModelTheory.ElementarySubstructures` `Mathlib.CategoryTheory.Filtered.Connected` `Mathlib.Algebra.Homology.HomologySequenceLemmas` `Mathlib.Algebra.Polynomial.Reverse` `Mathlib.Data.Set.Finite.Monad` `Mathlib.Combinatorics.SimpleGraph.Dart` `Mathlib.RingTheory.RingHom.Locally` `Mathlib.Data.Multiset.Interval` `Mathlib.LinearAlgebra.TensorProduct.DirectLimit` `Mathlib.CategoryTheory.Preadditive.Biproducts` `Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal` `Mathlib.Data.Fin.Tuple.Sort` `Mathlib.Data.Fintype.Prod` `Mathlib.RingTheory.Finiteness.Cardinality` `Mathlib.Algebra.Order.Antidiag.Finsupp` `Mathlib.Order.GameAdd` `Mathlib.Algebra.MvPolynomial.Equiv` `Mathlib.Algebra.Homology.Embedding.Boundary` `Mathlib.Order.Filter.Pi` `Mathlib.RingTheory.Ideal.IsPrimary` `Mathlib.Analysis.Convex.Function` `Mathlib.Order.Partition.Finpartition` `Mathlib.GroupTheory.Finiteness` `Mathlib.FieldTheory.RatFunc.Defs` `Mathlib.Topology.MetricSpace.Basic` `Mathlib.Algebra.Polynomial.SumIteratedDerivative` `Mathlib.CategoryTheory.Preadditive.ProjectiveResolution` `Mathlib.CategoryTheory.Limits.IndYoneda` `Mathlib.Topology.Sheaves.PresheafOfFunctions` `Mathlib.Algebra.BigOperators.Ring` `Mathlib.GroupTheory.GroupAction.Basic` `Mathlib.RingTheory.Bezout` `Mathlib.Order.BooleanGenerators` `Mathlib.SetTheory.Surreal.Multiplication` `Mathlib.Data.Multiset.Sort` `Mathlib.RingTheory.Polynomial.Nilpotent` `Mathlib.Algebra.Group.Submonoid.Finsupp` `Mathlib.CategoryTheory.Monoidal.Internal.Module` `Mathlib.Topology.Maps.Proper.UniversallyClosed` `Mathlib.LinearAlgebra.Goursat` `Mathlib.Data.ZMod.Defs` `Mathlib.Algebra.QuadraticDiscriminant` `Mathlib.Data.Nat.Factorization.Basic` `Mathlib.Algebra.Group.FiniteSupport` `Mathlib.RingTheory.Adjoin.Dimension` `Mathlib.Order.Atoms.Finite` `Mathlib.RingTheory.Polynomial.UniqueFactorization` `Mathlib.Algebra.DirectSum.Ring` `Mathlib.RingTheory.UniqueFactorizationDomain.Ideal` `Mathlib.Computability.NFA` `Mathlib.Algebra.Polynomial.Eval.Defs` `Mathlib.Data.Finset.Lattice.Lemmas` `Mathlib.CategoryTheory.EffectiveEpi.Extensive` `Mathlib.Algebra.Ring.Subsemiring.Pointwise` `Mathlib.RingTheory.LocalProperties.Submodule` `Mathlib.Algebra.Homology.HomologicalComplexAbelian` `Mathlib.Topology.MetricSpace.Defs` `Mathlib.Algebra.Algebra.Prod` `Mathlib.CategoryTheory.Preadditive.LeftExact` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField` `Mathlib.Algebra.Homology.DifferentialObject` `Mathlib.Data.QPF.Multivariate.Constructions.Comp` `Mathlib.Topology.EMetricSpace.Lipschitz` `Mathlib.Data.QPF.Multivariate.Constructions.Prj` `Mathlib.Data.ENNReal.Real` `Mathlib.Topology.Category.CompHausLike.SigmaComparison` `Mathlib.Algebra.Module.Presentation.Finite` `Mathlib.Data.Finset.Union` `Mathlib.SetTheory.Cardinal.ENat` `Mathlib.RingTheory.Finiteness.Prod` `Mathlib.Algebra.Category.MonCat.FilteredColimits` `Mathlib.Topology.RestrictGen` `Mathlib.Algebra.Group.Pointwise.Finset.Interval` `Mathlib.Topology.Separation.Hausdorff` `Mathlib.Topology.Order.OrderClosed` `Mathlib.CategoryTheory.Sites.Subcanonical` `Mathlib.Topology.Category.TopCat.Limits.Products` `Mathlib.AlgebraicTopology.SplitSimplicialObject` `Mathlib.Topology.Algebra.Order.LiminfLimsup` `Mathlib.Combinatorics.SimpleGraph.ConcreteColorings` `Mathlib.CategoryTheory.Limits.Constructions.Equalizers` `Mathlib.Topology.Sets.Compacts` `Mathlib.Topology.MetricSpace.Gluing` `Mathlib.CategoryTheory.GradedObject.Braiding` `Mathlib.AlgebraicTopology.Quasicategory.Basic` `Mathlib.RingTheory.MvPowerSeries.Order` `Mathlib.CategoryTheory.Limits.Bicones` `Mathlib.Logic.Denumerable` `Mathlib.Algebra.Order.CauSeq.BigOperators` `Mathlib.Algebra.Lie.Semisimple.Basic` `Mathlib.MeasureTheory.Constructions.Cylinders` `Mathlib.RingTheory.MvPolynomial.MonomialOrder` `Mathlib.Topology.UniformSpace.HeineCantor` `Mathlib.Algebra.Module.Submodule.EqLocus` `Mathlib.Order.Sublattice` `Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves` `Mathlib.Topology.Connected.TotallyDisconnected` `Mathlib.Deprecated.Subring` `Mathlib.RingTheory.LocalProperties.Reduced` `Mathlib.Analysis.BoxIntegral.Partition.Basic` `Mathlib.LinearAlgebra.Matrix.Symmetric` `Mathlib.RingTheory.MatrixAlgebra` `Mathlib.LinearAlgebra.Dimension.LinearMap` `Mathlib.Algebra.Lie.Derivation.Basic` `Mathlib.Analysis.Convex.Cone.Basic` `Mathlib.CategoryTheory.Idempotents.HomologicalComplex` `Mathlib.Combinatorics.Additive.Corner.Defs` `Mathlib.Order.Category.FinPartOrd` `Mathlib.Algebra.Category.AlgebraCat.Basic` `Mathlib.Algebra.Group.Subgroup.Finite` `Mathlib.Algebra.Category.CoalgebraCat.Monoidal` `Mathlib.RingTheory.Adjoin.Basic` `Mathlib.Tactic.Module` `Mathlib.LinearAlgebra.Multilinear.TensorProduct` `Mathlib.RingTheory.GradedAlgebra.Radical` `Mathlib.RingTheory.Coalgebra.Equiv` `Mathlib.Computability.Primrec` `Mathlib.Combinatorics.Enumerative.Catalan` `Mathlib.Control.Functor.Multivariate` `Mathlib.Algebra.Homology.LocalCohomology` `Mathlib.Algebra.GradedMulAction` `Mathlib.CategoryTheory.Abelian.Exact` `Mathlib.Algebra.Category.ModuleCat.Presheaf` `Mathlib.RingTheory.GradedAlgebra.Basic` `Mathlib.RingTheory.Idempotents` `Mathlib.Topology.Constructions` `Mathlib.Dynamics.Flow` `Mathlib.RingTheory.Valuation.ValuationSubring` `Mathlib.CategoryTheory.Comma.Final` `Mathlib.CategoryTheory.Shift.ShiftSequence` `Mathlib.Topology.Bornology.Hom` `Mathlib.Algebra.MvPolynomial.Cardinal` `Mathlib.Algebra.MvPolynomial.Division` `Mathlib.CategoryTheory.Idempotents.FunctorCategories` `Mathlib.Topology.Separation.Basic` `Mathlib.Combinatorics.SetFamily.HarrisKleitman` `Mathlib.Data.UInt` `Mathlib.Algebra.Polynomial.CoeffMem` `Mathlib.Topology.EMetricSpace.Paracompact` `Mathlib.Data.Sym.Card` `Mathlib.Data.Finset.SymmDiff` `Mathlib.Data.Complex.Module` `Mathlib.Algebra.Order.BigOperators.Group.Finset` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square` `Mathlib.Data.Multiset.Sections` `Mathlib.CategoryTheory.Limits.FunctorCategory.Filtered` `Mathlib.Data.ENNReal.Operations` `Mathlib.Analysis.CStarAlgebra.Module.Synonym` `Mathlib.Algebra.Group.Submonoid.Membership` `Mathlib.Algebra.Homology.QuasiIso` `Mathlib.Algebra.BigOperators.Finprod` `Mathlib.ModelTheory.Bundled` `Mathlib.Data.Finmap` `Mathlib.AlgebraicTopology.DoldKan.NCompGamma` `Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder` `Mathlib.Topology.ApproximateUnit` `Mathlib.ModelTheory.Equivalence` `Mathlib.Order.Filter.Lift` `Mathlib.LinearAlgebra.BilinearForm.Basic` `Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle` `Mathlib.LinearAlgebra.AffineSpace.Combination` `Mathlib.Topology.Sheaves.Functors` `Mathlib.Combinatorics.SetFamily.LYM` `Mathlib.Analysis.Convex.Jensen` `Mathlib.Data.DFinsupp.Ext` `Mathlib.RingTheory.Jacobson.Polynomial` `Mathlib.Data.Sym.Sym2` `Mathlib.Data.Finsupp.NeLocus` `Mathlib.CategoryTheory.Triangulated.Opposite.Basic` `Mathlib.Order.RelSeries` `Mathlib.ModelTheory.Algebra.Ring.FreeCommRing` `Mathlib.CategoryTheory.Preadditive.Opposite` `Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition` `Mathlib.Algebra.Category.Ring.Under.Basic` `Mathlib.Data.DFinsupp.Notation` `Mathlib.CategoryTheory.Sites.Over` `Mathlib.Computability.EpsilonNFA` `Mathlib.MeasureTheory.MeasurableSpace.Invariants` `Mathlib.Computability.Reduce` `Mathlib.Topology.Algebra.GroupCompletion` `Mathlib.SetTheory.Cardinal.Free` `Mathlib.Order.Interval.Finset.Box` `Mathlib.CategoryTheory.Subobject.Lattice` `Mathlib.Data.Matroid.IndepAxioms` `Mathlib.NumberTheory.BernoulliPolynomials` `Mathlib.Algebra.MonoidAlgebra.Grading` `Mathlib.RingTheory.RingHomProperties` `Mathlib.LinearAlgebra.BilinearForm.TensorProduct` `Mathlib.RingTheory.TensorProduct.Pi` `Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit` `Mathlib.CategoryTheory.Sites.MayerVietorisSquare` `Mathlib.Data.Real.EReal` `Mathlib.Combinatorics.SetFamily.Intersecting` `Mathlib.Algebra.FreeAlgebra.Cardinality` `Mathlib.Topology.Category.Sequential` `Mathlib.RingTheory.Ideal.Prime` `Mathlib.Data.PFunctor.Univariate.Basic` `Mathlib.ModelTheory.Types` `Mathlib.Analysis.Convex.Strict` `Mathlib.RingTheory.Valuation.Quotient` `Mathlib.Topology.Compactness.SigmaCompact` `Mathlib.Algebra.Category.Ring.Constructions` `Mathlib.CategoryTheory.Generator.Presheaf` `Mathlib.RingTheory.Polynomial.Eisenstein.Basic` `Mathlib.CategoryTheory.Abelian.NonPreadditive` `Mathlib.Algebra.CharP.LinearMaps` `Mathlib.Data.Finite.Sum` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification` `Mathlib.LinearAlgebra.Dimension.Free` `Mathlib.Order.Filter.Cocardinal` `Mathlib.Algebra.CharP.Reduced` `Mathlib.Data.QPF.Multivariate.Constructions.Sigma` `Mathlib.Algebra.Module.Presentation.RestrictScalars` `Mathlib.Algebra.Lie.BaseChange` `Mathlib.Data.Nat.PartENat` `Mathlib.Algebra.Algebra.Subalgebra.Unitization` `Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating` `Mathlib.CategoryTheory.Sites.CoverPreserving` `Mathlib.LinearAlgebra.Isomorphisms` `Mathlib.Topology.DiscreteQuotient` `Mathlib.Order.KonigLemma` `Mathlib.Topology.UniformSpace.Pi` `Mathlib.LinearAlgebra.Dual` `Mathlib.LinearAlgebra.TensorProduct.RightExactness` `Mathlib.Algebra.Group.Subgroup.Pointwise` `Mathlib.Topology.MetricSpace.ProperSpace.Lemmas` `Mathlib.Algebra.Category.Grp.Limits` `Mathlib.Algebra.Lie.CartanMatrix` `Mathlib.Algebra.Central.Basic` `Mathlib.Topology.Compactness.Compact` `Mathlib.RingTheory.Valuation.ValExtension` `Mathlib.Combinatorics.SimpleGraph.Acyclic` `Mathlib.Algebra.Star.Subsemiring` `Mathlib.Analysis.Convex.Combination` `Mathlib.Data.Matrix.Mul` `Mathlib.ModelTheory.Fraisse` `Mathlib.RingTheory.Bialgebra.Equiv` `Mathlib.AlgebraicTopology.ExtraDegeneracy` `Mathlib.Combinatorics.SimpleGraph.Hasse` `Mathlib.Topology.Sets.Opens` `Mathlib.Algebra.Polynomial.Lifts` `Mathlib.Data.QPF.Univariate.Basic` `Mathlib.Data.Finset.Attach` `Mathlib.Data.Nat.Choose.Multinomial` `Mathlib.CategoryTheory.Monoidal.Types.Symmetric` `Mathlib.CategoryTheory.Sites.PreservesLocallyBijective` `Mathlib.Order.UpperLower.LocallyFinite` `Mathlib.CategoryTheory.Sites.LocallyBijective` `Mathlib.RingTheory.Polynomial.ScaleRoots` `Mathlib.Topology.Category.CompHausLike.Limits` `Mathlib.RingTheory.FractionalIdeal.Operations` `Mathlib.Data.Nat.ChineseRemainder` `Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite` `Mathlib.Analysis.Convex.Hull` `Mathlib.Data.Finsupp.MonomialOrder.DegLex` `Mathlib.GroupTheory.FreeGroup.Reduce` `Mathlib.Algebra.Homology.Linear` `Mathlib.CategoryTheory.Sites.OneHypercover` `Mathlib.Data.Fintype.Pi` `Mathlib.Algebra.MonoidAlgebra.Division` `Mathlib.Analysis.Convex.Star` `Mathlib.Data.Finset.Sigma` `Mathlib.Algebra.Lie.UniversalEnveloping` `Mathlib.Topology.Algebra.Order.Group` `Mathlib.CategoryTheory.Sites.DenseSubsite.Basic` `Mathlib.Topology.EMetricSpace.Pi` `Mathlib.CategoryTheory.Sites.Types` `Mathlib.Data.Set.Finite.Lattice` `Mathlib.Topology.Order.Category.AlexDisc` `Mathlib.Topology.Algebra.InfiniteSum.Order` `Mathlib.Combinatorics.SetFamily.Compression.Down` `Mathlib.ModelTheory.Algebra.Field.CharP` `Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange` `Mathlib.Algebra.Polynomial.Eval.Coeff` `Mathlib.Topology.Algebra.InfiniteSum.Defs` `Mathlib.RingTheory.Ideal.Pointwise` `Mathlib.RingTheory.Ideal.Colon` `Mathlib.LinearAlgebra.Basis.Basic` `Mathlib.Topology.Defs.Ultrafilter` `Mathlib.Data.Finsupp.Lex` `Mathlib.Algebra.Polynomial.Degree.Lemmas` `Mathlib.Data.Fintype.Perm` `Mathlib.Order.Filter.Finite` `Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono` `Mathlib.Analysis.Convex.Basic` `Mathlib.Combinatorics.Pigeonhole` `Mathlib.Topology.LocallyConstant.Algebra` `Mathlib.Algebra.CharZero.Infinite` `Mathlib.CategoryTheory.Limits.VanKampen` `Mathlib.Topology.Sheaves.Skyscraper` `Mathlib.Topology.MetricSpace.Bilipschitz` `Mathlib.CategoryTheory.Abelian.InjectiveResolution` `Mathlib.InformationTheory.Hamming` `Mathlib.Algebra.CharP.Algebra` `Mathlib.Data.Finset.Range` `Mathlib.RingTheory.Localization.Module` `Mathlib.Algebra.Lie.Subalgebra` `Mathlib.RingTheory.MvPolynomial.Basic` `Mathlib.Algebra.Polynomial.Monomial` `Mathlib.ModelTheory.Basic` `Mathlib.Algebra.MvPolynomial.PDeriv` `Mathlib.CategoryTheory.Abelian.GrothendieckCategory` `Mathlib.Data.Sign` `Mathlib.Data.Finsupp.Interval` `Mathlib.Algebra.Lie.Sl2` `Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts` `Mathlib.Algebra.Module.LocalizedModule.Exact` `Mathlib.Data.Nat.Factorial.Cast` `Mathlib.Logic.Equiv.Fintype` `Mathlib.Data.Matrix.RowCol` `Mathlib.RingTheory.FreeCommRing` `Mathlib.Algebra.BigOperators.GroupWithZero.Finset` `Mathlib.Tactic.NormNum.IsCoprime` `Mathlib.RingTheory.PowerSeries.Order` `Mathlib.Data.Fin.Tuple.Reflection` `Mathlib.CategoryTheory.Limits.Over` `Mathlib.Data.ENat.Lattice` `Mathlib.Dynamics.FixedPoints.Topology` `Mathlib.Algebra.Category.Grp.Biproducts` `Mathlib.RingTheory.Valuation.PrimeMultiplicity` `Mathlib.CategoryTheory.Preadditive.InjectiveResolution` `Mathlib.Algebra.MvPolynomial.CommRing` `Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections` `Mathlib.CategoryTheory.Preadditive.HomOrthogonal` `Mathlib.Analysis.Convex.Extrema` `Mathlib.Algebra.Homology.Embedding.Restriction` `Mathlib.Algebra.Homology.ExactSequence` `Mathlib.Analysis.Convex.Extreme` `Mathlib.Data.Finset.Density` `Mathlib.Analysis.Convex.Visible` `Mathlib.CategoryTheory.Adjunction.Lifting.Right` `Mathlib.Data.QPF.Multivariate.Constructions.Const` `Mathlib.Data.Multiset.Fintype` `Mathlib.CategoryTheory.Functor.FunctorHom` `Mathlib.Algebra.Ring.Subsemiring.Basic` `Mathlib.LinearAlgebra.Dimension.Constructions` `Mathlib.Topology.Algebra.Localization` `Mathlib.RingTheory.LocalProperties.Basic` `Mathlib.Algebra.Algebra.Bilinear` `Mathlib.Algebra.Order.BigOperators.Group.Multiset` `Mathlib.SetTheory.Ordinal.FixedPoint` `Mathlib.Data.Fintype.Vector` `Mathlib.Combinatorics.SimpleGraph.Prod` `Mathlib.LinearAlgebra.Dimension.ErdosKaplansky` `Mathlib.Algebra.Category.Grp.Colimits` `Mathlib.Data.Matrix.DualNumber` `Mathlib.Data.Matroid.Restrict` `Mathlib.CategoryTheory.Limits.Indization.FilteredColimits` `Mathlib.Combinatorics.SimpleGraph.Subgraph` `Mathlib.Algebra.Lie.Solvable` `Mathlib.AlgebraicTopology.AlternatingFaceMapComplex` `Mathlib.Algebra.Group.UniqueProds.VectorSpace` `Mathlib.Topology.Order.T5` `Mathlib.MeasureTheory.MeasurableSpace.Instances` `Mathlib.Topology.KrullDimension` `Mathlib.Data.Finset.NoncommProd` `Mathlib.CategoryTheory.Abelian.LeftDerived` `Mathlib.MeasureTheory.PiSystem` `Mathlib.RingTheory.Ideal.Quotient.Operations` `Mathlib.CategoryTheory.Limits.Indization.Equalizers` `Mathlib.Data.ENNReal.Lemmas` `Mathlib.Algebra.Homology.Homotopy` `Mathlib.LinearAlgebra.TensorPower` `Mathlib.CategoryTheory.Linear.LinearFunctor` `Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects` `Mathlib.Algebra.QuaternionBasis` `Mathlib.NumberTheory.Basic` `Mathlib.RingTheory.Artinian.Instances` `Mathlib.NumberTheory.Bernoulli` `Mathlib.Algebra.Polynomial.UnitTrinomial` `Mathlib.Topology.Hom.ContinuousEvalConst` `Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ` `Mathlib.Data.Finsupp.ToDFinsupp` `Mathlib.MeasureTheory.SetSemiring` `Mathlib.Topology.Order.Priestley` `Mathlib.CategoryTheory.MorphismProperty.OverAdjunction` `Mathlib.RingTheory.LocalRing.RingHom.Basic` `Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory` `Mathlib.CategoryTheory.Extensive` `Mathlib.Algebra.Homology.CommSq` `Mathlib.Algebra.Algebra.Equiv` `Mathlib.CategoryTheory.LiftingProperties.Limits` `Mathlib.Order.Filter.AtTopBot.Monoid` `Mathlib.AlgebraicTopology.SimplicialObject.Basic` `Mathlib.Data.DFinsupp.Lex` `Mathlib.CategoryTheory.ChosenFiniteProducts` `Mathlib.Topology.Perfect` `Mathlib.Data.List.Sym` `Mathlib.LinearAlgebra.Dimension.StrongRankCondition` `Mathlib.Data.Matrix.Hadamard` `Mathlib.Analysis.Normed.Group.Submodule` `Mathlib.Combinatorics.SetFamily.KruskalKatona` `Mathlib.Order.Filter.CountableSeparatingOn` `Mathlib.CategoryTheory.Enriched.HomCongr` `Mathlib.CategoryTheory.Limits.MorphismProperty` `Mathlib.ModelTheory.DirectLimit` `Mathlib.Algebra.Lie.Engel` `Mathlib.Data.Nat.Fib.Zeckendorf` `Mathlib.Topology.Sheaves.PUnit` `Mathlib.Algebra.Category.ModuleCat.Free` `Mathlib.Data.Multiset.Pi` `Mathlib.Algebra.Polynomial.Basic` `Mathlib.Algebra.Algebra.Subalgebra.Directed` `Mathlib.Algebra.Central.Matrix` `Mathlib.CategoryTheory.Monad.Coequalizer` `Mathlib.RingTheory.FiniteLength` `Mathlib.Algebra.MvPolynomial.Polynomial` `Mathlib.Algebra.Polynomial.Basis` `Mathlib.AlgebraicTopology.MooreComplex` `Mathlib.Algebra.MonoidAlgebra.Defs` `Mathlib.NumberTheory.Zsqrtd.Basic` `Mathlib.Topology.Compactness.Paracompact` `Mathlib.Data.Finset.Preimage` `Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite` `Mathlib.Topology.Sheaves.Presheaf` `Mathlib.Algebra.GeomSum` `Mathlib.CategoryTheory.Adhesive` `Mathlib.CategoryTheory.Closed.Enrichment` `Mathlib.RingTheory.SimpleRing.Field` `Mathlib.CategoryTheory.Limits.Shapes.Biproducts` `Mathlib.Data.FunLike.Fintype` `Mathlib.RingTheory.Ideal.Lattice` `Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra` `Mathlib.RingTheory.Ideal.IdempotentFG` `Mathlib.Algebra.CharP.Lemmas` `Mathlib.SetTheory.Nimber.Basic` `Mathlib.RingTheory.MvPowerSeries.Trunc` `Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic` `Mathlib.Computability.PartrecCode` `Mathlib.RingTheory.Finiteness.Ideal` `Mathlib.CategoryTheory.Closed.Zero` `Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory` `Mathlib.LinearAlgebra.PiTensorProduct` `Mathlib.LinearAlgebra.Finsupp.Span` `Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat` `Mathlib.Topology.Order.IntermediateValue` `Mathlib.CategoryTheory.Closed.FunctorToTypes` `Mathlib.Topology.Algebra.Order.Floor` `Mathlib.Data.Rat.Cardinal` `Mathlib.Topology.Category.TopCat.Limits.Basic` `Mathlib.RingTheory.Finiteness.Defs` `Mathlib.CategoryTheory.Limits.Lattice` `Mathlib.Topology.IsLocalHomeomorph` `Mathlib.Data.Int.CardIntervalMod` `Mathlib.RingTheory.MvPowerSeries.Basic` `Mathlib.Data.QPF.Multivariate.Constructions.Cofix` `Mathlib.Algebra.MonoidAlgebra.Basic` `Mathlib.SetTheory.Game.Ordinal` `Mathlib.Analysis.NormedSpace.IndicatorFunction` `Mathlib.Algebra.Category.ModuleCat.Projective` `Mathlib.RingTheory.MaximalSpectrum` `Mathlib.Algebra.Homology.HomotopyCofiber` `Mathlib.NumberTheory.Padics.PadicVal.Defs` `Mathlib.Algebra.Polynomial.Roots` `Mathlib.Combinatorics.Digraph.Basic` `Mathlib.Algebra.Homology.Augment` `Mathlib.Analysis.Normed.Group.Constructions` `Mathlib.RingTheory.Ideal.Basic` `Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv` `Mathlib.Tactic.DeriveFintype` `Mathlib.RingTheory.FiniteType` `Mathlib.RingTheory.Ideal.Basis` `Mathlib.CategoryTheory.Limits.FintypeCat` `Mathlib.CategoryTheory.Sites.Adjunction` `Mathlib.Data.Multiset.Powerset` `Mathlib.Computability.Ackermann` `Mathlib.Algebra.Category.ModuleCat.Images` `Mathlib.CategoryTheory.Idempotents.Karoubi` `Mathlib.CategoryTheory.EffectiveEpi.Preserves` `Mathlib.CategoryTheory.Limits.EpiMono` `Mathlib.Topology.Category.TopCat.Yoneda` `Mathlib.Algebra.CharP.IntermediateField` `Mathlib.Algebra.Algebra.NonUnitalSubalgebra` `Mathlib.Topology.UniformSpace.UniformConvergenceTopology` `Mathlib.Combinatorics.SimpleGraph.Finite` `Mathlib.SetTheory.Cardinal.ToNat` `Mathlib.Data.Nat.Factorization.PrimePow` `Mathlib.GroupTheory.MonoidLocalization.Cardinality` `Mathlib.LinearAlgebra.Projectivization.Subspace` `Mathlib.Data.List.Pi` `Mathlib.RingTheory.Finiteness.Projective` `Mathlib.Topology.Category.TopCommRingCat` `Mathlib.Order.Filter.AtTopBot.Group` `Mathlib.Data.MLList.BestFirst` `Mathlib.Analysis.Convex.Caratheodory` `Mathlib.Data.Finsupp.AList` `Mathlib.LinearAlgebra.AffineSpace.Slope` `Mathlib.Algebra.BigOperators.WithTop` `Mathlib.Topology.Order.Bornology` `Mathlib.Analysis.Convex.Quasiconvex` `Mathlib.GroupTheory.OreLocalization.Cardinality` `Mathlib.Deprecated.Subfield` `Mathlib.Algebra.GCDMonoid.Finset` `Mathlib.CategoryTheory.Closed.Cartesian` `Mathlib.Data.PFunctor.Multivariate.Basic` `Mathlib.Data.PNat.Interval` `Mathlib.Topology.OmegaCompletePartialOrder` `Mathlib.FieldTheory.IntermediateField.Basic` `Mathlib.Computability.RegularExpressions` `Mathlib.Algebra.BigOperators.NatAntidiagonal` `Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi` `Mathlib.RingTheory.Ideal.Prod` `Mathlib.Order.Filter.Extr` `Mathlib.Algebra.Polynomial.CancelLeads` `Mathlib.Algebra.MvPolynomial.Degrees` `Mathlib.Topology.Algebra.GroupWithZero` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal` `Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient` `Mathlib.CategoryTheory.Idempotents.Biproducts` `Mathlib.Algebra.Algebra.Hom` `Mathlib.Combinatorics.Optimization.ValuedCSP` `Mathlib.Algebra.DirectSum.Algebra` `Mathlib.Topology.Connected.Separation` `Mathlib.LinearAlgebra.Finsupp.Defs` `Mathlib.Combinatorics.SimpleGraph.IncMatrix` `Mathlib.RingTheory.PrincipalIdealDomainOfPrime` `Mathlib.Topology.Category.UniformSpace` `Mathlib.CategoryTheory.Linear.Yoneda` `Mathlib.RingTheory.Localization.Cardinality` `Mathlib.Topology.Order.ExtrClosure` `Mathlib.CategoryTheory.Sites.Coherent.SheafComparison` `Mathlib.FieldTheory.Tower` `Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs` `Mathlib.RingTheory.HahnSeries.Multiplication` `Mathlib.RingTheory.TensorProduct.Free` `Mathlib.CategoryTheory.Preadditive.EndoFunctor` `Mathlib.Topology.Category.FinTopCat` `Mathlib.NumberTheory.FLT.Basic` `Mathlib.MeasureTheory.Constructions.SubmoduleQuotient` `Mathlib.Algebra.Homology.HomologySequence` `Mathlib.SetTheory.Cardinal.Finite` `Mathlib.Data.Nat.Lattice` `Mathlib.CategoryTheory.Comma.Presheaf.Colimit` `Mathlib.RingTheory.PrimeSpectrum` `Mathlib.Topology.Algebra.Support` `Mathlib.Topology.Separation.GDelta` `Mathlib.Geometry.RingedSpace.PresheafedSpace` `Mathlib.Topology.Algebra.Module.WeakBilin` `Mathlib.Algebra.CharP.MixedCharZero` `Mathlib.Analysis.Normed.Order.Hom.Ultra` `Mathlib.Algebra.Polynomial.Identities` `Mathlib.Data.Set.Card` `Mathlib.Data.Finsupp.Order` `Mathlib.Topology.Metrizable.Uniformity` `Mathlib.CategoryTheory.Category.Grpd` `Mathlib.Topology.ContinuousMap.T0Sierpinski` `Mathlib.Topology.Metrizable.ContinuousMap` `Mathlib.Algebra.Polynomial.EraseLead` `Mathlib.Algebra.MvPolynomial.Invertible` `Mathlib.CategoryTheory.Limits.Preserves.Finite` `Mathlib.Data.Finset.NAry` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian` `Mathlib.CategoryTheory.Preadditive.FunctorCategory` `Mathlib.RingTheory.RingHom.Surjective` `Mathlib.Topology.UniformSpace.Equicontinuity` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward` `Mathlib.Data.Matrix.ConjTranspose` `Mathlib.Algebra.Order.Field.Pi` `Mathlib.LinearAlgebra.Dimension.Finite` `Mathlib.RingTheory.Finiteness.Nilpotent` `Mathlib.RingTheory.FreeRing` `Mathlib.Analysis.Convex.StoneSeparation` `Mathlib.LinearAlgebra.Basis.Bilinear` `Mathlib.Algebra.Algebra.NonUnitalHom` `Mathlib.Data.Nat.Prime.Nth` `Mathlib.Algebra.Polynomial.Degree.Units` `Mathlib.Topology.Separation.Regular` `Mathlib.Algebra.DualNumber` `Mathlib.AlgebraicTopology.SimplicialCategory.Basic` `Mathlib.Topology.Category.TopCat.EffectiveEpi` `Mathlib.CategoryTheory.Linear.FunctorCategory` `Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers` `Mathlib.Algebra.Star.Unitary` `Mathlib.SetTheory.ZFC.Rank` `Mathlib.MeasureTheory.MeasurableSpace.Prod` `Mathlib.Order.PartialSups` `Mathlib.Topology.Order.Hom.Basic` `Mathlib.Topology.Order.IsLUB` `Mathlib.Algebra.Homology.ShortComplex.ShortExact` `Mathlib.SetTheory.Ordinal.FixedPointApproximants` `Mathlib.Algebra.Polynomial.Eval.Subring` `Mathlib.LinearAlgebra.LinearPMap` `Mathlib.Analysis.Convex.Radon` `Mathlib.Algebra.Category.Ring.Adjunctions` `Mathlib.Algebra.Lie.TensorProduct` `Mathlib.Order.Interval.Finset.Nat` `Mathlib.Algebra.Homology.HomotopyCategory` `Mathlib.Algebra.Star.CentroidHom` `Mathlib.Data.DFinsupp.Submonoid` `Mathlib.Algebra.BigOperators.Expect` `Mathlib.Algebra.SkewMonoidAlgebra.Basic` `Mathlib.LinearAlgebra.TensorProduct.Basic` `Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous` `Mathlib.Algebra.Homology.ShortComplex.Limits` `Mathlib.LinearAlgebra.Prod` `Mathlib.Data.Finset.MulAntidiagonal` `Mathlib.Topology.Sheaves.Sheafify` `Mathlib.LinearAlgebra.TensorProduct.Basis` `Mathlib.Topology.MetricSpace.DilationEquiv` `Mathlib.FieldTheory.RatFunc.Basic` `Mathlib.RingTheory.Support` `Mathlib.Topology.Algebra.Constructions.DomMulAct` `Mathlib.Algebra.Field.Subfield.Basic` `Mathlib.RepresentationTheory.Maschke` `Mathlib.Analysis.BoxIntegral.Partition.Split` `Mathlib.Topology.Compactness.Exterior` `Mathlib.RingTheory.Valuation.Basic` `Mathlib.CategoryTheory.MorphismProperty.Limits` `Mathlib.Algebra.Category.HopfAlgebraCat.Basic` `Mathlib.Data.DFinsupp.Order` `Mathlib.SetTheory.Surreal.Basic` `Mathlib.Topology.MetricSpace.Ultra.TotallySeparated` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify` `Mathlib.Data.Matrix.Notation` `Mathlib.RingTheory.Localization.FractionRing` `Mathlib.RingTheory.TensorProduct.Basic` `Mathlib.LinearAlgebra.AffineSpace.Midpoint` `Mathlib.Algebra.Module.Submodule.LinearMap` `Mathlib.Data.Finite.Prod` `Mathlib.ModelTheory.ElementaryMaps` `Mathlib.Combinatorics.SimpleGraph.AdjMatrix` `Mathlib.Algebra.Module.GradedModule` `Mathlib.Algebra.Polynomial.Degree.TrailingDegree` `Mathlib.Topology.Order.MonotoneContinuity` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent` `Mathlib.RingTheory.Valuation.RankOne` `Mathlib.LinearAlgebra.Dimension.RankNullity` `Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct` `Mathlib.Algebra.Algebra.Tower` `Mathlib.LinearAlgebra.Basis.Flag` `Mathlib.CategoryTheory.Functor.Flat` `Mathlib.Analysis.Normed.Group.AddTorsor` `Mathlib.AlgebraicTopology.DoldKan.FunctorN` `Mathlib.CategoryTheory.Shift.ShiftedHom` `Mathlib.Algebra.Group.Subgroup.Finsupp` `Mathlib.Combinatorics.Derangements.Finite` `Mathlib.LinearAlgebra.Basis.Cardinality` `Mathlib.Algebra.Polynomial.Cardinal` `Mathlib.Algebra.Lie.InvariantForm` `Mathlib.ModelTheory.Satisfiability` `Mathlib.Topology.Algebra.InfiniteSum.Basic` `Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic` `Mathlib.Topology.AlexandrovDiscrete` `Mathlib.Data.Matroid.Sum` `Mathlib.Tactic.Algebraize` `Mathlib.Topology.UniformSpace.Equiv` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits` `Mathlib.CategoryTheory.Limits.FunctorCategory.Finite` `Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent` `Mathlib.Topology.Ultrafilter` `Mathlib.Order.Filter.AtTopBot.Floor` `Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated` `Mathlib.Algebra.Homology.ShortComplex.ExactFunctor` `Mathlib.Order.CompactlyGenerated.Basic` `Mathlib.Data.Nat.PrimeFin` `Mathlib.RingTheory.Ideal.BigOperators` `Mathlib.Algebra.Homology.Embedding.StupidTrunc` `Mathlib.Algebra.Polynomial.Module.AEval` `Mathlib.Data.Finset.Prod` `Mathlib.NumberTheory.FLT.MasonStothers` `Mathlib.Data.PNat.Factors` `Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings` `Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable` `Mathlib.Algebra.Module.Submodule.Ker` `Mathlib.LinearAlgebra.FreeModule.Basic` `Mathlib.Data.Sym.Sym2.Order` `Mathlib.CategoryTheory.FinCategory.Basic` `Mathlib.Topology.Sheaves.Stalks` `Mathlib.Topology.ContinuousOn` `Mathlib.CategoryTheory.Sites.Plus` `Mathlib.CategoryTheory.Limits.Final` `Mathlib.Algebra.FreeAlgebra` `Mathlib.CategoryTheory.Shift.Pullback` `Mathlib.RingTheory.PowerSeries.Trunc` `Mathlib.GroupTheory.Perm.Subgroup` `Mathlib.Algebra.Order.Rearrangement` `Mathlib.RingTheory.Ideal.Nonunits` `Mathlib.SetTheory.Ordinal.Basic` `Mathlib.CategoryTheory.Enriched.Ordinary` `Mathlib.Algebra.Category.ModuleCat.EpiMono` `Mathlib.Order.Filter.CardinalInter` `Mathlib.Analysis.Normed.Group.Basic` `Mathlib.Combinatorics.SimpleGraph.Coloring` `Mathlib.Algebra.Homology.ConcreteCategory` `Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain` `Mathlib.Combinatorics.Enumerative.Partition` `Mathlib.CategoryTheory.Sites.CompatibleSheafification` `Mathlib.LinearAlgebra.Multilinear.DFinsupp` `Mathlib.Topology.Algebra.InfiniteSum.Constructions` `Mathlib.Topology.Exterior` `Mathlib.Algebra.Homology.Factorizations.Basic` `Mathlib.Algebra.Group.ConjFinite` `Mathlib.Data.List.ToFinsupp` `Mathlib.Algebra.BigOperators.Module` `Mathlib.Algebra.BigOperators.Fin` `Mathlib.Combinatorics.SimpleGraph.Ends.Properties` `Mathlib.RingTheory.PowerSeries.Basic` `Mathlib.LinearAlgebra.Matrix.SemiringInverse` `Mathlib.RingTheory.TensorProduct.MvPolynomial` `Mathlib.LinearAlgebra.TensorProduct.Vanishing` `Mathlib.Algebra.Module.Submodule.Pointwise` `Mathlib.Order.Filter.EventuallyConst` `Mathlib.Algebra.Polynomial.Smeval` `Mathlib.LinearAlgebra.StdBasis` `Mathlib.RingTheory.Localization.Algebra` `Mathlib.Order.KrullDimension` `Mathlib.Topology.MetricSpace.Pseudo.Defs` `Mathlib.Logic.Godel.GodelBetaFunction` `Mathlib.LinearAlgebra.Matrix.Circulant` `Mathlib.LinearAlgebra.Matrix.Dual` `Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors` `Mathlib.LinearAlgebra.Matrix.Orthogonal` `Mathlib.CategoryTheory.Preadditive.Yoneda.Limits` `Mathlib.Data.Multiset.Dedup` `Mathlib.RingTheory.LocalProperties.Projective` `Mathlib.Data.Fintype.Lattice` `Mathlib.Topology.Instances.Sign` `Mathlib.Combinatorics.SimpleGraph.Basic` `Mathlib.Topology.MetricSpace.Pseudo.Constructions` `Mathlib.LinearAlgebra.AffineSpace.AffineMap` `Mathlib.LinearAlgebra.Basis.VectorSpace` `Mathlib.CategoryTheory.Sites.Coherent.RegularTopology` `Mathlib.Data.Set.Finite.Lemmas` `Mathlib.Algebra.Homology.Embedding.ExtendHomology` `Mathlib.Data.Multiset.Lattice` `Mathlib.RingTheory.Derivation.DifferentialRing` `Mathlib.Topology.Category.TopCat.Limits.Pullbacks` `Mathlib.FieldTheory.Differential.Basic` `Mathlib.Algebra.Lie.OfAssociative` `Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat` `Mathlib.Algebra.Colimit.Ring` `Mathlib.GroupTheory.FreeAbelianGroup` `Mathlib.RingTheory.PowerSeries.Inverse` `Mathlib.LinearAlgebra.AffineSpace.AffineSubspace` `Mathlib.Data.Analysis.Filter` `Mathlib.Topology.Inseparable` `Mathlib.AlgebraicTopology.DoldKan.NReflectsIso` `Mathlib.Order.Filter.Interval` `Mathlib.CategoryTheory.Limits.Sifted` `Mathlib.Algebra.Polynomial.Div` `Mathlib.Topology.MetricSpace.Bounded` `Mathlib.AlgebraicTopology.DoldKan.Degeneracies` `Mathlib.LinearAlgebra.FreeProduct.Basic` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Free` `Mathlib.AlgebraicTopology.DoldKan.Projections` `Mathlib.Topology.QuasiSeparated` `Mathlib.Algebra.Homology.Embedding.TruncGE` `Mathlib.CategoryTheory.Filtered.OfColimitCommutesFiniteLimit` `Mathlib.Topology.Maps.Basic` `Mathlib.Algebra.Module.LocalizedModule.Submodule` `Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit` `Mathlib.RingTheory.Ideal.Quotient.Basic` `Mathlib.CategoryTheory.Sites.CoverLifting` `Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict` `Mathlib.LinearAlgebra.Projectivization.Basic` `Mathlib.Topology.Algebra.Order.Archimedean` `Mathlib.Topology.MetricSpace.MetricSeparated`	1

Declarations diff

+ instDistribLattice
+ instLattice
+ instance : Inter (Multiset α) := ⟨inter⟩
+ instance : Sub (Multiset α) := ⟨.sub⟩
+ instance : Union (Multiset α) := ⟨union⟩
- instance : DistribLattice (Multiset α)
- instance : Inter (Multiset α)
- instance : Lattice (Multiset α)
- instance : Sub (Multiset α)
- instance : Union (Multiset α)

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) = (1.00, 0.00)

Current number	Change	Type
202	1	disabled simpNF lints

Current commit df14c3cf54
Reference commit 14950c530f

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

b-mehta · 2024-12-10T15:48:38Z

Can you please add to the PR description a more accurate summary of what's changing in this PR, rather than "other cleanups"? It looks to me like you are

changing docs
moving lemmas around which don't involve sub
changing proofs
changing the simp-set
changing the implicitness of lemmas

Timeroot · 2024-12-12T23:52:38Z

Sorry about that, fat finger.

mathlib4-dependent-issues-bot · 2024-12-20T06:03:28Z

This PR/issue depends on:

~~[Merged by Bors] - chore(Multiset): make all arguments to inter_le_left, etc... implicit #20045~~
By Dependent Issues (🤖). Happy coding!

Vierkantor

Happy new year! :) Please don't forget this comment:

Can you please add to the PR description a more accurate summary of what's changing in this PR, rather than "other cleanups"?

In addition I have a few minor remarks, but LGTM overall.

Mathlib/Data/Multiset/Basic.lean

Vierkantor · 2025-01-06T09:49:32Z

Mathlib/Data/Multiset/Basic.lean

+
+@[simp]
+lemma count_sub (a : α) (s t : Multiset α) : count a (s - t) = count a s - count a t :=
+  Quotient.inductionOn₂ s t <| by simp [List.count_diff]


This is indeed a nice change!

Mathlib/Data/Multiset/Basic.lean

and other cleanups that will be used to stop importing algebra here

YaelDillies · 2025-01-06T11:48:21Z

Sorry, I had forgotten. Done now!

Vierkantor · 2025-01-06T11:49:50Z

Thanks! Let's wait for the build to succeed, then it looks good for borsifying.

bors d+

mathlib-bors · 2025-01-06T11:49:53Z

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

leanprover-community-mathlib4-bot · 2025-01-06T12:27:23Z

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

… lower (#19863) * Move the sections about `sub`, `union` and `inter` under the sections about `count` and `filter` * `Multiset.countP_sub` now has a different argument order to match `List.countP_diff` * Golf `List.count_sub` * Name the instances and declare them using `where` notation * Define `Multiset.card` using `Quotient.lift`, not `Quotient.liftOn`

mathlib-bors · 2025-01-06T13:13:23Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (189 commits) chore(Algebra): make more names consistent (#20449) feat: Polynomial FLT (#18882) feat: A disjoint union is finite iff all sets are finite, and all but finitely many are empty (#20457) fix: linkfix in 100.yaml (#20517) feat(1000): fill in more entries (#20470) feat(Combinatorics/SimpleGraph/Walk): add `penultimate` and `snd` (#16769) feat(ContinuousMultilinearMap): add lemmas about `.prod` (#20462) feat(RingTheory): classification of etale algebras over fields (#20324) fix: Allow multiple builds on staging branch (#20515) feat(CategoryTheory/Shift/Adjunction): properties of `Adjunction.CommShift` (#20337) chore(Data/Multiset/Basic): move the `sub`, `union`, `inter` sections lower (#19863) chore(Topology/UniformSpace/Completion): make coe' argument implicit (#20514) refactor(Algebra/Category/Grp/Colimits): change the construction of colimits in `AddCommGrp` (#20474) feat(Topology/Algebra/InfiniteSum/NatInt): Add pnat lems (#16544) chore(RingTheory/Finiteness): rename Module.Finite.out (#20506) refactor(CategoryTheory/Limits/Preserves/Ulift): simplify the proof that the universe lifting functor for types preserves all colimits (#20508) feat(CategoryTheory): products in the category of Ind-objects (#20507) chore: remove >9 month old deprecations (#20505) chore(FieldTheory/Galois): small cleanup (#20217) chore(LinearIndependent): generalize to semirings (#20480) chore(NumberTheory/NumberField/AdeleRing): refactor adele rings (#20500) chore: replace `aesop` with `simp` where possible (#20483) chore(1000): remove nonexistent fields (#20493) chore(CategoryTheory/Adjunction.Basic, CategoryTheory/Equivalence): change definition of `Adjunction.comp` and `Equivalence.trans` (#20490) feat(Asymptotics): add `Asymptotics.*.*Prod` lemmas (#20458) feat: a conditional kernel is almost everywhere a probability measure (#20430) feat: if `f` is a measurable group hom, then every point has a neighborhood `s` such that `f '' s` is bounded (#20304) feat: `Ico`, `Ioc`, and `Ioo` are not closed or compact (#20479) chore: drop redundant hypothesis in `Module.Dual.eq_of_preReflection_mapsTo` (#20492) feat(FaaDiBruno): derive `DecidableEq` (#20482) chore(SetTheory/Ordinal/Basic): `{x // x < y}` → `Iio y` (#20413) chore: generalize `FormalMultilinearSeries.ofScalars_norm` to `Seminormed` (#20351) chore(MvPolynomial/Localization): golf using TensorProduct (#20309) chore(Combinatorics/Enumerative/Partition): auto-derive DecidableEq (#20277) chore(CategoryTheory): make relevant parameters explicit in `Arrow.homMk`. (#20259) feat: add `IsStarNormal (↑x⁻¹ : R)` instance for `x : Rˣ` (#20091) fix: Stop cancelling builds of master (#20435) chore: update Mathlib dependencies 2025-01-05 (#20485) feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas (#18933) chore: bump toolchain to v4.16.0-rc1, and merge bump/v4.16.0 (#20464) chore: bot validates lean-toolchain on bump/v4.X.0 branches (#20478) feat: shorthand lemmas for the L1 norm (#20383) chore: remove unnecessary adaptation notes (#20467) chore(Algebra/Category/MonCat/Colimits): remove smallness condition (#20473) chore(SetTheory/Ordinal/Arithmetic): `IsLeftCancelAdd Ordinal` (#19888) feat(Algebra): more on `OrthogonalIdempotents` (#18195) feat(Radical): `(radical a).natDegree ≤ a.natDegree` (#20468) feat(Polynomial): `(a^n)' = 0` iff `a' = 0` when `n` doesn't divide the characteristic (#20190) feat(Algebra/Lie): add Lie's theorem (#13480) chore(RingTheory/Generators): make algebra instance a def (#14265) ...

YaelDillies added the t-data Data (lists, quotients, numbers, etc) label Dec 10, 2024

YaelDillies mentioned this pull request Dec 10, 2024

[Merged by Bors] - chore: don't import algebra in Data.Multiset.Basic #19775

Closed

3 tasks

Vierkantor added the awaiting-author A reviewer has asked the author a question or requested changes label Dec 11, 2024

Timeroot closed this Dec 12, 2024

Timeroot reopened this Dec 12, 2024

YaelDillies force-pushed the multiset_cleanup branch from c9ae1c3 to 3415b32 Compare December 18, 2024 18:02

mathlib4-dependent-issues-bot added blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) labels Dec 18, 2024

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 20, 2024

YaelDillies force-pushed the multiset_cleanup branch from 3415b32 to 2bd5031 Compare December 20, 2024 10:14

YaelDillies changed the title ~~chore(Data/Multiset/Basic): move the sub section lower~~ chore(Data/Multiset/Basic): move the sub, union, inter sections lower Dec 20, 2024

leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 20, 2024

YaelDillies removed the awaiting-author A reviewer has asked the author a question or requested changes label Dec 21, 2024

YaelDillies requested a review from Vierkantor December 21, 2024 10:18

Vierkantor reviewed Jan 6, 2025

View reviewed changes

Vierkantor added the awaiting-author A reviewer has asked the author a question or requested changes label Jan 6, 2025

YaelDillies added 2 commits January 6, 2025 11:31

chore(Data/Multiset/Basic): move the sub section lower

32ae525

and other cleanups that will be used to stop importing algebra here

fix indentation

df14c3c

YaelDillies force-pushed the multiset_cleanup branch from 2bd5031 to df14c3c Compare January 6, 2025 11:48

YaelDillies removed the awaiting-author A reviewer has asked the author a question or requested changes label Jan 6, 2025

leanprover-community-mathlib4-bot added the delegated label Jan 6, 2025

YaelDillies added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Jan 6, 2025

leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Jan 6, 2025

mathlib-bors bot changed the title ~~chore(Data/Multiset/Basic): move the sub, union, inter sections lower~~ [Merged by Bors] - chore(Data/Multiset/Basic): move the sub, union, inter sections lower Jan 6, 2025

mathlib-bors bot closed this Jan 6, 2025

mathlib-bors bot deleted the multiset_cleanup branch January 6, 2025 13:13

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore(Data/Multiset/Basic): move the `sub`, `union`, `inter` sections lower #19863

[Merged by Bors] - chore(Data/Multiset/Basic): move the `sub`, `union`, `inter` sections lower #19863

YaelDillies commented Dec 10, 2024 •

edited

Loading

github-actions bot commented Dec 10, 2024 •

edited

Loading

Import changes for modified files

Declarations diff

b-mehta commented Dec 10, 2024

Timeroot commented Dec 12, 2024

mathlib4-dependent-issues-bot commented Dec 20, 2024

Vierkantor left a comment

Vierkantor Jan 6, 2025

YaelDillies commented Jan 6, 2025

Vierkantor commented Jan 6, 2025

mathlib-bors bot commented Jan 6, 2025

leanprover-community-mathlib4-bot commented Jan 6, 2025

mathlib-bors bot commented Jan 6, 2025

[Merged by Bors] - chore(Data/Multiset/Basic): move the sub, union, inter sections lower #19863

[Merged by Bors] - chore(Data/Multiset/Basic): move the sub, union, inter sections lower #19863

Conversation

YaelDillies commented Dec 10, 2024 • edited Loading

github-actions bot commented Dec 10, 2024 • edited Loading

PR summary df14c3cf54

Import changes for modified files

Declarations diff

b-mehta commented Dec 10, 2024

Timeroot commented Dec 12, 2024

mathlib4-dependent-issues-bot commented Dec 20, 2024

Vierkantor left a comment

Choose a reason for hiding this comment

Vierkantor Jan 6, 2025

Choose a reason for hiding this comment

YaelDillies commented Jan 6, 2025

Vierkantor commented Jan 6, 2025

mathlib-bors bot commented Jan 6, 2025

leanprover-community-mathlib4-bot commented Jan 6, 2025

mathlib-bors bot commented Jan 6, 2025

[Merged by Bors] - chore(Data/Multiset/Basic): move the `sub`, `union`, `inter` sections lower #19863

[Merged by Bors] - chore(Data/Multiset/Basic): move the `sub`, `union`, `inter` sections lower #19863

YaelDillies commented Dec 10, 2024 •

edited

Loading

github-actions bot commented Dec 10, 2024 •

edited

Loading