feat(Order): constructors for DistribLattice and IsModularLattice

[alreadydone]

Add three constructors for DistribLattice and one for IsModularLattice.

Co-authored-by: Aaron Liu @plp127

---

[github-actions]

PR summary 1df8bea232

Import changes exceeding 2%

%	File
+2.78%	Mathlib.Order.ModularLattice

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Order.ModularLattice	395	406	+11 (+2.78%)

Import changes for all files

Files	Import difference
392 files Mathlib.Algebra.Algebra.Epi Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting Mathlib.Algebra.Category.ModuleCat.Ext.HasExt Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension Mathlib.Algebra.Category.ModuleCat.Topology.Basic Mathlib.Algebra.Category.ModuleCat.Topology.Homology Mathlib.Algebra.Category.Ring.Epi Mathlib.Algebra.CharP.CharAndCard Mathlib.Algebra.CharP.Frobenius Mathlib.Algebra.CharP.IntermediateField Mathlib.Algebra.CharP.Lemmas Mathlib.Algebra.CharP.Reduced Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries Mathlib.Algebra.FreeAlgebra.Cardinality Mathlib.Algebra.Group.ForwardDiff Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.Algebra.Homology.DerivedCategory.Ext.MapBijective Mathlib.Algebra.Homology.DerivedCategory.KInjective Mathlib.Algebra.Homology.DerivedCategory.KProjective Mathlib.Algebra.Homology.DerivedCategory.Plus Mathlib.Algebra.Homology.DerivedCategory.RightDerivedFunctorPlus Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle Mathlib.Algebra.Module.ZMod Mathlib.Algebra.MvPolynomial.Cardinal Mathlib.Algebra.MvPolynomial.Coeff Mathlib.Algebra.MvPolynomial.Derivation Mathlib.Algebra.MvPolynomial.Equiv Mathlib.Algebra.MvPolynomial.Funext Mathlib.Algebra.MvPolynomial.PDeriv Mathlib.Algebra.MvPolynomial.Polynomial Mathlib.Algebra.MvPolynomial.SchwartzZippel Mathlib.Algebra.Order.Antidiag.Nat Mathlib.Algebra.Order.CauSeq.BigOperators Mathlib.Algebra.Order.Module.HahnEmbedding Mathlib.Algebra.Order.Ring.IsNonarchimedean Mathlib.Algebra.Polynomial.AlgebraMap Mathlib.Algebra.Polynomial.BigOperators Mathlib.Algebra.Polynomial.CancelLeads Mathlib.Algebra.Polynomial.CoeffList Mathlib.Algebra.Polynomial.CoeffMem Mathlib.Algebra.Polynomial.Coeff Mathlib.Algebra.Polynomial.Degree.Domain Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree Mathlib.Algebra.Polynomial.Degree.Lemmas Mathlib.Algebra.Polynomial.Degree.Operations Mathlib.Algebra.Polynomial.Degree.SmallDegree Mathlib.Algebra.Polynomial.Degree.Support Mathlib.Algebra.Polynomial.Degree.TrailingDegree Mathlib.Algebra.Polynomial.Degree.Units Mathlib.Algebra.Polynomial.DenomsClearable Mathlib.Algebra.Polynomial.Derivative Mathlib.Algebra.Polynomial.Div Mathlib.Algebra.Polynomial.EraseLead Mathlib.Algebra.Polynomial.Eval.Coeff Mathlib.Algebra.Polynomial.Eval.Degree Mathlib.Algebra.Polynomial.Eval.Irreducible Mathlib.Algebra.Polynomial.Eval.SMul Mathlib.Algebra.Polynomial.Eval.Subring Mathlib.Algebra.Polynomial.GroupRingAction Mathlib.Algebra.Polynomial.HasseDeriv Mathlib.Algebra.Polynomial.Identities Mathlib.Algebra.Polynomial.Inductions Mathlib.Algebra.Polynomial.Lifts Mathlib.Algebra.Polynomial.Mirror Mathlib.Algebra.Polynomial.Monic Mathlib.Algebra.Polynomial.OfFn Mathlib.Algebra.Polynomial.PartialFractions Mathlib.Algebra.Polynomial.Reverse Mathlib.Algebra.Polynomial.RingDivision Mathlib.Algebra.Polynomial.Roots Mathlib.Algebra.Polynomial.RuleOfSigns Mathlib.Algebra.Polynomial.Smeval Mathlib.Algebra.Polynomial.SumIteratedDerivative Mathlib.Algebra.Polynomial.Taylor Mathlib.Algebra.Polynomial.UnitTrinomial Mathlib.Algebra.Ring.Divisibility.Lemmas Mathlib.Algebra.Ring.IsFormallyReal Mathlib.Algebra.Ring.Subring.IntPolynomial Mathlib.Algebra.Squarefree.Basic Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.AlgebraicTopology.DoldKan.Equivalence Mathlib.AlgebraicTopology.DoldKan.GammaCompN Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate Mathlib.Analysis.Asymptotics.Defs Mathlib.Analysis.CStarAlgebra.Module.Synonym Mathlib.Analysis.Calculus.TangentCone.Basic Mathlib.Analysis.Calculus.TangentCone.Defs Mathlib.Analysis.Calculus.TangentCone.Pi Mathlib.Analysis.Calculus.TangentCone.Prod Mathlib.Analysis.Convex.Cone.Basic Mathlib.Analysis.Convex.Cone.Extension Mathlib.Analysis.Convex.ContinuousLinearEquiv Mathlib.Analysis.Convex.Exposed Mathlib.Analysis.Convex.Extrema Mathlib.Analysis.Convex.NNReal Mathlib.Analysis.Convex.Slope Mathlib.Analysis.Convex.Strict Mathlib.Analysis.Fourier.Notation Mathlib.Analysis.Normed.Field.Basic Mathlib.Analysis.Normed.Group.Basic Mathlib.Analysis.Normed.Group.Constructions Mathlib.Analysis.Normed.Group.Defs Mathlib.Analysis.Normed.Group.Indicator Mathlib.Analysis.Normed.Group.Real Mathlib.Analysis.Normed.Group.Subgroup Mathlib.Analysis.Normed.Group.Submodule Mathlib.Analysis.Normed.Lp.WithLp Mathlib.Analysis.Normed.Module.MStructure Mathlib.Analysis.Normed.Order.Basic Mathlib.Analysis.Normed.Order.Hom.Basic Mathlib.Analysis.Normed.Order.Hom.Ultra Mathlib.Analysis.Normed.Ring.Basic Mathlib.Analysis.Normed.Ring.Finite Mathlib.Analysis.Oscillation Mathlib.Analysis.Polynomial.CauchyBound Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt Mathlib.CategoryTheory.Abelian.Injective.Dimension Mathlib.CategoryTheory.Abelian.Injective.Ext Mathlib.CategoryTheory.Abelian.Projective.Dimension Mathlib.CategoryTheory.Abelian.Projective.Ext Mathlib.CategoryTheory.Galois.Equivalence Mathlib.CategoryTheory.Galois.EssSurj Mathlib.CategoryTheory.Galois.IsFundamentalgroup Mathlib.CategoryTheory.Galois.Topology Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris Mathlib.Combinatorics.Enumerative.Bell Mathlib.Combinatorics.Enumerative.Partition.GenFun Mathlib.Combinatorics.SimpleGraph.FiveWheelLike Mathlib.Combinatorics.SimpleGraph.Triangle.Counting Mathlib.Data.Nat.Choose.Factorization Mathlib.Data.Nat.Choose.Multinomial Mathlib.Data.Nat.Choose.Sum Mathlib.Data.Nat.Choose.Vandermonde Mathlib.Data.Nat.Digits.Div Mathlib.Data.Nat.Digits.Lemmas Mathlib.Data.Nat.Multiplicity Mathlib.Data.Nat.Squarefree Mathlib.FieldTheory.IntermediateField.Adjoin.Defs Mathlib.FieldTheory.IntermediateField.Basic Mathlib.FieldTheory.IsRealClosed.Basic Mathlib.GroupTheory.ArchimedeanDensely Mathlib.GroupTheory.Coxeter.Inversion Mathlib.GroupTheory.Coxeter.Length Mathlib.GroupTheory.Descent Mathlib.GroupTheory.DivisibleHull Mathlib.GroupTheory.FinitelyPresentedGroup Mathlib.GroupTheory.Focal Mathlib.GroupTheory.Frattini Mathlib.GroupTheory.IsPerfect Mathlib.GroupTheory.Nilpotent Mathlib.GroupTheory.RegularWreathProduct Mathlib.GroupTheory.Schreier Mathlib.GroupTheory.SchurZassenhaus Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour Mathlib.GroupTheory.SpecificGroups.Alternating.Simple Mathlib.GroupTheory.Sylow Mathlib.GroupTheory.Transfer Mathlib.InformationTheory.Hamming Mathlib.LinearAlgebra.ConvexSpace.AffineSpace Mathlib.LinearAlgebra.Matrix.Adjugate Mathlib.LinearAlgebra.Matrix.FixedDetMatrices Mathlib.LinearAlgebra.Matrix.Nondegenerate Mathlib.LinearAlgebra.Matrix.Polynomial Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup Mathlib.MeasureTheory.OuterMeasure.Defs Mathlib.ModelTheory.Algebra.Field.CharP Mathlib.ModelTheory.Algebra.Ring.FreeCommRing Mathlib.ModelTheory.Arithmetic.Presburger.Definability Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic Mathlib.ModelTheory.Fraisse Mathlib.ModelTheory.Order Mathlib.NumberTheory.AlmostPrime Mathlib.NumberTheory.ArithmeticFunction.Defs Mathlib.NumberTheory.ArithmeticFunction.LFunction Mathlib.NumberTheory.ArithmeticFunction.Liouville Mathlib.NumberTheory.ArithmeticFunction.Misc Mathlib.NumberTheory.ArithmeticFunction.Moebius Mathlib.NumberTheory.ArithmeticFunction.Zeta Mathlib.NumberTheory.DirichletCharacter.Basic Mathlib.NumberTheory.LegendreSymbol.ZModChar Mathlib.NumberTheory.LucasPrimality Mathlib.NumberTheory.MaricaSchoenheim Mathlib.NumberTheory.MulChar.Basic Mathlib.NumberTheory.Multiplicity Mathlib.NumberTheory.Padics.Measure.Basic Mathlib.NumberTheory.Padics.PadicNorm Mathlib.NumberTheory.Padics.PadicVal.Basic Mathlib.NumberTheory.Primorial Mathlib.NumberTheory.SelbergSieve Mathlib.NumberTheory.SmoothNumbers Mathlib.RingTheory.Adjoin.Polynomial.Basic Mathlib.RingTheory.Adjoin.Polynomial Mathlib.RingTheory.Adjoin.Singleton Mathlib.RingTheory.Algebraic.Cardinality Mathlib.RingTheory.Algebraic.Defs Mathlib.RingTheory.Algebraic.LinearIndependent Mathlib.RingTheory.Algebraic.Pi Mathlib.RingTheory.Binomial Mathlib.RingTheory.Derivation.Basic Mathlib.RingTheory.Derivation.DifferentialRing Mathlib.RingTheory.FormalGroup.Basic Mathlib.RingTheory.FreeCommRing Mathlib.RingTheory.HahnSeries.Binomial Mathlib.RingTheory.HahnSeries.HEval Mathlib.RingTheory.HahnSeries.Lex Mathlib.RingTheory.HahnSeries.PowerSeries Mathlib.RingTheory.Ideal.Basic Mathlib.RingTheory.Ideal.Quotient.Basic Mathlib.RingTheory.IntegralDomain Mathlib.RingTheory.MatrixPolynomialAlgebra Mathlib.RingTheory.MvPolynomial.FreeCommRing Mathlib.RingTheory.MvPowerSeries.Evaluation Mathlib.RingTheory.MvPowerSeries.GaussNorm Mathlib.RingTheory.MvPowerSeries.LinearTopology Mathlib.RingTheory.MvPowerSeries.PiTopology Mathlib.RingTheory.MvPowerSeries.Rename Mathlib.RingTheory.MvPowerSeries.Substitution Mathlib.RingTheory.Nilpotent.Basic Mathlib.RingTheory.Nilpotent.Exp Mathlib.RingTheory.Polynomial.Bernstein Mathlib.RingTheory.Polynomial.GaussNorm Mathlib.RingTheory.Polynomial.Hermite.Basic Mathlib.RingTheory.Polynomial.HilbertPoly Mathlib.RingTheory.Polynomial.Opposites Mathlib.RingTheory.Polynomial.Pochhammer Mathlib.RingTheory.Polynomial.ShiftedLegendre Mathlib.RingTheory.Polynomial.Subring Mathlib.RingTheory.Polynomial.Tower Mathlib.RingTheory.Polynomial.Wronskian Mathlib.RingTheory.PolynomialAlgebra Mathlib.RingTheory.PowerSeries.Basic Mathlib.RingTheory.PowerSeries.Binomial Mathlib.RingTheory.PowerSeries.Catalan Mathlib.RingTheory.PowerSeries.Evaluation Mathlib.RingTheory.PowerSeries.GaussNorm Mathlib.RingTheory.PowerSeries.Order Mathlib.RingTheory.PowerSeries.PiTopology Mathlib.RingTheory.PowerSeries.Schroder Mathlib.RingTheory.PowerSeries.Substitution Mathlib.RingTheory.PowerSeries.Trunc Mathlib.RingTheory.PowerSeries.WellKnown Mathlib.RingTheory.Radical.Basic Mathlib.RingTheory.RootsOfUnity.Basic Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots Mathlib.RingTheory.TensorProduct.Finite Mathlib.RingTheory.TensorProduct.MvPolynomial Mathlib.RingTheory.UniqueFactorizationDomain.Moebius Mathlib.SetTheory.Cardinal.Free Mathlib.Tactic.ComputeDegree Mathlib.Tactic.Polynomial.Basic Mathlib.Topology.Algebra.AffineSubspace Mathlib.Topology.Algebra.Algebra.Equiv Mathlib.Topology.Algebra.Algebra Mathlib.Topology.Algebra.ClopenNhdofOne Mathlib.Topology.Algebra.ContinuousAffineEquiv Mathlib.Topology.Algebra.ContinuousAffineMap Mathlib.Topology.Algebra.Equicontinuity Mathlib.Topology.Algebra.Field Mathlib.Topology.Algebra.FilterBasis Mathlib.Topology.Algebra.Group.Basic Mathlib.Topology.Algebra.Group.ClosedSubgroup Mathlib.Topology.Algebra.Group.CompactOpen Mathlib.Topology.Algebra.Group.Compact Mathlib.Topology.Algebra.Group.Extension Mathlib.Topology.Algebra.Group.GroupTopology Mathlib.Topology.Algebra.Group.OpenMapping Mathlib.Topology.Algebra.Group.Pointwise Mathlib.Topology.Algebra.Group.Quotient Mathlib.Topology.Algebra.Group.SubmonoidClosure Mathlib.Topology.Algebra.Group.TopologicalAbelianization Mathlib.Topology.Algebra.GroupCompletion Mathlib.Topology.Algebra.InfiniteSum.Constructions Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion Mathlib.Topology.Algebra.InfiniteSum.Group Mathlib.Topology.Algebra.InfiniteSum.Module Mathlib.Topology.Algebra.InfiniteSum.NatInt Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean Mathlib.Topology.Algebra.InfiniteSum.Order Mathlib.Topology.Algebra.InfiniteSum.Ring Mathlib.Topology.Algebra.InfiniteSum.UniformOn Mathlib.Topology.Algebra.IntermediateField Mathlib.Topology.Algebra.IsUniformGroup.Basic Mathlib.Topology.Algebra.IsUniformGroup.Constructions Mathlib.Topology.Algebra.IsUniformGroup.Defs Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup Mathlib.Topology.Algebra.IsUniformGroup.Order Mathlib.Topology.Algebra.LinearMapCompletion Mathlib.Topology.Algebra.LinearTopology Mathlib.Topology.Algebra.Localization Mathlib.Topology.Algebra.Module.Alternating.Basic Mathlib.Topology.Algebra.Module.Basic Mathlib.Topology.Algebra.Module.ClosedSubmodule Mathlib.Topology.Algebra.Module.Compact Mathlib.Topology.Algebra.Module.Complement Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict Mathlib.Topology.Algebra.Module.Equiv Mathlib.Topology.Algebra.Module.IsWeak Mathlib.Topology.Algebra.Module.LinearMapPiProd Mathlib.Topology.Algebra.Module.LinearMap Mathlib.Topology.Algebra.Module.LinearPMap Mathlib.Topology.Algebra.Module.ModuleTopology Mathlib.Topology.Algebra.Module.Multilinear.Basic Mathlib.Topology.Algebra.Module.PerfectPairing Mathlib.Topology.Algebra.Module.Spaces.WeakBilin Mathlib.Topology.Algebra.Module.Spaces.WeakDual Mathlib.Topology.Algebra.Module.Star Mathlib.Topology.Algebra.Module.WeakDual Mathlib.Topology.Algebra.MvPolynomial Mathlib.Topology.Algebra.NonUnitalAlgebra Mathlib.Topology.Algebra.NonUnitalStarAlgebra Mathlib.Topology.Algebra.Nonarchimedean.Bases Mathlib.Topology.Algebra.Nonarchimedean.Basic Mathlib.Topology.Algebra.Nonarchimedean.Completion Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected Mathlib.Topology.Algebra.OpenSubgroup Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete Mathlib.Topology.Algebra.Order.Archimedean Mathlib.Topology.Algebra.Order.Field Mathlib.Topology.Algebra.Order.Floor Mathlib.Topology.Algebra.Order.UpperLower Mathlib.Topology.Algebra.ProperAction.AddTorsor Mathlib.Topology.Algebra.ProperAction.Basic Mathlib.Topology.Algebra.ProperAction.Torsor Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace Mathlib.Topology.Algebra.Ring.Basic Mathlib.Topology.Algebra.Ring.Ideal Mathlib.Topology.Algebra.SeparationQuotient.Basic Mathlib.Topology.Algebra.SeparationQuotient.FiniteDimensional Mathlib.Topology.Algebra.SeparationQuotient.Hom Mathlib.Topology.Algebra.SeparationQuotient.Section Mathlib.Topology.Algebra.Star.Real Mathlib.Topology.Algebra.StarSubalgebra Mathlib.Topology.Algebra.TopologicallyNilpotent Mathlib.Topology.Algebra.UniformConvergence Mathlib.Topology.Algebra.UniformField Mathlib.Topology.Algebra.UniformFilterBasis Mathlib.Topology.Algebra.UniformMulAction Mathlib.Topology.Algebra.UniformRing Mathlib.Topology.Category.TopCommRingCat Mathlib.Topology.ContinuousMap.Algebra Mathlib.Topology.ContinuousMap.Lattice Mathlib.Topology.ContinuousMap.LocallyConstant Mathlib.Topology.ContinuousMap.Periodic Mathlib.Topology.ContinuousMap.Star Mathlib.Topology.Covering.Quotient Mathlib.Topology.EMetricSpace.Basic Mathlib.Topology.EMetricSpace.Diam Mathlib.Topology.EMetricSpace.Lipschitz Mathlib.Topology.EMetricSpace.Paracompact Mathlib.Topology.EMetricSpace.Pi Mathlib.Topology.Instances.ENat Mathlib.Topology.Instances.TrivSqZeroExt Mathlib.Topology.Maps.Strict.Group Mathlib.Topology.MetricSpace.Basic Mathlib.Topology.MetricSpace.CauSeqFilter Mathlib.Topology.MetricSpace.Cauchy Mathlib.Topology.MetricSpace.Equicontinuity Mathlib.Topology.MetricSpace.Infsep Mathlib.Topology.MetricSpace.ProperSpace Mathlib.Topology.MetricSpace.Pseudo.Basic Mathlib.Topology.MetricSpace.Pseudo.Lemmas Mathlib.Topology.MetricSpace.Pseudo.Pi Mathlib.Topology.MetricSpace.Pseudo.Real Mathlib.Topology.MetricSpace.TransferInstance Mathlib.Topology.MetricSpace.Ultra.Basic Mathlib.Topology.MetricSpace.Ultra.Pi Mathlib.Topology.MetricSpace.Ultra.TotallySeparated Mathlib.Topology.Metrizable.ContinuousMap Mathlib.Topology.Metrizable.Real Mathlib.Topology.Metrizable.Uniformity Mathlib.Topology.Order.Real Mathlib.Topology.UniformSpace.ProdApproximation Mathlib.Topology.UniformSpace.Real	8
1024 files Mathlib.Algebra.Algebra.Bilinear Mathlib.Algebra.Algebra.IsSimpleRing Mathlib.Algebra.Algebra.NonUnitalSubalgebra Mathlib.Algebra.Algebra.Operations Mathlib.Algebra.Algebra.RestrictScalars Mathlib.Algebra.Algebra.Subalgebra.Basic Mathlib.Algebra.Algebra.Subalgebra.Centralizer Mathlib.Algebra.Algebra.Subalgebra.Directed Mathlib.Algebra.Algebra.Subalgebra.Lattice Mathlib.Algebra.Algebra.Subalgebra.Matrix Mathlib.Algebra.Algebra.Subalgebra.MulOpposite Mathlib.Algebra.Algebra.Subalgebra.Order Mathlib.Algebra.Algebra.Subalgebra.Pi Mathlib.Algebra.Algebra.Subalgebra.Pointwise Mathlib.Algebra.Algebra.Subalgebra.Prod Mathlib.Algebra.Algebra.Subalgebra.Tower Mathlib.Algebra.Algebra.Subalgebra.Unitization Mathlib.Algebra.Algebra.Tower Mathlib.Algebra.Algebra.Unitization Mathlib.Algebra.Azumaya.Defs Mathlib.Algebra.Azumaya.Matrix Mathlib.Algebra.BigOperators.Module Mathlib.Algebra.Category.AlgCat.Basic Mathlib.Algebra.Category.AlgCat.FilteredColimits Mathlib.Algebra.Category.AlgCat.Limits Mathlib.Algebra.Category.AlgCat.Monoidal Mathlib.Algebra.Category.AlgCat.Symmetric Mathlib.Algebra.Category.AlgCat.TensorAlgebra Mathlib.Algebra.Category.BialgCat.Basic Mathlib.Algebra.Category.BialgCat.Monoidal Mathlib.Algebra.Category.CoalgCat.Basic Mathlib.Algebra.Category.CoalgCat.ComonEquivalence Mathlib.Algebra.Category.CoalgCat.Monoidal Mathlib.Algebra.Category.Grp.AB Mathlib.Algebra.Category.Grp.Abelian Mathlib.Algebra.Category.Grp.Images Mathlib.Algebra.Category.Grp.IsFinite Mathlib.Algebra.Category.Grp.Subobject Mathlib.Algebra.Category.HopfAlgCat.Basic Mathlib.Algebra.Category.HopfAlgCat.Monoidal Mathlib.Algebra.Category.ModuleCat.AB Mathlib.Algebra.Category.ModuleCat.Abelian Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.Algebra.Category.ModuleCat.Algebra Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.Algebra.Category.ModuleCat.ChangeOfRingsExact Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Colimits Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.Algebra.Category.ModuleCat.FilteredColimits Mathlib.Algebra.Category.ModuleCat.Images Mathlib.Algebra.Category.ModuleCat.Kernels Mathlib.Algebra.Category.ModuleCat.LeftResolution Mathlib.Algebra.Category.ModuleCat.Limits Mathlib.Algebra.Category.ModuleCat.Localization Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono Mathlib.Algebra.Category.ModuleCat.Presheaf.Free Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback Mathlib.Algebra.Category.ModuleCat.Presheaf.PushforwardZeroMonoidal Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.Algebra.Category.ModuleCat.Products Mathlib.Algebra.Category.ModuleCat.Projective Mathlib.Algebra.Category.ModuleCat.Pseudofunctor Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.Algebra.Category.ModuleCat.Stalk Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.Algebra.Category.ModuleCat.Tannaka Mathlib.Algebra.Category.Ring.Adjunctions Mathlib.Algebra.Central.Basic Mathlib.Algebra.Central.Defs Mathlib.Algebra.Central.End Mathlib.Algebra.Central.Matrix Mathlib.Algebra.CharP.Algebra Mathlib.Algebra.CharP.Subring Mathlib.Algebra.Colimit.Finiteness Mathlib.Algebra.Colimit.Module Mathlib.Algebra.Colimit.TensorProduct Mathlib.Algebra.DirectSum.Algebra Mathlib.Algebra.DirectSum.Decomposition Mathlib.Algebra.DirectSum.Finsupp Mathlib.Algebra.DirectSum.Internal Mathlib.Algebra.DirectSum.Module Mathlib.Algebra.DualNumber Mathlib.Algebra.Exact.Basic Mathlib.Algebra.Exact Mathlib.Algebra.Field.GeomSum Mathlib.Algebra.Field.Subfield.Basic Mathlib.Algebra.FiveLemma Mathlib.Algebra.FreeAlgebra Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra Mathlib.Algebra.Group.UniqueProds.VectorSpace Mathlib.Algebra.Homology.AlternatingConst Mathlib.Algebra.Homology.ConcreteCategory Mathlib.Algebra.Homology.EulerCharacteristic Mathlib.Algebra.Homology.ShortComplex.Ab Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.Algebra.Module.Bimodule Mathlib.Algebra.Module.GradedModule Mathlib.Algebra.Module.LocalizedModule.AtPrime Mathlib.Algebra.Module.LocalizedModule.Away Mathlib.Algebra.Module.LocalizedModule.Basic Mathlib.Algebra.Module.LocalizedModule.Exact Mathlib.Algebra.Module.LocalizedModule.Int Mathlib.Algebra.Module.LocalizedModule.IsLocalization Mathlib.Algebra.Module.LocalizedModule.Submodule Mathlib.Algebra.Module.Presentation.Basic Mathlib.Algebra.Module.Presentation.Cokernel Mathlib.Algebra.Module.Presentation.DirectSum Mathlib.Algebra.Module.Presentation.Free Mathlib.Algebra.Module.Presentation.RestrictScalars Mathlib.Algebra.Module.Presentation.Tautological Mathlib.Algebra.Module.Presentation.Tensor Mathlib.Algebra.Module.Projective Mathlib.Algebra.Module.SnakeLemma Mathlib.Algebra.Module.Submodule.Bilinear Mathlib.Algebra.MonoidAlgebra.Basic Mathlib.Algebra.MonoidAlgebra.Degree Mathlib.Algebra.MonoidAlgebra.Grading Mathlib.Algebra.MonoidAlgebra.Ideal Mathlib.Algebra.MonoidAlgebra.Module Mathlib.Algebra.MonoidAlgebra.Support Mathlib.Algebra.MonoidAlgebra.ToDirectSum Mathlib.Algebra.MvPolynomial.Basic Mathlib.Algebra.MvPolynomial.Comap Mathlib.Algebra.MvPolynomial.CommRing Mathlib.Algebra.MvPolynomial.Counit Mathlib.Algebra.MvPolynomial.Degrees Mathlib.Algebra.MvPolynomial.Division Mathlib.Algebra.MvPolynomial.Eval Mathlib.Algebra.MvPolynomial.Invertible Mathlib.Algebra.MvPolynomial.Monad Mathlib.Algebra.MvPolynomial.Rename Mathlib.Algebra.MvPolynomial.Supported Mathlib.Algebra.MvPolynomial.Variables Mathlib.Algebra.Order.Field.GeomSum Mathlib.Algebra.Order.Group.Cyclic Mathlib.Algebra.Order.Ring.GeomSum Mathlib.Algebra.Polynomial.Basic Mathlib.Algebra.Polynomial.Basis Mathlib.Algebra.Polynomial.Cardinal Mathlib.Algebra.Polynomial.Degree.Definitions Mathlib.Algebra.Polynomial.Degree.Defs Mathlib.Algebra.Polynomial.Degree.Monomial Mathlib.Algebra.Polynomial.Eval.Algebra Mathlib.Algebra.Polynomial.Eval.Defs Mathlib.Algebra.Polynomial.Monomial Mathlib.Algebra.Ring.GeomSum Mathlib.Algebra.RingQuot Mathlib.Algebra.SkewMonoidAlgebra.Basic Mathlib.Algebra.SkewMonoidAlgebra.Lift Mathlib.Algebra.SkewMonoidAlgebra.Single Mathlib.Algebra.SkewMonoidAlgebra.Support Mathlib.Algebra.SkewPolynomial.Basic Mathlib.Algebra.Star.Free Mathlib.Algebra.Star.Module Mathlib.Algebra.Star.NonUnitalSubalgebra Mathlib.Algebra.Star.RingQuot Mathlib.Algebra.Star.Subalgebra Mathlib.Algebra.Star.TensorProduct Mathlib.Algebra.TrivSqZeroExt.Basic Mathlib.Algebra.TrivSqZeroExt Mathlib.Algebra.Vertex.HVertexOperator Mathlib.Algebra.Vertex.VertexOperator Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.AlgebraicTopology.CechNerve Mathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.AlgebraicTopology.DoldKan.Faces Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.AlgebraicTopology.MooreComplex Mathlib.AlgebraicTopology.Quasicategory.Basic Mathlib.AlgebraicTopology.Quasicategory.InnerFibration Mathlib.AlgebraicTopology.Quasicategory.Nerve Mathlib.AlgebraicTopology.Quasicategory.StrictBicategory Mathlib.AlgebraicTopology.Quasicategory.StrictSegal Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal Mathlib.AlgebraicTopology.SimplexCategory.Basic Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty Mathlib.AlgebraicTopology.SimplexCategory.Rev Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne Mathlib.AlgebraicTopology.SimplexCategory.Truncated Mathlib.AlgebraicTopology.SimplicialCategory.Basic Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject Mathlib.AlgebraicTopology.SimplicialComplex.Basic Mathlib.AlgebraicTopology.SimplicialNerve Mathlib.AlgebraicTopology.SimplicialObject.Basic Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter Mathlib.AlgebraicTopology.SimplicialObject.Homotopy Mathlib.AlgebraicTopology.SimplicialObject.II Mathlib.AlgebraicTopology.SimplicialObject.Op Mathlib.AlgebraicTopology.SimplicialObject.Split Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd Mathlib.AlgebraicTopology.SimplicialSet.Basic Mathlib.AlgebraicTopology.SimplicialSet.Boundary Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated Mathlib.AlgebraicTopology.SimplicialSet.CompStruct Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal Mathlib.AlgebraicTopology.SimplicialSet.Degenerate Mathlib.AlgebraicTopology.SimplicialSet.Dimension Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd Mathlib.AlgebraicTopology.SimplicialSet.Finite Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat Mathlib.AlgebraicTopology.SimplicialSet.Homotopy Mathlib.AlgebraicTopology.SimplicialSet.HornColimits Mathlib.AlgebraicTopology.SimplicialSet.Horn Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct Mathlib.AlgebraicTopology.SimplicialSet.KanComplex Mathlib.AlgebraicTopology.SimplicialSet.Monoidal Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction Mathlib.AlgebraicTopology.SimplicialSet.NerveCodiscrete Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate Mathlib.AlgebraicTopology.SimplicialSet.Nerve Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices Mathlib.AlgebraicTopology.SimplicialSet.Nonempty Mathlib.AlgebraicTopology.SimplicialSet.NonsingularColimit Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular Mathlib.AlgebraicTopology.SimplicialSet.Op Mathlib.AlgebraicTopology.SimplicialSet.Path Mathlib.AlgebraicTopology.SimplicialSet.PiZero Mathlib.AlgebraicTopology.SimplicialSet.Presentable Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct Mathlib.AlgebraicTopology.SimplicialSet.RegularEpi Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism Mathlib.AlgebraicTopology.SimplicialSet.Simplices Mathlib.AlgebraicTopology.SimplicialSet.Skeleton Mathlib.AlgebraicTopology.SimplicialSet.Splitting Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexEvaluation Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexOp Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex Mathlib.AlgebraicTopology.SimplicialSet.Subdivision Mathlib.Analysis.Convex.Basic Mathlib.Analysis.Convex.Caratheodory Mathlib.Analysis.Convex.Combination Mathlib.Analysis.Convex.Cone.Closure Mathlib.Analysis.Convex.Extreme Mathlib.Analysis.Convex.FunctionTopology Mathlib.Analysis.Convex.Function Mathlib.Analysis.Convex.Hull Mathlib.Analysis.Convex.Independent Mathlib.Analysis.Convex.Jensen Mathlib.Analysis.Convex.Join Mathlib.Analysis.Convex.Mul Mathlib.Analysis.Convex.Piecewise Mathlib.Analysis.Convex.Segment Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion Mathlib.Analysis.Convex.SimplicialComplex.Basic Mathlib.Analysis.Convex.Star Mathlib.Analysis.Convex.StoneSeparation Mathlib.CategoryTheory.Abelian.Ext Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite Mathlib.CategoryTheory.Abelian.Injective.Basic Mathlib.CategoryTheory.Abelian.Projective.Basic Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Abelian.Yoneda Mathlib.CategoryTheory.Action.Continuous Mathlib.CategoryTheory.Adhesive.Basic Mathlib.CategoryTheory.Adhesive.Over Mathlib.CategoryTheory.Adhesive.Subobject Mathlib.CategoryTheory.Adhesive Mathlib.CategoryTheory.Category.Cat.Colimit Mathlib.CategoryTheory.CofilteredSystem Mathlib.CategoryTheory.EffectiveEpi.Extensive Mathlib.CategoryTheory.Extensive Mathlib.CategoryTheory.Galois.Action Mathlib.CategoryTheory.Galois.Full Mathlib.CategoryTheory.Galois.Prorepresentability Mathlib.CategoryTheory.Idempotents.SimplicialObject Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy Mathlib.CategoryTheory.Monoidal.Internal.Module Mathlib.CategoryTheory.MorphismProperty.CommaSites Mathlib.CategoryTheory.Noetherian Mathlib.CategoryTheory.Preadditive.Yoneda.Injective Mathlib.CategoryTheory.Preadditive.Yoneda.Limits Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.CategoryTheory.RegularCategory.Basic Mathlib.CategoryTheory.Simple Mathlib.CategoryTheory.Sites.Abelian Mathlib.CategoryTheory.Sites.Coherent.Basic Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology Mathlib.CategoryTheory.Sites.Coherent.Comparison Mathlib.CategoryTheory.Sites.Coherent.Equivalence Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves Mathlib.CategoryTheory.Sites.Coherent.RegularTopology Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit Mathlib.CategoryTheory.Sites.Coherent.SheafComparison Mathlib.CategoryTheory.Sites.ConstantSheaf Mathlib.CategoryTheory.Sites.CoversTop.Over Mathlib.CategoryTheory.Sites.DenseSubsite.Basic Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime Mathlib.CategoryTheory.Sites.Descent.DescentData Mathlib.CategoryTheory.Sites.Descent.IsPrestack Mathlib.CategoryTheory.Sites.Descent.IsStack Mathlib.CategoryTheory.Sites.Descent.Precoverage Mathlib.CategoryTheory.Sites.EpiMono Mathlib.CategoryTheory.Sites.Equivalence Mathlib.CategoryTheory.Sites.GlobalSections Mathlib.CategoryTheory.Sites.LeftExact Mathlib.CategoryTheory.Sites.LocalProperties Mathlib.CategoryTheory.Sites.LocalSite Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.CategoryTheory.Sites.Monoidal Mathlib.CategoryTheory.Sites.Over Mathlib.CategoryTheory.Sites.Point.Basic Mathlib.CategoryTheory.Sites.Point.Category Mathlib.CategoryTheory.Sites.Point.Comap Mathlib.CategoryTheory.Sites.Point.Conservative Mathlib.CategoryTheory.Sites.Point.IsMonoidalW Mathlib.CategoryTheory.Sites.Point.Map Mathlib.CategoryTheory.Sites.Point.Monoidal Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered Mathlib.CategoryTheory.Sites.Point.Over Mathlib.CategoryTheory.Sites.Point.Presheaf Mathlib.CategoryTheory.Sites.Point.Skyscraper Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver Mathlib.CategoryTheory.Sites.Pullback Mathlib.CategoryTheory.Sites.RegularEpi Mathlib.CategoryTheory.Sites.SheafCohomology.Cech Mathlib.CategoryTheory.Sites.SheafHom Mathlib.CategoryTheory.Sites.Spaces Mathlib.CategoryTheory.Sites.SubcanonicalOver Mathlib.CategoryTheory.Subobject.ArtinianObject Mathlib.CategoryTheory.Topos.Sheaf Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.Combinatorics.Colex Mathlib.Combinatorics.Enumerative.IncidenceAlgebra Mathlib.Combinatorics.Enumerative.Schroder Mathlib.Combinatorics.Hall.Basic Mathlib.Combinatorics.Hindman Mathlib.Combinatorics.Optimization.ValuedCSP Mathlib.Combinatorics.SetFamily.AhlswedeZhang Mathlib.Combinatorics.SetFamily.Compression.UV Mathlib.Combinatorics.SetFamily.FourFunctions Mathlib.Combinatorics.SetFamily.KruskalKatona Mathlib.Combinatorics.SetFamily.LYM Mathlib.Combinatorics.SetFamily.Shadow Mathlib.Combinatorics.SimpleGraph.Acyclic Mathlib.Combinatorics.SimpleGraph.AdjMatrix Mathlib.Combinatorics.SimpleGraph.Bipartite Mathlib.Combinatorics.SimpleGraph.Circulant Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex Mathlib.Combinatorics.SimpleGraph.Coloring Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite Mathlib.Combinatorics.SimpleGraph.ConcreteColorings Mathlib.Combinatorics.SimpleGraph.CycleGraph Mathlib.Combinatorics.SimpleGraph.Density Mathlib.Combinatorics.SimpleGraph.Ends.Defs Mathlib.Combinatorics.SimpleGraph.Ends.Properties Mathlib.Combinatorics.SimpleGraph.Extremal.Turan Mathlib.Combinatorics.SimpleGraph.Finsubgraph Mathlib.Combinatorics.SimpleGraph.Girth Mathlib.Combinatorics.SimpleGraph.Hall Mathlib.Combinatorics.SimpleGraph.Hasse Mathlib.Combinatorics.SimpleGraph.Partition Mathlib.Combinatorics.SimpleGraph.Prod Mathlib.Combinatorics.SimpleGraph.Regularity.Energy Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform Mathlib.Combinatorics.SimpleGraph.Star Mathlib.Combinatorics.SimpleGraph.StronglyRegular Mathlib.Combinatorics.SimpleGraph.Sum Mathlib.Computability.TMComputable Mathlib.Computability.TuringMachine.Computable Mathlib.Data.Finset.Grade Mathlib.Data.Finset.Interval Mathlib.Data.Matrix.Basic Mathlib.Data.Matrix.Basis Mathlib.Data.Matrix.Bilinear Mathlib.Data.Matrix.Block Mathlib.Data.Matrix.Cartan Mathlib.Data.Matrix.ColumnRowPartitioned Mathlib.Data.Matrix.Composition Mathlib.Data.Matrix.DualNumber Mathlib.Data.Matrix.Invertible Mathlib.Data.Matrix.Reflection Mathlib.Data.Nat.Factorial.SuperFactorial Mathlib.Data.Nat.Totient Mathlib.Data.Setoid.Partition.Card Mathlib.Dynamics.FixedPoints.Support Mathlib.Dynamics.FixedPoints.Topology Mathlib.Dynamics.Flow Mathlib.Dynamics.Minimal Mathlib.Dynamics.OmegaLimit Mathlib.Dynamics.SymbolicDynamics.Basic Mathlib.Dynamics.Transitive Mathlib.FieldTheory.PrimeField Mathlib.FieldTheory.RatFunc.Defs Mathlib.Geometry.Convex.Cone.Basic Mathlib.Geometry.Convex.Cone.DualFinite Mathlib.Geometry.Convex.Cone.Dual Mathlib.Geometry.Convex.Cone.Face.Basic Mathlib.Geometry.Convex.Cone.Pointed Mathlib.Geometry.Convex.Cone.Simplicial Mathlib.Geometry.Convex.ConvexSpace.AffineSpace Mathlib.Geometry.Convex.ConvexSpace.Module Mathlib.Geometry.Convex.Hull Mathlib.Geometry.Convex.Set Mathlib.Geometry.Convex.Star Mathlib.Geometry.RingedSpace.Basic Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits Mathlib.Geometry.RingedSpace.PresheafedSpace Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.Geometry.RingedSpace.Stalks Mathlib.GroupTheory.Archimedean Mathlib.GroupTheory.CommutingProbability Mathlib.GroupTheory.CosetCover Mathlib.GroupTheory.Coxeter.Basic Mathlib.GroupTheory.Coxeter.Matrix Mathlib.GroupTheory.FixedPointFree Mathlib.GroupTheory.GroupAction.Blocks Mathlib.GroupTheory.GroupAction.Iwasawa Mathlib.GroupTheory.GroupAction.Jordan Mathlib.GroupTheory.GroupAction.MultiplePrimitivity Mathlib.GroupTheory.GroupAction.MultipleTransitivity Mathlib.GroupTheory.GroupAction.Primitive Mathlib.GroupTheory.GroupAction.SubMulAction.Combination Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup Mathlib.GroupTheory.IsSubnormal Mathlib.GroupTheory.NoncommPiCoprod Mathlib.GroupTheory.PGroup Mathlib.GroupTheory.Perm.Centralizer Mathlib.GroupTheory.Perm.ConjAct Mathlib.GroupTheory.Perm.Cycle.Concrete Mathlib.GroupTheory.Perm.Cycle.Factors Mathlib.GroupTheory.Perm.Cycle.PossibleTypes Mathlib.GroupTheory.Perm.Cycle.Type Mathlib.GroupTheory.Perm.Fin Mathlib.GroupTheory.Perm.MaximalSubgroups Mathlib.GroupTheory.Solvable Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups Mathlib.GroupTheory.SpecificGroups.Alternating Mathlib.GroupTheory.SpecificGroups.Cyclic Mathlib.GroupTheory.SpecificGroups.Dihedral Mathlib.GroupTheory.SpecificGroups.KleinFour Mathlib.GroupTheory.SpecificGroups.Quaternion Mathlib.GroupTheory.Torsion Mathlib.LinearAlgebra.AffineSpace.AffineEquiv Mathlib.LinearAlgebra.AffineSpace.AffineMap Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift Mathlib.LinearAlgebra.AffineSpace.Basis Mathlib.LinearAlgebra.AffineSpace.Centroid Mathlib.LinearAlgebra.AffineSpace.Ceva Mathlib.LinearAlgebra.AffineSpace.Combination Mathlib.LinearAlgebra.AffineSpace.Independent Mathlib.LinearAlgebra.AffineSpace.MidpointZero Mathlib.LinearAlgebra.AffineSpace.Midpoint Mathlib.LinearAlgebra.AffineSpace.Ordered Mathlib.LinearAlgebra.AffineSpace.Pointwise Mathlib.LinearAlgebra.AffineSpace.Restrict Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid Mathlib.LinearAlgebra.AffineSpace.Slope Mathlib.LinearAlgebra.Alternating.Basic Mathlib.LinearAlgebra.Alternating.Curry Mathlib.LinearAlgebra.Alternating.DomCoprod Mathlib.LinearAlgebra.Alternating.Uncurry.Fin Mathlib.LinearAlgebra.Basis.Basic Mathlib.LinearAlgebra.Basis.Cardinality Mathlib.LinearAlgebra.Basis.Exact Mathlib.LinearAlgebra.Basis.Fin Mathlib.LinearAlgebra.Basis.Flag Mathlib.LinearAlgebra.Basis.Prod Mathlib.LinearAlgebra.Basis.SMul Mathlib.LinearAlgebra.Basis.Submodule Mathlib.LinearAlgebra.Basis.VectorSpace Mathlib.LinearAlgebra.BilinearForm.Basic Mathlib.LinearAlgebra.BilinearForm.Hom Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv Mathlib.LinearAlgebra.Countable Mathlib.LinearAlgebra.CrossProduct Mathlib.LinearAlgebra.DFinsupp Mathlib.LinearAlgebra.Dimension.Basic Mathlib.LinearAlgebra.Dimension.Finrank Mathlib.LinearAlgebra.Dimension.Subsingleton Mathlib.LinearAlgebra.DirectSum.Basis Mathlib.LinearAlgebra.DirectSum.Finite Mathlib.LinearAlgebra.DirectSum.Finsupp Mathlib.LinearAlgebra.DirectSum.TensorProduct Mathlib.LinearAlgebra.Finsupp.Pi Mathlib.LinearAlgebra.Finsupp.Span Mathlib.LinearAlgebra.Finsupp.VectorSpace Mathlib.LinearAlgebra.FixedSubmodule Mathlib.LinearAlgebra.FreeModule.Basic Mathlib.LinearAlgebra.FreeModule.Finite.Basic Mathlib.LinearAlgebra.FreeProduct.Basic Mathlib.LinearAlgebra.Goursat Mathlib.LinearAlgebra.Isomorphisms Mathlib.LinearAlgebra.LeftExact Mathlib.LinearAlgebra.LinearIndependent.Lemmas Mathlib.LinearAlgebra.LinearPMap Mathlib.LinearAlgebra.Matrix.AbsoluteValue Mathlib.LinearAlgebra.Matrix.Basis Mathlib.LinearAlgebra.Matrix.Bilinear Mathlib.LinearAlgebra.Matrix.Cartan Mathlib.LinearAlgebra.Matrix.Circulant Mathlib.LinearAlgebra.Matrix.ConjTranspose Mathlib.LinearAlgebra.Matrix.Determinant.Basic Mathlib.LinearAlgebra.Matrix.Determinant.Misc Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular Mathlib.LinearAlgebra.Matrix.DotProduct Mathlib.LinearAlgebra.Matrix.DualNumber Mathlib.LinearAlgebra.Matrix.Dual Mathlib.LinearAlgebra.Matrix.Hadamard Mathlib.LinearAlgebra.Matrix.Invertible Mathlib.LinearAlgebra.Matrix.IsDiag Mathlib.LinearAlgebra.Matrix.Kronecker Mathlib.LinearAlgebra.Matrix.Module Mathlib.LinearAlgebra.Matrix.MvPolynomial Mathlib.LinearAlgebra.Matrix.Notation Mathlib.LinearAlgebra.Matrix.Permanent Mathlib.LinearAlgebra.Matrix.Reindex Mathlib.LinearAlgebra.Matrix.RowCol Mathlib.LinearAlgebra.Matrix.StdBasis Mathlib.LinearAlgebra.Matrix.Symmetric Mathlib.LinearAlgebra.Matrix.ToLin Mathlib.LinearAlgebra.Matrix.Trace Mathlib.LinearAlgebra.Matrix.Transvection Mathlib.LinearAlgebra.Matrix.Unique Mathlib.LinearAlgebra.Matrix.Vec Mathlib.LinearAlgebra.Multilinear.Basic Mathlib.LinearAlgebra.Multilinear.Basis Mathlib.LinearAlgebra.Multilinear.Curry Mathlib.LinearAlgebra.Multilinear.DFinsupp Mathlib.LinearAlgebra.Multilinear.DirectSum Mathlib.LinearAlgebra.Multilinear.Finsupp Mathlib.LinearAlgebra.Multilinear.Pi Mathlib.LinearAlgebra.Multilinear.TensorProduct Mathlib.LinearAlgebra.PiTensorProduct.Basic Mathlib.LinearAlgebra.PiTensorProduct.Basis Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp Mathlib.LinearAlgebra.PiTensorProduct.DirectSum Mathlib.LinearAlgebra.PiTensorProduct.Dual Mathlib.LinearAlgebra.PiTensorProduct.Finite Mathlib.LinearAlgebra.PiTensorProduct.Finsupp Mathlib.LinearAlgebra.PiTensorProduct.Generators Mathlib.LinearAlgebra.PiTensorProduct Mathlib.LinearAlgebra.Pi Mathlib.LinearAlgebra.Prod Mathlib.LinearAlgebra.Projection Mathlib.LinearAlgebra.Quotient.Basic Mathlib.LinearAlgebra.Quotient.Bilinear Mathlib.LinearAlgebra.Quotient.Pi Mathlib.LinearAlgebra.Ray Mathlib.LinearAlgebra.SModEq.Basic Mathlib.LinearAlgebra.SModEq.Pointwise Mathlib.LinearAlgebra.SesquilinearForm.Basic Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal Mathlib.LinearAlgebra.Span.Basic Mathlib.LinearAlgebra.StdBasis Mathlib.LinearAlgebra.SymmetricAlgebra.Basic Mathlib.LinearAlgebra.TensorAlgebra.Basic Mathlib.LinearAlgebra.TensorAlgebra.Grading Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower Mathlib.LinearAlgebra.TensorPower.Basic Mathlib.LinearAlgebra.TensorPower.Pairing Mathlib.LinearAlgebra.TensorPower.Symmetric Mathlib.LinearAlgebra.TensorProduct.Associator Mathlib.LinearAlgebra.TensorProduct.Basic Mathlib.LinearAlgebra.TensorProduct.Basis Mathlib.LinearAlgebra.TensorProduct.Decomposition Mathlib.LinearAlgebra.TensorProduct.Defs Mathlib.LinearAlgebra.TensorProduct.DirectLimit Mathlib.LinearAlgebra.TensorProduct.Finiteness Mathlib.LinearAlgebra.TensorProduct.Free Mathlib.LinearAlgebra.TensorProduct.Graded.External Mathlib.LinearAlgebra.TensorProduct.Graded.Internal Mathlib.LinearAlgebra.TensorProduct.Map Mathlib.LinearAlgebra.TensorProduct.Matrix Mathlib.LinearAlgebra.TensorProduct.Opposite Mathlib.LinearAlgebra.TensorProduct.Pi Mathlib.LinearAlgebra.TensorProduct.Prod Mathlib.LinearAlgebra.TensorProduct.Subalgebra Mathlib.LinearAlgebra.TensorProduct.Submodule Mathlib.LinearAlgebra.TensorProduct.Tower Mathlib.MeasureTheory.Constructions.Cylinders Mathlib.MeasureTheory.Constructions.SimpleGraph Mathlib.MeasureTheory.Constructions.SubmoduleQuotient Mathlib.MeasureTheory.MeasurableSpace.Constructions Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated Mathlib.MeasureTheory.MeasurableSpace.Embedding Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated Mathlib.MeasureTheory.MeasurableSpace.NCard Mathlib.MeasureTheory.MeasurableSpace.Pi Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict Mathlib.MeasureTheory.MeasurableSpace.Prod Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs Mathlib.ModelTheory.Bundled Mathlib.ModelTheory.Complexity Mathlib.ModelTheory.DirectLimit Mathlib.ModelTheory.ElementaryMaps Mathlib.ModelTheory.ElementarySubstructures Mathlib.ModelTheory.Equivalence Mathlib.ModelTheory.FinitelyGenerated Mathlib.ModelTheory.Graph Mathlib.ModelTheory.PartialEquiv Mathlib.ModelTheory.Satisfiability Mathlib.ModelTheory.Skolem Mathlib.ModelTheory.Substructures Mathlib.ModelTheory.Topology.Types Mathlib.ModelTheory.Types Mathlib.ModelTheory.Ultraproducts Mathlib.NumberTheory.Basic Mathlib.NumberTheory.FactorisationProperties Mathlib.NumberTheory.PrimeCounting Mathlib.Order.BooleanGenerators Mathlib.Order.CompactlyGenerated.Basic Mathlib.Order.CompactlyGenerated.Intervals Mathlib.Order.Interval.Finset.Box Mathlib.Order.KonigLemma Mathlib.Order.KrullDimension Mathlib.Order.Partition.Equipartition Mathlib.Probability.Kernel.IonescuTulcea.Maps Mathlib.RingTheory.Adjoin.Basic Mathlib.RingTheory.AlgebraTower Mathlib.RingTheory.AlgebraicIndependent.Defs Mathlib.RingTheory.Bialgebra.Basic Mathlib.RingTheory.Bialgebra.Convolution Mathlib.RingTheory.Bialgebra.Equiv Mathlib.RingTheory.Bialgebra.Hom Mathlib.RingTheory.Bialgebra.SymmetricAlgebra Mathlib.RingTheory.Bialgebra.TensorProduct Mathlib.RingTheory.ChainOfDivisors Mathlib.RingTheory.Coalgebra.Basic Mathlib.RingTheory.Coalgebra.CoassocSimps Mathlib.RingTheory.Coalgebra.Convolution Mathlib.RingTheory.Coalgebra.Equiv Mathlib.RingTheory.Coalgebra.Hom Mathlib.RingTheory.Coalgebra.MulOpposite Mathlib.RingTheory.Coalgebra.TensorProduct Mathlib.RingTheory.Congruence.Hom Mathlib.RingTheory.Finiteness.Basic Mathlib.RingTheory.Finiteness.Bilinear Mathlib.RingTheory.Finiteness.Cardinality Mathlib.RingTheory.Finiteness.Defs Mathlib.RingTheory.Finiteness.Finsupp Mathlib.RingTheory.Finiteness.Lattice Mathlib.RingTheory.Finiteness.Prod Mathlib.RingTheory.Finiteness.Projective Mathlib.RingTheory.Finiteness.Subalgebra Mathlib.RingTheory.GradedAlgebra.AlgHom Mathlib.RingTheory.GradedAlgebra.Basic Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring Mathlib.RingTheory.GradedAlgebra.RingHom Mathlib.RingTheory.GradedAlgebra.TensorProduct Mathlib.RingTheory.HahnSeries.Cardinal Mathlib.RingTheory.HahnSeries.Multiplication Mathlib.RingTheory.HahnSeries.Summable Mathlib.RingTheory.HopfAlgebra.Basic Mathlib.RingTheory.HopfAlgebra.Convolution Mathlib.RingTheory.HopfAlgebra.TensorProduct Mathlib.RingTheory.Ideal.Basis Mathlib.RingTheory.Ideal.IsAugmentation Mathlib.RingTheory.Ideal.Maximal Mathlib.RingTheory.Ideal.Nonunits Mathlib.RingTheory.Ideal.Span Mathlib.RingTheory.IntegralClosure.Algebra.Defs Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs Mathlib.RingTheory.IsTensorProduct Mathlib.RingTheory.LocalRing.Basic Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs Mathlib.RingTheory.Localization.Basic Mathlib.RingTheory.Localization.Cardinality Mathlib.RingTheory.Localization.FractionRing Mathlib.RingTheory.Localization.Module Mathlib.RingTheory.Localization.NumDen Mathlib.RingTheory.MatrixAlgebra Mathlib.RingTheory.Morita.Basic Mathlib.RingTheory.Morita.Matrix Mathlib.RingTheory.MvPolynomial.Basic Mathlib.RingTheory.MvPolynomial.Symmetric.Defs Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities Mathlib.RingTheory.MvPolynomial.Tower Mathlib.RingTheory.MvPowerSeries.Basic Mathlib.RingTheory.MvPowerSeries.Inverse Mathlib.RingTheory.MvPowerSeries.LexOrder Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors Mathlib.RingTheory.MvPowerSeries.Order Mathlib.RingTheory.MvPowerSeries.Trunc Mathlib.RingTheory.Noetherian.Defs Mathlib.RingTheory.Noetherian.Filter Mathlib.RingTheory.OrzechProperty Mathlib.RingTheory.PiTensorProduct Mathlib.RingTheory.Regular.Category Mathlib.RingTheory.SimpleRing.Basic Mathlib.RingTheory.SimpleRing.Congr Mathlib.RingTheory.SimpleRing.Defs Mathlib.RingTheory.SimpleRing.Field Mathlib.RingTheory.Spectrum.Maximal.Defs Mathlib.RingTheory.TensorProduct.Basic Mathlib.RingTheory.TensorProduct.Free Mathlib.RingTheory.TensorProduct.Maps Mathlib.RingTheory.TensorProduct.MonoidAlgebra Mathlib.RingTheory.TensorProduct.Pi Mathlib.SetTheory.Cardinal.EventuallyConst Mathlib.SetTheory.Cardinal.Subfield Mathlib.Tactic.Algebraize Mathlib.Tactic.Module Mathlib.Topology.AlexandrovDiscrete Mathlib.Topology.Algebra.Affine Mathlib.Topology.Algebra.Algebra.Rat Mathlib.Topology.Algebra.ConstMulAction Mathlib.Topology.Algebra.Constructions.DomMulAct Mathlib.Topology.Algebra.Constructions Mathlib.Topology.Algebra.Group.AddTorsor Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup Mathlib.Topology.Algebra.Group.Torsor Mathlib.Topology.Algebra.Group.Units Mathlib.Topology.Algebra.GroupWithZero Mathlib.Topology.Algebra.InfiniteSum.Basic Mathlib.Topology.Algebra.InfiniteSum.Defs Mathlib.Topology.Algebra.Monoid.AddChar Mathlib.Topology.Algebra.Monoid.FunOnFinite Mathlib.Topology.Algebra.Monoid Mathlib.Topology.Algebra.MulAction Mathlib.Topology.Algebra.Order.Group Mathlib.Topology.Algebra.Order.Module Mathlib.Topology.Algebra.Order.Support Mathlib.Topology.Algebra.ProperConstSMul Mathlib.Topology.Algebra.Semigroup Mathlib.Topology.Algebra.Star Mathlib.Topology.Algebra.Support Mathlib.Topology.Algebra.WithZeroTopology Mathlib.Topology.ApproximateUnit Mathlib.Topology.Baire.LocallyCompactRegular Mathlib.Topology.Category.CompHausLike.Basic Mathlib.Topology.Category.CompHausLike.Cartesian Mathlib.Topology.Category.CompHausLike.EffectiveEpi Mathlib.Topology.Category.CompHausLike.Limits Mathlib.Topology.Category.CompHausLike.SigmaComparison Mathlib.Topology.Category.FinTopCat Mathlib.Topology.Category.Sequential Mathlib.Topology.Category.TopCat.Adjunctions Mathlib.Topology.Category.TopCat.Basic Mathlib.Topology.Category.TopCat.EffectiveEpi Mathlib.Topology.Category.TopCat.EpiMono Mathlib.Topology.Category.TopCat.GrothendieckTopology Mathlib.Topology.Category.TopCat.Limits.Basic Mathlib.Topology.Category.TopCat.Limits.Cofiltered Mathlib.Topology.Category.TopCat.Limits.Konig Mathlib.Topology.Category.TopCat.Limits.Products Mathlib.Topology.Category.TopCat.Limits.Pullbacks Mathlib.Topology.Category.TopCat.OpenNhds Mathlib.Topology.Category.TopCat.Opens Mathlib.Topology.Category.TopCat.ULift Mathlib.Topology.Category.TopCat.Yoneda Mathlib.Topology.Category.UniformSpace Mathlib.Topology.ClopenBox Mathlib.Topology.CompactOpen Mathlib.Topology.Compactification.OnePoint.Basic Mathlib.Topology.Compactification.StoneCech Mathlib.Topology.Compactness.CompactSystem Mathlib.Topology.Compactness.CompactlyCoherentSpace Mathlib.Topology.Compactness.CountablyCompact Mathlib.Topology.Compactness.NhdsKer Mathlib.Topology.Compactness.Paracompact Mathlib.Topology.Connected.Basic Mathlib.Topology.Connected.CardComponents Mathlib.Topology.Connected.Clopen Mathlib.Topology.Connected.LocallyConnected Mathlib.Topology.Connected.Separation Mathlib.Topology.Connected.TotallyDisconnected Mathlib.Topology.Constructible Mathlib.Topology.ContinuousMap.Basic Mathlib.Topology.ContinuousMap.CocompactMap Mathlib.Topology.ContinuousMap.Interval Mathlib.Topology.ContinuousMap.Ordered Mathlib.Topology.ContinuousMap.SecondCountableSpace Mathlib.Topology.ContinuousMap.Sigma Mathlib.Topology.ContinuousMap.T0Sierpinski Mathlib.Topology.Convenient.Category Mathlib.Topology.Convenient.ContinuousMapGeneratedBy Mathlib.Topology.Convenient.GeneratedBy Mathlib.Topology.Convenient.HomSpace Mathlib.Topology.Convenient.Localization Mathlib.Topology.Convenient.OpenClosed Mathlib.Topology.Covering.Basic Mathlib.Topology.DenseEmbedding Mathlib.Topology.DerivedSet Mathlib.Topology.DiscreteQuotient Mathlib.Topology.DiscreteSubset Mathlib.Topology.ExtendFrom Mathlib.Topology.ExtremallyDisconnected Mathlib.Topology.FiberBundle.Basic Mathlib.Topology.FiberBundle.Constructions Mathlib.Topology.FiberBundle.Trivialization Mathlib.Topology.FiberPartition Mathlib.Topology.Filter Mathlib.Topology.GDelta.MetrizableSpace Mathlib.Topology.Germ Mathlib.Topology.Gluing Mathlib.Topology.Hom.Open Mathlib.Topology.Homeomorph.Lemmas Mathlib.Topology.Homeomorph.Quotient Mathlib.Topology.IndicatorConstPointwise Mathlib.Topology.Instances.Discrete Mathlib.Topology.Instances.Sign Mathlib.Topology.Irreducible Mathlib.Topology.IsClosedRestrict Mathlib.Topology.IsLocalHomeomorph Mathlib.Topology.JacobsonSpace Mathlib.Topology.KrullDimension Mathlib.Topology.LocalAtTarget Mathlib.Topology.LocallyConstant.Algebra Mathlib.Topology.LocallyConstant.Basic Mathlib.Topology.LocallyFinsupp.Pushforward Mathlib.Topology.LocallyFinsupp Mathlib.Topology.Maps.Proper.Basic Mathlib.Topology.Maps.Proper.CompactlyGenerated Mathlib.Topology.Maps.Proper.UniversallyClosed Mathlib.Topology.Maps.Strict.Basic Mathlib.Topology.Metrizable.Basic Mathlib.Topology.NatEmbedding Mathlib.Topology.NoetherianSpace Mathlib.Topology.OmegaCompletePartialOrder Mathlib.Topology.OpenPartialHomeomorph.Basic Mathlib.Topology.OpenPartialHomeomorph.Composition Mathlib.Topology.OpenPartialHomeomorph.Constructions Mathlib.Topology.OpenPartialHomeomorph.Continuity Mathlib.Topology.OpenPartialHomeomorph.IsImage Mathlib.Topology.Order.AtTopBotIxx Mathlib.Topology.Order.Basic Mathlib.Topology.Order.Category.AlexDisc Mathlib.Topology.Order.Completion Mathlib.Topology.Order.CountableSeparating Mathlib.Topology.Order.DenselyOrdered Mathlib.Topology.Order.ExtendFrom Mathlib.Topology.Order.ExtrClosure Mathlib.Topology.Order.Filter Mathlib.Topology.Order.HullKernel Mathlib.Topology.Order.IsLUB Mathlib.Topology.Order.IsLocallyClosed Mathlib.Topology.Order.IsNormal Mathlib.Topology.Order.Lattice Mathlib.Topology.Order.LawsonTopology Mathlib.Topology.Order.LeftRightNhds Mathlib.Topology.Order.LowerUpperTopology Mathlib.Topology.Order.MonotoneContinuity Mathlib.Topology.Order.MonotoneConvergence Mathlib.Topology.Order.NhdsSet Mathlib.Topology.Order.OrderClosedExtr Mathlib.Topology.Order.OrderClosed Mathlib.Topology.Order.PartialSups Mathlib.Topology.Order.Priestley Mathlib.Topology.Order.ProjIcc Mathlib.Topology.Order.ScottTopology Mathlib.Topology.Order.SuccPred Mathlib.Topology.Order.T5 Mathlib.Topology.Order.UpperLowerSetTopology Mathlib.Topology.Order.WithTop Mathlib.Topology.Perfect Mathlib.Topology.QuasiSeparated Mathlib.Topology.Semicontinuity.Hemicontinuity Mathlib.Topology.SeparatedMap Mathlib.Topology.Separation.AlexandrovDiscrete Mathlib.Topology.Separation.Basic Mathlib.Topology.Separation.Connected Mathlib.Topology.Separation.CountableSeparatingOn Mathlib.Topology.Separation.DisjointCover Mathlib.Topology.Separation.GDelta Mathlib.Topology.Separation.Hausdorff Mathlib.Topology.Separation.LinearUpperLowerSetTopology Mathlib.Topology.Separation.NotNormal Mathlib.Topology.Separation.Profinite Mathlib.Topology.Separation.Regular Mathlib.Topology.Sequences Mathlib.Topology.Sets.BaseChangeNhds Mathlib.Topology.Sets.Closeds Mathlib.Topology.Sets.CompactOpenCovered Mathlib.Topology.Sets.Compacts Mathlib.Topology.Sets.OpenCover Mathlib.Topology.Sets.Opens Mathlib.Topology.Sets.Order Mathlib.Topology.Sets.VietorisTopology Mathlib.Topology.Sheaves.Abelian Mathlib.Topology.Sheaves.AddCommGrpCat Mathlib.Topology.Sheaves.Alexandrov Mathlib.Topology.Sheaves.EtaleSpace Mathlib.Topology.Sheaves.Flasque Mathlib.Topology.Sheaves.Forget Mathlib.Topology.Sheaves.Functors Mathlib.Topology.Sheaves.Limits Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Topology.Sheaves.MayerVietoris Mathlib.Topology.Sheaves.Module Mathlib.Topology.Sheaves.Over Mathlib.Topology.Sheaves.PUnit Mathlib.Topology.Sheaves.Points Mathlib.Topology.Sheaves.PresheafOfFunctions Mathlib.Topology.Sheaves.Presheaf Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.Topology.Sheaves.SheafCondition.Sites Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.Topology.Sheaves.Sheaf Mathlib.Topology.Sheaves.Sheafify Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.Sheaves.Stalks Mathlib.Topology.ShrinkingLemma Mathlib.Topology.Sober Mathlib.Topology.Specialization Mathlib.Topology.Spectral.Basic Mathlib.Topology.Spectral.ConstructibleTopology Mathlib.Topology.Spectral.Hom Mathlib.Topology.Spectral.Prespectral Mathlib.Topology.UniformSpace.AbstractCompletion Mathlib.Topology.UniformSpace.Ascoli Mathlib.Topology.UniformSpace.Cauchy Mathlib.Topology.UniformSpace.Closeds Mathlib.Topology.UniformSpace.CompactConvergence Mathlib.Topology.UniformSpace.CompleteSeparated Mathlib.Topology.UniformSpace.Completion Mathlib.Topology.UniformSpace.Equicontinuity Mathlib.Topology.UniformSpace.Equiv Mathlib.Topology.UniformSpace.HeineCantor Mathlib.Topology.UniformSpace.LocallyUniformConvergence Mathlib.Topology.UniformSpace.OfCompactT2 Mathlib.Topology.UniformSpace.Pi Mathlib.Topology.UniformSpace.Separation Mathlib.Topology.UniformSpace.Ultra.Completion Mathlib.Topology.UniformSpace.Ultra.Constructions Mathlib.Topology.UniformSpace.UniformApproximation Mathlib.Topology.UniformSpace.UniformConvergenceTopology Mathlib.Topology.UniformSpace.UniformConvergence Mathlib.Topology.UniformSpace.UniformEmbedding	9
43 files Mathlib.Algebra.BigOperators.Intervals Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite Mathlib.Algebra.Order.Disjointed Mathlib.Algebra.Order.Group.PartialSups Mathlib.Algebra.Order.Hom.Lattice Mathlib.Algebra.Order.SuccPred.PartialSups Mathlib.Combinatorics.Compactness Mathlib.Data.Fintype.Order Mathlib.Data.Set.Accumulate Mathlib.Data.Set.Dissipate Mathlib.Data.Setoid.Partition Mathlib.MeasureTheory.PiSystem Mathlib.MeasureTheory.SetAlgebra Mathlib.MeasureTheory.SetSemiring Mathlib.Order.Atoms.Finite Mathlib.Order.Birkhoff Mathlib.Order.Category.FinBddDistLat Mathlib.Order.Category.FinBoolAlg Mathlib.Order.Category.NonemptyFinLinOrd Mathlib.Order.CountableDenseLinearOrder Mathlib.Order.Disjointed Mathlib.Order.Filter.EventuallyConst Mathlib.Order.Filter.FilterProduct Mathlib.Order.Filter.Subsingleton Mathlib.Order.Filter.Ultrafilter.Basic Mathlib.Order.Ideal Mathlib.Order.PFilter Mathlib.Order.PartialSups Mathlib.Order.Partition.Basic Mathlib.Order.Partition.Finpartition Mathlib.Order.PrimeIdeal Mathlib.Order.PrimeSeparator Mathlib.Order.SetAccumulate Mathlib.Order.SetDissipate Mathlib.Order.SupIndep Mathlib.Topology.Compactness.Bases Mathlib.Topology.Compactness.Compact Mathlib.Topology.Compactness.Lindelof Mathlib.Topology.Compactness.LocallyCompact Mathlib.Topology.Compactness.LocallyFinite Mathlib.Topology.Compactness.SigmaCompact Mathlib.Topology.Ultrafilter Mathlib.Topology.UniformSpace.Compact	10
10 files Mathlib.Algebra.Group.Subgroup.Order Mathlib.GroupTheory.Subgroup.Simple Mathlib.Order.Atoms Mathlib.Order.Filter.Pointwise Mathlib.Order.Filter.Ultrafilter.Defs Mathlib.Order.ModularLattice Mathlib.Order.Radical Mathlib.Order.SuccPred.Tree Mathlib.Order.ZornAtoms Mathlib.Topology.Defs.Ultrafilter	11

---

Declarations diff (regex)

+ DistribLattice.ofSupInfLeAssoc
+ isModularLattice_iff_eq_of_le_of_inf_le_of_le_sup
+ ofEqOfInfSupEq
+ ofInfSupLeSupInf

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 1df8bea).

• +4 new declarations
• −0 removed declarations

+DistribLattice.ofEqOfInfSupEq
+DistribLattice.ofInfSupLeSupInf
+DistribLattice.ofSupInfLeAssoc
+isModularLattice_iff_eq_of_le_of_inf_le_of_le_sup

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 1df8bea232
Reference commit 4efb186f10

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).

[alreadydone]

Hopefully this is reasonable despite the large-import

[plp127]

!radar

[leanprover-radar]

Benchmark results for 1df8bea against 4efb186 are in. There are significant results. @plp127

• 🟥 build//instructions: +223.4G (+0.14%)

Large changes (1🟥)

• 🟥 build/module/Mathlib.Order.ModularLattice//instructions: +16.6G (+115.94%)

Small changes (1🟥)

1 hidden