Team Ai
Datasetpublic

MathNetwork/MathlibGraph

MathlibGraph: The Multinetwork of Mathlib Dependency graph of Mathlib (commit 534cf0b, 2 Feb 2026), the largest formal mathematics library for Lean 4 (v4.28.0-rc1). Three dependency layers (declarations, modules, namespaces), each with nodes, edges, and precomputed network metrics. Quick Stats Declarations Modules Namespaces (k=2) Nodes 308,129 7,564 10,097 Edges 8,436,366 20,881 332,081 (weighted) DAG depth 83 154 7 (after SCC condensation)… See the full description on the dataset page: https://huggingface.co/datasets/MathNetwork/MathlibGraph.

sourceHugging Faceapache-2.0updated 6mo agoView on Hugging Face
0likes466downloads
rootv2modulenodes.csv
nodes.csv7566 linesDownload Raw Back to module
1module,decl_count2Mathlib.Algebra.Order.Module.Equiv,63Mathlib.Topology.Instances.Sign,54Mathlib.LinearAlgebra.Matrix.Determinant.Misc,45Mathlib.LinearAlgebra.Matrix.Stochastic,286Mathlib.RingTheory.RingHom.FiniteType,137Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic,98Mathlib.Logic.Equiv.Functor,109Mathlib.Topology.IsClosedRestrict,1210Mathlib.Analysis.AbsoluteValue.Equivalence,3211Mathlib.CategoryTheory.Monad.Algebra,12512Mathlib.Algebra.PEmptyInstances,213Mathlib.Data.Multiset.Fintype,5614Mathlib.Data.Nat.Totient,4715Mathlib.Tactic.FastInstance,216Mathlib.Data.Finset.Dedup,3517Mathlib.Topology.EMetricSpace.Defs,18318Mathlib.Algebra.Polynomial.Div,9619Mathlib.Probability.ProbabilityMassFunction.Binomial,720Mathlib.RingTheory.Adjoin.PowerBasis,1221Mathlib.Algebra.Algebra.NonUnitalSubalgebra,21722Mathlib.Algebra.GroupWithZero.Action.Basic,1323Mathlib.Data.PNat.Xgcd,8424Mathlib.Data.Nat.BitIndices,1525Mathlib.CategoryTheory.Bicategory.Extension,7426Mathlib.RingTheory.Spectrum.Prime.Noetherian,527Mathlib.Combinatorics.SetFamily.KruskalKatona,828Mathlib.CategoryTheory.Monoidal.Free.Coherence,4529Mathlib.MeasureTheory.MeasurableSpace.Constructions,18330Mathlib.Algebra.Order.CauSeq.Basic,16631Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff,3132Mathlib.Combinatorics.SetFamily.Shadow,3733Mathlib.NumberTheory.LSeries.Deriv,1234Mathlib.Analysis.SpecificLimits.Fibonacci,235Mathlib.Data.PNat.Notation,636Mathlib.Algebra.Lie.IdealOperations,3637Mathlib.Analysis.Convex.Caratheodory,938Mathlib.Algebra.Order.Group.Indicator,5639Mathlib.CategoryTheory.Category.Pointed,3940Mathlib.Data.Real.ENatENNReal,2641Mathlib.Tactic.ReduceModChar.Ext,142Mathlib.Topology.MetricSpace.Contracting,4143Mathlib.Algebra.Order.Nonneg.Lattice,944Mathlib.Condensed.Solid,1045Mathlib.RingTheory.RootsOfUnity.Minpoly,1246Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic,6547Mathlib.Tactic.CategoryTheory.Elementwise,748Mathlib.Data.Sigma.Basic,4549Mathlib.Algebra.BigOperators.GroupWithZero.Finset,1150Mathlib.Algebra.Polynomial.CoeffList,1551Mathlib.FieldTheory.PolynomialGaloisGroup,4752Mathlib.CategoryTheory.Sites.Monoidal,1253Mathlib.Data.Nat.Factorization.Basic,7154Mathlib.Analysis.CStarAlgebra.Projection,255Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties,456Mathlib.Order.Filter.AtTopBot.Finset,1157Mathlib.Algebra.Ring.Subring.Order,458Mathlib.Analysis.Normed.Group.Basic,57259Mathlib.Tactic.Explode,360Mathlib.CategoryTheory.Functor.KanExtension.Dense,1761Mathlib.Data.Sigma.Order,3162Mathlib.Algebra.Polynomial.Coeff,6463Mathlib.GroupTheory.Coset.Defs,6164Mathlib.Order.CompleteLattice.Chain,1565Mathlib.Topology.Defs.Sequences,1566Mathlib.AlgebraicGeometry.Morphisms.Descent,1067Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal,968Mathlib.AlgebraicGeometry.ResidueField,6769Mathlib.Geometry.RingedSpace.Stalks,2370Mathlib.RingTheory.Adjoin.Singleton,771Mathlib.MeasureTheory.Measure.Haar.Disintegration,572Mathlib.Topology.Algebra.Constructions.DomMulAct,8073Mathlib.Data.Set.Finite.Lattice,6174Mathlib.Computability.Ackermann,4975Mathlib.CategoryTheory.LiftingProperties.Over,276Mathlib.Algebra.BigOperators.RingEquiv,777Mathlib.Data.Set.SymmDiff,1278Mathlib.RingTheory.Nakayama,1779Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels,280Mathlib.AlgebraicGeometry.RelativeGluing,2381Mathlib.CategoryTheory.Limits.Indization.ParallelPair,3482Mathlib.Topology.ContinuousMap.Lattice,683Mathlib.CategoryTheory.Limits.Preserves.Limits,2684Mathlib.Algebra.DirectSum.Internal,5885Mathlib.Algebra.Star.MonoidHom,8086Mathlib.RingTheory.IntegralClosure.Algebra.Ideal,487Mathlib.Data.Nat.PrimeFin,2988Mathlib.RingTheory.Polynomial.Wronskian,1689Mathlib.Algebra.Homology.HomotopyCategory.MappingCone,10690Mathlib.Analysis.InnerProductSpace.CanonicalTensor,391Mathlib.Data.NNReal.Defs,22492Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic,2093Mathlib.CategoryTheory.Closed.FunctorToTypes,094Mathlib.CategoryTheory.Sites.Precoverage,5295Mathlib.GroupTheory.IsSubnormal,2196Mathlib.FieldTheory.RatFunc.Defs,3097Mathlib.Algebra.Ring.Action.ConjAct,198Mathlib.Algebra.Group.Invertible.Basic,3199Mathlib.Deprecated.RingHom,0100Mathlib.CategoryTheory.Galois.Topology,24101Mathlib.Tactic.CategoryTheory.Coherence.Basic,6102Mathlib.Analysis.Distribution.Distribution,5103Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure,31104Mathlib.Topology.ContinuousMap.Compact,83105Mathlib.Algebra.Category.ModuleCat.Differentials.Basic,15106Mathlib.SetTheory.Ordinal.NaturalOps,142107Mathlib.CategoryTheory.Monoidal.Bimon_,126108Mathlib.Analysis.Calculus.Implicit,88109Mathlib.Algebra.Field.GeomSum,8110Mathlib.Data.Finset.Insert,145111Mathlib.RingTheory.NoetherNormalization,4112Mathlib.Topology.Instances.TrivSqZeroExt,38113Mathlib.SetTheory.ZFC.Ordinal,67114Mathlib.Tactic.CategoryTheory.Monoidal.Basic,4115Mathlib.Tactic.Linter.DocString,3116Mathlib.RepresentationTheory.Homological.GroupHomology.Basic,26117Mathlib.RingTheory.Invariant.Defs,4118Mathlib.Tactic.RewriteSearch,1119Mathlib.Analysis.Analytic.WithLp,4120Mathlib.Data.Option.NAry,33121Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno,85122Mathlib.CategoryTheory.Limits.Preserves.Bifunctor,44123Mathlib.Tactic.Generalize,1124Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite,34125Mathlib.Algebra.Polynomial.SpecificDegree,3126Mathlib.Topology.Connected.Clopen,51127Mathlib.Topology.UniformSpace.Completion,85128Mathlib.Data.Fintype.Pi,34129Mathlib.Analysis.Asymptotics.Theta,81130Mathlib.Data.QPF.Multivariate.Constructions.Sigma,14131Mathlib.GroupTheory.Subgroup.Center,33132Mathlib.Algebra.Central.Defs,3133Mathlib.Analysis.SpecialFunctions.Exp,71134Mathlib.Algebra.Group.Action.Pointwise.Set.Finite,8135Mathlib.Algebra.Order.GroupWithZero.WithZero,9136Mathlib.Data.Multiset.AddSub,89137Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol,50138Mathlib.Order.Interval.Set.OrdConnectedLinear,5139Mathlib.RingTheory.Localization.NormTrace,6140Mathlib.Control.Lawful,3141Mathlib.Computability.TuringDegree,39142Mathlib.ModelTheory.Skolem,12143Mathlib.Tactic.Subsingleton,5144Mathlib.Combinatorics.Matroid.Dual,39145Mathlib.Algebra.Order.BigOperators.Ring.List,1146Mathlib.MeasureTheory.Integral.CircleAverage,29147Mathlib.Util.DischargerAsTactic,1148Mathlib.MeasureTheory.Group.Arithmetic,257149Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono,6150Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap,27151Mathlib.Topology.MetricSpace.Similarity,47152Mathlib.CategoryTheory.Monad.Comonadicity,51153Mathlib.Data.Int.LeastGreatest,8154Mathlib.Topology.Instances.Discrete,6155Mathlib.Algebra.Order.Ring.Archimedean,51156Mathlib.CategoryTheory.Presentable.Adjunction,10157Mathlib.CategoryTheory.Limits.Preserves.Creates.Pullbacks,2158Mathlib.GroupTheory.Commutator.Basic,53159Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real,18160Mathlib.RingTheory.Ideal.Colon,32161Mathlib.RingTheory.PowerSeries.WellKnown,24162Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification,95163Mathlib.Algebra.Algebra.Hom,112164Mathlib.Algebra.Divisibility.Hom,3165Mathlib.CategoryTheory.Core,99166Mathlib.CategoryTheory.ExtremalEpi,8167Mathlib.CategoryTheory.ObjectProperty.ShiftAdditive,1168Mathlib.Algebra.MvPolynomial.Variables,32169Mathlib.Combinatorics.SimpleGraph.Walks.Maps,47170Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic,38171Mathlib.InformationTheory.KullbackLeibler.KLFun,26172Mathlib.Order.Category.Preord,51173Mathlib.CategoryTheory.Adjunction.Evaluation,20174Mathlib.LinearAlgebra.FreeModule.Determinant,1175Mathlib.CategoryTheory.Bicategory.LocallyGroupoid,63176Mathlib.Algebra.BigOperators.Finprod,278177Mathlib.Algebra.Field.ModEq,3178Mathlib.AlgebraicGeometry.LimitsOver,12179Mathlib.Algebra.Group.Nat.Defs,14180Mathlib.Logic.Encodable.Basic,110181Mathlib.Combinatorics.Additive.SmallTripling,4182Mathlib.Algebra.BigOperators.ModEq,40183Mathlib.Algebra.Polynomial.PartialFractions,2184Mathlib.CategoryTheory.Products.Basic,135185Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point,98186Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization,3187Mathlib.CategoryTheory.Monoidal.Closed.Functor,15188Mathlib.Probability.Moments.Covariance,51189Mathlib.LinearAlgebra.Quotient.Defs,48190Mathlib.Algebra.Category.Ring.Under.Basic,27191Mathlib.Data.Prod.TProd,23192Mathlib.Util.FormatTable,16193Mathlib.Tactic.Linter.TextBased.UnicodeLinter,3194Mathlib.Probability.Martingale.Convergence,18195Mathlib.Analysis.Normed.Module.RCLike.Basic,7196Mathlib.Algebra.Module.Card,1197Mathlib.MeasureTheory.Function.ConvergenceInMeasure,40198Mathlib.CategoryTheory.Abelian.Projective.Basic,3199Mathlib.LinearAlgebra.FiniteDimensional.Lemmas,36200Mathlib.CategoryTheory.Monoidal.Closed.Basic,106201Mathlib.Data.PFunctor.Multivariate.W,40202Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric,2203Mathlib.Topology.Algebra.IsUniformGroup.Basic,91204Mathlib.Dynamics.Transitive,22205Mathlib.Algebra.GroupWithZero.Equiv,8206Mathlib.Topology.Category.CompHaus.Projective,3207Mathlib.Algebra.GroupWithZero.Nat,7208Mathlib.FieldTheory.PurelyInseparable.Exponent,36209Mathlib.GroupTheory.GroupAction.Quotient,78210Mathlib.Topology.Algebra.MetricSpace.Lipschitz,4211Mathlib.Probability.Kernel.MeasurableLIntegral,14212Mathlib.Topology.Instances.RealVectorSpace,5213Mathlib.RingTheory.Unramified.Locus,8214Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody,54215Mathlib.CategoryTheory.Sites.CompatibleSheafification,13216Mathlib.Data.List.Destutter,41217Mathlib.Topology.Category.CompactlyGenerated,28218Mathlib.Algebra.GroupWithZero.Divisibility,24219Mathlib.Analysis.Convolution,85220Mathlib.MeasureTheory.Measure.DiracProba,22221Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating,7222Mathlib.Algebra.Star.NonUnitalSubalgebra,216223Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap,27224Mathlib.ModelTheory.Ultraproducts,8225Mathlib.MeasureTheory.Function.ConvergenceInDistribution,16226Mathlib.Analysis.Calculus.FDeriv.Comp,35227Mathlib.RingTheory.Valuation.Basic,210228Mathlib.CategoryTheory.Comma.Over.OverClass,53229Mathlib.Algebra.Group.Pointwise.Set.Scalar,120230Mathlib.Data.PEquiv,75231Mathlib.Algebra.Category.ModuleCat.Limits,38232Mathlib.RingTheory.WittVector.Frobenius,28233Mathlib.RingTheory.QuotSMulTop,18234Mathlib.Algebra.Group.Pointwise.Finset.Scalar,132235Mathlib.Algebra.Category.CommAlgCat.FiniteType,18236Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic,69237Mathlib.Analysis.CStarAlgebra.Unitary.Connected,49238Mathlib.RingTheory.Smooth.StandardSmoothCotangent,38239Mathlib.CategoryTheory.Sites.Hypercover.One,174240Mathlib.Geometry.Manifold.VectorBundle.Pullback,1241Mathlib.LinearAlgebra.QuadraticForm.Real,6242Mathlib.RingTheory.FreeCommRing,53243Mathlib.CategoryTheory.Idempotents.Karoubi,79244Mathlib.Topology.Hom.Open,34245Mathlib.Algebra.MvPolynomial.Invertible,2246Mathlib.RingTheory.Morita.Matrix,31247Mathlib.CategoryTheory.Retract,69248Mathlib.Topology.Algebra.Star.Real,2249Mathlib.AlgebraicGeometry.Morphisms.Integral,25250Mathlib.Topology.ContinuousOn,172251Mathlib.Tactic.Basic,17252Mathlib.NumberTheory.NumberField.Discriminant.Basic,23253Mathlib.FieldTheory.IsPerfectClosure,77254Mathlib.Data.Pi.Interval,14255Mathlib.Algebra.Homology.Embedding.TruncLEHomology,22256Mathlib.Data.Analysis.Filter,56257Mathlib.NumberTheory.ArithmeticFunction.Misc,69258Mathlib.NumberTheory.LSeries.ZMod,33259Mathlib.LinearAlgebra.TensorProduct.Associator,49260Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan,80261Mathlib.Algebra.Category.ModuleCat.Basic,120262Mathlib.CategoryTheory.Category.Grpd,0263Mathlib.CategoryTheory.Sites.CartesianMonoidal,13264Mathlib.Order.Types.Defs,38265Mathlib.LinearAlgebra.SModEq.Pointwise,1266Mathlib.CategoryTheory.Localization.Monoidal.Braided,16267Mathlib.Data.Fintype.Sets,61268Mathlib.Tactic.NormNum.NatLog,5269Mathlib.Analysis.Calculus.Monotone,6270Mathlib.LinearAlgebra.BilinearForm.Orthogonal,41271Mathlib.GroupTheory.Perm.MaximalSubgroups,20272Mathlib.RingTheory.AdjoinRoot,177273Mathlib.Order.OmegaCompletePartialOrder,151274Mathlib.RingTheory.Nilpotent.Lemmas,17275Mathlib.GroupTheory.MonoidLocalization.Cardinality,2276Mathlib.Algebra.Star.Unitary,126277Mathlib.Algebra.Group.Submonoid.BigOperators,32278Mathlib.Algebra.Homology.TotalComplexShift,42279Mathlib.Geometry.RingedSpace.PresheafedSpace,75280Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1,43281Mathlib.RingTheory.Coalgebra.Hom,72282Mathlib.AlgebraicGeometry.Stalk,59283Mathlib.Analysis.InnerProductSpace.Basic,158284Mathlib.Analysis.Normed.Algebra.Basic,2285Mathlib.Algebra.MvPolynomial.Expand,34286Mathlib.GroupTheory.MonoidLocalization.Basic,393287Mathlib.Data.PSigma.Order,16288Mathlib.Analysis.Analytic.IteratedFDeriv,19289Mathlib.Data.Nat.Choose.Factorization,23290Mathlib.Data.PNat.Find,17291Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho,42292Mathlib.LinearAlgebra.FreeModule.IdealQuotient,5293Mathlib.GroupTheory.FreeGroup.Reduce,113294Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim,13295Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order,60296Mathlib.Algebra.Homology.ShortComplex.Abelian,61297Mathlib.SetTheory.Cardinal.Arithmetic,112298Mathlib.Analysis.Complex.Asymptotics,12299Mathlib.Algebra.Module.Presentation.Tensor,13300Mathlib.Topology.UniformSpace.Compact,20301Mathlib.RingTheory.KrullDimension.Zero,22302Mathlib.Data.Nat.Factorial.DoubleFactorial,12303Mathlib.Analysis.LocallyConvex.StrongTopology,2304Mathlib.CategoryTheory.Functor.ReflectsIso.Basic,10305Mathlib.Topology.Category.LightProfinite.Injective,5306Mathlib.Algebra.Order.Monoid.ToMulBot,8307Mathlib.Data.Array.Defs,3308Mathlib.Tactic.Nontriviality.Core,5309Mathlib.CategoryTheory.Groupoid.Discrete,2310Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp,31311Mathlib.CategoryTheory.Limits.Shapes.Connected,2312Mathlib.Topology.Algebra.Valued.ValuativeRel,34313Mathlib.MeasureTheory.Function.LpSpace.Basic,154314Mathlib.Topology.ContinuousMap.Sigma,4315Mathlib.AlgebraicGeometry.Fiber,21316Mathlib.Data.PFunctor.Univariate.M,116317Mathlib.Algebra.Category.CoalgCat.Basic,44318Mathlib.MeasureTheory.Integral.CircleIntegral,67319Mathlib.Algebra.Group.Pi.Basic,73320Mathlib.Data.Option.Basic,48321Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic,284322Mathlib.Algebra.EuclideanDomain.Field,5323Mathlib.Algebra.Order.Monoid.NatCast,20324Mathlib.Algebra.GCDMonoid.Finset,42325Mathlib.Algebra.MonoidAlgebra.Lift,12326Mathlib.Topology.Order.LiminfLimsup,50327Mathlib.AlgebraicGeometry.GammaSpecAdjunction,89328Mathlib.Algebra.GroupWithZero.Pointwise.Finset,12329Mathlib.Algebra.DirectSum.AddChar,3330Mathlib.Logic.Nontrivial.Defs,23331Mathlib.Algebra.Category.MonCat.Yoneda,22332Mathlib.Analysis.InnerProductSpace.Dual,23333Mathlib.Data.Nat.Cast.Basic,34334Mathlib.Topology.Category.Compactum,39335Mathlib.Data.Multiset.FinsetOps,52336Mathlib.Combinatorics.SimpleGraph.DegreeSum,12337Mathlib.Algebra.Group.Finsupp,95338Mathlib.Analysis.SpecialFunctions.Complex.LogBounds,34339Mathlib.Algebra.Order.Nonneg.Module,8340Mathlib.AlgebraicGeometry.OpenImmersion,169341Mathlib.AlgebraicTopology.SimplicialSet.CompStruct,39342Mathlib.Tactic.Ring,0343Mathlib.Analysis.SpecialFunctions.Gamma.Basic,42344Mathlib.Analysis.Normed.Group.SeparationQuotient,15345Mathlib.Probability.Martingale.Centering,15346Mathlib.Algebra.Group.Submonoid.Pointwise,73347Mathlib.Util.Simp,1348Mathlib.AlgebraicGeometry.Morphisms.Preimmersion,21349Mathlib.RingTheory.Ideal.Maps,204350Mathlib.RingTheory.Spectrum.Prime.Polynomial,15351Mathlib.Topology.Algebra.GroupWithZero,54352Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass,99353Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology,34354Mathlib.Data.List.Enum,4355Mathlib.Probability.Independence.Kernel.IndepFun,77356Mathlib.Analysis.NormedSpace.HomeomorphBall,0357Mathlib.Combinatorics.Derangements.Exponential,1358Mathlib.Algebra.Ring.Action.Pointwise.Set,7359Mathlib.Probability.Process.Stopping,123360Mathlib.CategoryTheory.Monoidal.Functor,321361Mathlib.CategoryTheory.Bicategory.InducedBicategory,55362Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle,81363Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift,102364Mathlib.Data.Int.Fib.Lemmas,2365Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu,12366Mathlib.Topology.Algebra.Module.Multilinear.Topology,35367Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing,60368Mathlib.LinearAlgebra.Projectivization.Independence,11369Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four,15370Mathlib.Algebra.Group.ConjFinite,5371Mathlib.CategoryTheory.Sites.Localization,12372Mathlib.Data.Set.Inclusion,14373Mathlib.Algebra.Group.Torsion,37374Mathlib.Order.Interval.Set.OrderEmbedding,10375Mathlib.MeasureTheory.OuterMeasure.AE,57376Mathlib.Analysis.Calculus.UniformLimitsDeriv,17377Mathlib.Data.Finset.Lattice.Pi,2378Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono,15379Mathlib.LinearAlgebra.FreeModule.ModN,10380Mathlib.Topology.Algebra.Order.UpperLower,16381Mathlib.Tactic.ToFun,1382Mathlib.LinearAlgebra.FreeModule.Basic,30383Mathlib.CategoryTheory.Functor.CurryingThree,46384Mathlib.Tactic.NormNum.RealSqrt,8385Mathlib.Probability.Kernel.Composition.KernelLemmas,10386Mathlib.RingTheory.Extension.Cotangent.LocalizationAway,17387Mathlib.Data.Set.Finite.Powerset,2388Mathlib.CategoryTheory.ObjectProperty.Extensions,8389Mathlib.GroupTheory.MonoidLocalization.Order,24390Mathlib.Tactic.ExistsI,1391Mathlib.RingTheory.Spectrum.Prime.TensorProduct,4392Mathlib.Algebra.Ring.Invertible,26393Mathlib.CategoryTheory.Bicategory.Adjunction.Cat,13394Mathlib.Data.PFun,115395Mathlib.Data.List.Duplicate,28396Mathlib.Data.Set.Disjoint,32397Mathlib.Algebra.Lie.LieTheorem,4398Mathlib.MeasureTheory.Measure.Haar.NormedSpace,26399Mathlib.Logic.Equiv.List,27400Mathlib.CategoryTheory.Limits.Types.Products,48401Mathlib.CategoryTheory.Limits.Cones,334402Mathlib.Algebra.Category.Grp.Adjunctions,24403Mathlib.Algebra.Category.CoalgCat.Monoidal,19404Mathlib.FieldTheory.PurelyInseparable.Tower,18405Mathlib.CategoryTheory.Subobject.MonoOver,95406Mathlib.Algebra.Group.Pointwise.Set.BigOperators,34407Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring,25408Mathlib.GroupTheory.Archimedean,7409Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov,8410Mathlib.MeasureTheory.Function.EssSup,55411Mathlib.CategoryTheory.Shift.CommShiftTwo,33412Mathlib.LinearAlgebra.PerfectPairing.Restrict,8413Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor,92414Mathlib.SetTheory.Ordinal.Rank,11415Mathlib.LinearAlgebra.Matrix.FixedDetMatrices,27416Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology,80417Mathlib.Analysis.CStarAlgebra.Basic,50418Mathlib.LinearAlgebra.FreeModule.Norm,4419Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp,24420Mathlib.CategoryTheory.Sites.Closed,26421Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions,161422Mathlib.Algebra.Order.Monoid.Unbundled.Basic,386423Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete,6424Mathlib.Data.Seq.Parallel,14425Mathlib.MeasureTheory.Covering.LiminfLimsup,6426Mathlib.Algebra.Order.Group.Pointwise.Interval,249427Mathlib.CategoryTheory.Sites.Hypercover.Homotopy,42428Mathlib.Tactic.Linarith.Verification,13429Mathlib.Algebra.Group.Action.TransferInstance,11430Mathlib.CategoryTheory.Preadditive.SingleObj,1431Mathlib.Order.SetIsMax,2432Mathlib.MeasureTheory.Measure.HasOuterApproxClosed,21433Mathlib.NumberTheory.Padics.PadicNumbers,156434Mathlib.RingTheory.Polynomial.Chebyshev,145435Mathlib.Analysis.Normed.Group.Lemmas,2436Mathlib.GroupTheory.Perm.ViaEmbedding,6437Mathlib.Algebra.Group.Invertible.Defs,45438Mathlib.Data.Set.BooleanAlgebra,2439Mathlib.Algebra.Lie.Basic,268440Mathlib.Algebra.Order.Monoid.Defs,40441Mathlib.Analysis.Normed.Algebra.QuaternionExponential,10442Mathlib.Algebra.Order.Archimedean.Hom,7443Mathlib.Algebra.Group.Nat.Even,22444Mathlib.Topology.OpenPartialHomeomorph.Defs,61445Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan,2446Mathlib.Topology.Instances.Int,16447Mathlib.CategoryTheory.CodiscreteCategory,32448Mathlib.MeasureTheory.OuterMeasure.OfAddContent,10449Mathlib.RingTheory.Ideal.Int,8450Mathlib.Algebra.Category.ModuleCat.Simple,5451Mathlib.Data.Nat.Bits,56452Mathlib.ModelTheory.LanguageMap,128453Mathlib.Topology.Algebra.OpenSubgroup,186454Mathlib.Algebra.Order.Monovary,212455Mathlib.CategoryTheory.Monad.Coequalizer,18456Mathlib.Data.Fin.Tuple.Finset,15457Mathlib.Probability.Kernel.Composition.MeasureCompProd,48458Mathlib.Topology.MetricSpace.GromovHausdorff,41459Mathlib.Probability.Kernel.Composition.ParallelComp,20460Mathlib.Tactic.Monotonicity,0461Mathlib.Algebra.Order.Ring.Defs,29462Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes,63463Mathlib.Data.Nat.ModEq,118464Mathlib.Algebra.Order.Interval.Set.Monoid,18465Mathlib.CategoryTheory.Functor.Basic,29466Mathlib.CategoryTheory.Products.Unitor,24467Mathlib.Tactic.Linter.DocPrime,1468Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits,16469Mathlib.CategoryTheory.Action.Monoidal,62470Mathlib.Probability.Martingale.OptionalStopping,7471Mathlib.NumberTheory.LSeries.Linearity,28472Mathlib.Analysis.Analytic.RadiusLiminf,2473Mathlib.Util.Qq,9474Mathlib.Dynamics.Ergodic.RadonNikodym,3475Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm,0476Mathlib.Tactic.Monotonicity.Basic,1477Mathlib.AlgebraicGeometry.Modules.Tilde,43478Mathlib.Analysis.Normed.Lp.Matrix,15479Mathlib.Data.ENat.Pow,18480Mathlib.Topology.Order.AtTopBotIxx,22481Mathlib.Data.Rat.Init,20482Mathlib.Probability.Moments.ComplexMGF,24483Mathlib.CategoryTheory.Category.Cat.Terminal,5484Mathlib.Order.CompleteBooleanAlgebra,200485Mathlib.MeasureTheory.Integral.TorusIntegral,24486Mathlib.Data.Nat.NthRoot.Defs,2487Mathlib.Topology.Algebra.Nonarchimedean.Basic,24488Mathlib.SetTheory.Surreal.Basic,75489Mathlib.Topology.Algebra.Module.ClosedSubmodule,82490Mathlib.RingTheory.KrullDimension.Regular,19491Mathlib.MeasureTheory.OuterMeasure.Basic,31492Mathlib.FieldTheory.Isaacs,9493Mathlib.Combinatorics.Derangements.Finite,12494Mathlib.Topology.Category.Profinite.Projective,3495Mathlib.Analysis.InnerProductSpace.Semisimple,2496Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs,154497Mathlib.Algebra.FiveLemma,21498Mathlib.LinearAlgebra.TensorAlgebra.Basis,9499Mathlib.LinearAlgebra.PiTensorProduct.Dual,12500Mathlib.Analysis.Real.Cardinality,29501Mathlib.Data.ENat.Defs,8502Mathlib.Topology.Algebra.InfiniteSum.Order,85503Mathlib.CategoryTheory.Limits.Preserves.Grothendieck,6504Mathlib.CategoryTheory.Filtered.Small,46505Mathlib.Topology.FiberBundle.Constructions,58506Mathlib.CategoryTheory.Monoidal.Grp_,202507Mathlib.RingTheory.Ideal.Operations,208508Mathlib.NumberTheory.Harmonic.Bounds,5509Mathlib.Algebra.Ring.AddAut,6510Mathlib.Computability.Language,96511Mathlib.Computability.Halting,54512Mathlib.Data.Set.Subset,25513Mathlib.RingTheory.DedekindDomain.SelmerGroup,18514Mathlib.LinearAlgebra.PiTensorProduct.Basis,4515Mathlib.AlgebraicTopology.CechNerve,75516Mathlib.Algebra.Order.Monoid.Units,26517Mathlib.Algebra.GroupWithZero.Submonoid.Primal,1518Mathlib.RepresentationTheory.Tannaka,29519Mathlib.Util.ElabWithoutMVars,1520Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus,0521Mathlib.Algebra.GroupWithZero.Units.Basic,111522Mathlib.Geometry.Manifold.MFDeriv.NormedSpace,34523Mathlib.Order.Filter.Cofinite,47524Mathlib.CategoryTheory.ConcreteCategory.Elementwise,10525Mathlib.Algebra.Category.Grp.Yoneda,22526Mathlib.Data.List.Sym,30527Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex,75528Mathlib.Probability.Process.Predictable,13529Mathlib.Control.EquivFunctor,15530Mathlib.LinearAlgebra.Matrix.ToLin,187531Mathlib.LinearAlgebra.Matrix.Diagonal,6532Mathlib.MeasureTheory.Covering.Besicovitch,66533Mathlib.CategoryTheory.Abelian.Refinements,5534Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp,61535Mathlib.Analysis.Normed.Order.Hom.Ultra,2536Mathlib.Analysis.Calculus.FDeriv.Analytic,85537Mathlib.Combinatorics.Quiver.Basic,27538Mathlib.CategoryTheory.Category.Quiv,53539Mathlib.AlgebraicTopology.DoldKan.FunctorN,12540Mathlib.GroupTheory.Torsion,65541Mathlib.Order.Category.BddDistLat,55542Mathlib.CategoryTheory.Generator.Abelian,2543Mathlib.MeasureTheory.Measure.WithDensity,86544Mathlib.Algebra.Lie.Free,53545Mathlib.Algebra.Homology.ShortComplex.PreservesHomology,139546Mathlib.CategoryTheory.Closed.Types,0547Mathlib.NumberTheory.Primorial,7548Mathlib.Data.Fin.Tuple.Reflection,23549Mathlib.Algebra.Order.Ring.Pow,9550Mathlib.Algebra.GCDMonoid.FinsetLemmas,3551Mathlib.Algebra.MvPolynomial.Polynomial,2552Mathlib.Algebra.MvPolynomial.Division,40553Mathlib.Tactic.Linter.MinImports,4554Mathlib.Data.DFinsupp.Module,23555Mathlib.Combinatorics.SimpleGraph.Girth,17556Mathlib.CategoryTheory.Filtered.Basic,114557Mathlib.Topology.LocallyConstant.Basic,118558Mathlib.Data.Rat.Cast.Defs,44559Mathlib.Analysis.CStarAlgebra.CStarMatrix,152560Mathlib.MeasureTheory.Constructions.Polish.Basic,75561Mathlib.SetTheory.Cardinal.HasCardinalLT,23562Mathlib.RingTheory.WittVector.Compare,22563Mathlib.Algebra.Quaternion,477564Mathlib.LinearAlgebra.TensorProduct.Subalgebra,31565Mathlib.Data.Matrix.Basic,167566Mathlib.Probability.Kernel.MeasurableIntegral,9567Mathlib.CategoryTheory.Functor.Trifunctor,30568Mathlib.Topology.OmegaCompletePartialOrder,9569Mathlib.Probability.Kernel.Disintegration.Integral,28570Mathlib.Topology.Algebra.Equicontinuity,4571Mathlib.Algebra.Polynomial.Lifts,22572Mathlib.CategoryTheory.Monoidal.Functor.Types,3573Mathlib.Combinatorics.Enumerative.Partition.GenFun,8574Mathlib.RingTheory.Coprime.Lemmas,43575Mathlib.GroupTheory.FreeGroup.CyclicallyReduced,42576Mathlib.AlgebraicTopology.ModelCategory.Homotopy,14577Mathlib.Analysis.LocallyConvex.Polar,51578Mathlib.Algebra.Module.Torsion.Prod,1579Mathlib.CategoryTheory.Preadditive.EilenbergMoore,16580Mathlib.Order.Disjoint,165581Mathlib.Analysis.SpecialFunctions.Log.ERealExp,21582Mathlib.MeasureTheory.Measure.LogLikelihoodRatio,21583Mathlib.MeasureTheory.Measure.Complex,19584Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas,7585Mathlib.Analysis.Oscillation,10586Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs,47587Mathlib.RingTheory.RingHom.LocallyStandardSmooth,3588Mathlib.Topology.UniformSpace.UniformEmbedding,84589Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise,11590Mathlib.Data.Set.Order,17591Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky,1592Mathlib.Algebra.Order.Floor.Semifield,14593Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Def,3594Mathlib.Algebra.FreeMonoid.Symbols,10595Mathlib.Algebra.Group.Pointwise.Set.Lattice,120596Mathlib.Topology.Algebra.Valued.ValuedField,27597Mathlib.Algebra.Regular.Pi,7598Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp,4599Mathlib.Data.Int.Range,6600Mathlib.Combinatorics.Enumerative.Stirling,24601Mathlib.Analysis.SpecialFunctions.Complex.Log,49602Mathlib.Analysis.Convex.Radon,9603Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap,11604Mathlib.Topology.Order.Compact,76605Mathlib.RingTheory.Finiteness.Finsupp,9606Mathlib.Data.Nat.Factorial.NatCast,7607Mathlib.Order.Interval.Set.UnorderedInterval,94608Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong,93609Mathlib.Data.List.Shortlex,16610Mathlib.Analysis.Convex.NNReal,4611Mathlib.Algebra.QuadraticAlgebra.Defs,136612Mathlib.Algebra.Colimit.TensorProduct,1613Mathlib.Order.Category.CompleteLat,22614Mathlib.Data.Matrix.DualNumber,3615Mathlib.Analysis.Convex.KreinMilman,3616Mathlib.RingTheory.Flat.CategoryTheory,6617Mathlib.Algebra.Module.ZMod,16618Mathlib.RingTheory.SimpleRing.Field,2619Mathlib.Tactic.GCongr.CoreAttrs,3620Mathlib.Util.TermReduce,8621Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace,9622Mathlib.Analysis.Complex.BorelCaratheodory,2623Mathlib.NumberTheory.NumberField.InfiniteAdeleRing,14624Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing,29625Mathlib.AlgebraicTopology.SimplicialSet.Basic,59626Mathlib.Analysis.Normed.Lp.MeasurableSpace,10627Mathlib.Analysis.Complex.TaylorSeries,12628Mathlib.AlgebraicGeometry.Sites.BigZariski,4629Mathlib.LinearAlgebra.Matrix.Reindex,17630Mathlib.Analysis.Analytic.Composition,77631Mathlib.MeasureTheory.Measure.GiryMonad,49632Mathlib.CategoryTheory.Monoidal.Braided.Opposite,3633Mathlib.Algebra.SkewPolynomial.Basic,24634Mathlib.Algebra.Group.Subgroup.Basic,212635Mathlib.Tactic.Linter.DeprecatedModule,4636Mathlib.MeasureTheory.Integral.IntervalAverage,8637Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality,122638Mathlib.NumberTheory.Transcendental.Liouville.Residual,5639Mathlib.Algebra.Polynomial.Mirror,23640Mathlib.Topology.IsLocalHomeomorph,37641Mathlib.Algebra.NeZero,14642Mathlib.Algebra.Category.Grp.Kernels,4643Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable,38644Mathlib.Topology.Bornology.Real,3645Mathlib.Tactic.NoncommRing,3646Mathlib.Data.Finset.NatDivisors,7647Mathlib.Analysis.Calculus.LocalExtr.Rolle,4648Mathlib.CategoryTheory.ObjectProperty.Retract,14649Mathlib.Analysis.CStarAlgebra.Multiplier,101650Mathlib.Combinatorics.SimpleGraph.Diam,80651Mathlib.Analysis.Analytic.CPolynomialDef,64652Mathlib.RingTheory.Perfectoid.FontaineTheta,15653Mathlib.RingTheory.Unramified.Pi,2654Mathlib.RingTheory.FiniteLength,16655Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal,13656Mathlib.CategoryTheory.Functor.Const,21657Mathlib.CategoryTheory.Functor.Flat,35658Mathlib.Analysis.Normed.Ring.InfiniteSum,17659Mathlib.Algebra.Order.Group.Unbundled.Basic,277660Mathlib.Algebra.Ring.Shrink,16661Mathlib.Data.Finset.Powerset,49662Mathlib.Data.Multiset.Sort,15663Mathlib.Data.Finite.Perm,1664Mathlib.Combinatorics.SimpleGraph.Walks.Operations,145665Mathlib.Data.Fin.SuccPred,194666Mathlib.Tactic.CategoryTheory.BicategoryCoherence,28667Mathlib.CategoryTheory.EffectiveEpi.RegularEpi,0668Mathlib.RingTheory.Localization.Pi,6669Mathlib.Topology.Compactification.StoneCech,49670Mathlib.Geometry.Manifold.Bordism,34671Mathlib.CategoryTheory.Limits.Preorder,36672Mathlib.Algebra.Order.Star.Basic,72673Mathlib.CategoryTheory.Sites.CoversTop,14674Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv,14675Mathlib.MeasureTheory.Function.AEMeasurableSequence,17676Mathlib.Analysis.Convex.DoublyStochasticMatrix,16677Mathlib.Data.Fin.Parity,19678Mathlib.Analysis.Normed.Algebra.Ultra,3679Mathlib.SetTheory.Ordinal.Principal,45680Mathlib.Topology.Instances.Matrix,85681Mathlib.Data.List.Indexes,5682Mathlib.CategoryTheory.Limits.Indization.Category,41683Mathlib.Data.Finset.Interval,23684Mathlib.Algebra.Module.Torsion.Field,1685Mathlib.CategoryTheory.Limits.Preserves.Yoneda,3686Mathlib.CategoryTheory.Preadditive.Indization,2687Mathlib.RingTheory.SimpleModule.IsAlgClosed,2688Mathlib.RingTheory.Flat.Tensor,8689Mathlib.RingTheory.Finiteness.ModuleFinitePresentation,4690Mathlib.Algebra.Star.Conjneg,26691Mathlib.RingTheory.Extension.Presentation.Core,66692Mathlib.CategoryTheory.Category.Cat.CartesianClosed,24693Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived,19694Mathlib.Data.Fintype.Option,9695Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro,2696Mathlib.Data.Finset.Density,40697Mathlib.Topology.Category.Stonean.Basic,32698Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas,23699Mathlib.Topology.Metrizable.CompletelyMetrizable,43700Mathlib.Analysis.BoundedVariation,9701Mathlib.Algebra.Homology.ShortComplex.Retract,1702Mathlib.Analysis.Normed.Field.Basic,73703Mathlib.LinearAlgebra.LinearIndependent.Lemmas,78704Mathlib.CategoryTheory.Limits.Shapes.IsTerminal,78705Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify,40706Mathlib.Data.Finset.Order,2707Mathlib.CategoryTheory.Monoidal.Mon_,268708Mathlib.Data.Int.Lemmas,17709Mathlib.Algebra.BigOperators.Finsupp.Fin,7710Mathlib.Data.Real.Basic,121711Mathlib.Algebra.Group.Subsemigroup.Membership,26712Mathlib.Probability.Independence.Integration,22713Mathlib.RingTheory.OrzechProperty,9714Mathlib.RingTheory.RingHom.OpenImmersion,19715Mathlib.RingTheory.Finiteness.Projective,1716Mathlib.Topology.Category.Born,11717Mathlib.Topology.MetricSpace.ShrinkingLemma,6718Mathlib.Probability.Decision.Risk.Basic,26719Mathlib.Lean.Elab.Term,3720Mathlib.Algebra.Homology.Embedding.TruncLE,47721Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv,25722Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits,2723Mathlib.Analysis.Complex.JensenFormula,4724Mathlib.LinearAlgebra.Complex.Orientation,1725Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine,68726Mathlib.Topology.Category.Profinite.Nobeling.Successor,63727Mathlib.Logic.Embedding.Set,32728Mathlib.LinearAlgebra.Isomorphisms,25729Mathlib.Topology.Algebra.Module.WeakBilin,16730Mathlib.Algebra.Polynomial.Eval.Irreducible,1731Mathlib.Tactic.GRewrite,0732Mathlib.CategoryTheory.Bicategory.Product,67733Mathlib.Algebra.DirectSum.Basic,75734Mathlib.RingTheory.Regular.IsSMulRegular,22735Mathlib.Algebra.Homology.Embedding.AreComplementary,46736Mathlib.CategoryTheory.Monoidal.Closed.Types,7737Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor,128738Mathlib.CategoryTheory.SingleObj,40739Mathlib.RingTheory.PowerSeries.Expand,20740Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro,2741Mathlib.CategoryTheory.Bicategory.CatEnriched,62742Mathlib.Data.Rat.Encodable,1743Mathlib.Algebra.BigOperators.Ring.List,10744Mathlib.Algebra.QuadraticAlgebra.Basic,45745Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf,16746Mathlib.Tactic.NormNum,0747Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated,59748Mathlib.CategoryTheory.Sites.Equivalence,43749Mathlib.Analysis.Fourier.FourierTransformDeriv,63750Mathlib.CategoryTheory.Limits.MonoCoprod,25751Mathlib.Order.Basic,323752Mathlib.MeasureTheory.Function.LpSeminorm.Trim,7753Mathlib.NumberTheory.LucasLehmer,115754Mathlib.Algebra.Quandle,150755Mathlib.Data.DFinsupp.Interval,23756Mathlib.Order.Atoms,227757Mathlib.LinearAlgebra.Dimension.Basic,51758Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric,9759Mathlib.Algebra.Lie.Engel,14760Mathlib.Topology.Instances.ENat,19761Mathlib.Analysis.Normed.Module.MStructure,38762Mathlib.Algebra.Field.Subfield.Basic,106763Mathlib.Order.Defs.LinearOrder,85764Mathlib.Tactic.TautoSet,2765Mathlib.Combinatorics.SimpleGraph.Tutte,7766Mathlib.Topology.ContinuousMap.ContinuousMapZero,110767Mathlib.CategoryTheory.Monoidal.Braided.Transport,8768Mathlib.Algebra.Order.CompleteField,45769Mathlib.AlgebraicTopology.DoldKan.NReflectsIso,3770Mathlib.Data.Nat.Factorial.Basic,85771Mathlib.RingTheory.Ideal.Maximal,27772Mathlib.Tactic.NormNum.Abs,5773Mathlib.Algebra.ContinuedFractions.Determinant,2774Mathlib.Data.List.Cycle,153775Mathlib.AlgebraicTopology.SimplicialSet.Presentable,3776Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived,11777Mathlib.Data.Finite.Prod,34778Mathlib.Data.ENNReal.Real,85779Mathlib.Tactic.Widget.InteractiveUnfold,12780Mathlib.MeasureTheory.VectorMeasure.WithDensity,21781Mathlib.Algebra.GCDMonoid.IntegrallyClosed,2782Mathlib.Probability.Kernel.Invariance,8783Mathlib.Analysis.Complex.UpperHalfPlane.Exp,4784Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor,1785Mathlib.MeasureTheory.Function.ContinuousMapDense,15786Mathlib.Topology.UniformSpace.UniformConvergence,82787Mathlib.CategoryTheory.Abelian.Projective.Resolution,50788Mathlib.Order.SetNotation,36789Mathlib.GroupTheory.Subgroup.Simple,22790Mathlib.CategoryTheory.Limits.Types.Pushouts,40791Mathlib.Algebra.Order.Ring.Star,1792Mathlib.Topology.Category.CompHaus.Limits,4793Mathlib.Data.List.Triplewise,19794Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual,0795Mathlib.Algebra.Polynomial.Identities,4796Mathlib.MeasureTheory.Constructions.SubmoduleQuotient,2797Mathlib.NumberTheory.Transcendental.Liouville.Basic,5798Mathlib.Algebra.GroupWithZero.ProdHom,24799Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs,3800Mathlib.Order.BooleanGenerators,14801Mathlib.Order.Bounds.Basic,243802Mathlib.Data.ENNReal.Holder,34803Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn,7804Mathlib.Order.Interval.Set.ProjIcc,74805Mathlib.Topology.ContinuousMap.Star,22806Mathlib.Topology.Algebra.FilterBasis,88807Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries,28808Mathlib.RingTheory.TensorProduct.MonoidAlgebra,20809Mathlib.RingTheory.Polynomial.Hermite.Gaussian,3810Mathlib.Topology.Subpath,25811Mathlib.Algebra.CharP.Defs,66812Mathlib.RingTheory.MvPowerSeries.Evaluation,42813Mathlib.Data.Finsupp.Defs,92814Mathlib.Analysis.Convex.Jensen,26815Mathlib.Topology.Sheaves.Over,8816Mathlib.CategoryTheory.ObjectProperty.Equivalence,13817Mathlib.CategoryTheory.Limits.Constructions.Pullbacks,4818Mathlib.Data.Real.Pi.Bounds,0819Mathlib.RingTheory.Coalgebra.MonoidAlgebra,15820Mathlib.NumberTheory.Harmonic.EulerMascheroni,18821Mathlib.Util.PrintSorries,13822Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique,42823Mathlib.RingTheory.Lasker,20824Mathlib.Algebra.Ring.CentroidHom,110825Mathlib.CategoryTheory.Abelian.Monomorphisms,0826Mathlib.Algebra.Ring.Action.Basic,14827Mathlib.Tactic.HigherOrder,5828Mathlib.GroupTheory.OreLocalization.Basic,144829Mathlib.Analysis.Matrix.LDL,12830Mathlib.Algebra.MonoidAlgebra.Cardinal,12831Mathlib.Tactic.FindSyntax,3832Mathlib.Data.Tree.Basic,36833Mathlib.Algebra.Lie.Semisimple.Lemmas,3834Mathlib.Algebra.Homology.ExactSequenceFour,31835Mathlib.Condensed.TopCatAdjunction,27836Mathlib.MeasureTheory.Measure.Haar.DistribChar,11837Mathlib.Tactic.Linter.Lint,3838Mathlib.Algebra.Polynomial.Module.AEval,33839Mathlib.Data.List.Lookmap,13840Mathlib.RingTheory.PowerSeries.Basic,168841Mathlib.Topology.Constructions,265842Mathlib.RingTheory.Valuation.DiscreteValuativeRel,2843Mathlib.CategoryTheory.Enriched.Opposite,13844Mathlib.Algebra.Homology.HomotopyCategory.KProjective,14845Mathlib.RingTheory.TensorProduct.Maps,122846Mathlib.Analysis.Distribution.FourierSchwartz,0847Mathlib.GroupTheory.Order.Min,16848Mathlib.Topology.Category.Profinite.Basic,33849Mathlib.Algebra.Order.Group.Bounds,4850Mathlib.CategoryTheory.Center.Localization,9851Mathlib.AlgebraicGeometry.Sites.Small,21852Mathlib.Analysis.Calculus.FDeriv.Affine,10853Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric,18854Mathlib.Topology.Sober,55855Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv,30856Mathlib.Analysis.RCLike.Lemmas,14857Mathlib.Algebra.Polynomial.Factors,0858Mathlib.MeasureTheory.Measure.MeasureSpace,212859Mathlib.CategoryTheory.Linear.Yoneda,22860Mathlib.SetTheory.Cardinal.Basic,213861Mathlib.Algebra.Star.CHSH,18862Mathlib.Order.Hom.Set,37863Mathlib.Analysis.Convex.LinearIsometry,8864Mathlib.Combinatorics.Tiling.Tile,59865Mathlib.MeasureTheory.Measure.Stieltjes,85866Mathlib.NumberTheory.FLT.Basic,21867Mathlib.Order.JordanHolder,48868Mathlib.NumberTheory.NumberField.DedekindZeta,6869Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra,6870Mathlib.RingTheory.LocalRing.RingHom.Basic,14871Mathlib.CategoryTheory.Limits.Shapes.KernelPair,23872Mathlib.CategoryTheory.ComposableArrows.One,5873Mathlib.CategoryTheory.Monad.Types,13874Mathlib.Dynamics.Ergodic.Action.Regular,4875Mathlib.CategoryTheory.ObjectProperty.Opposite,23876Mathlib.Topology.Algebra.Module.LinearPMap,26877Mathlib.RingTheory.Coalgebra.Basic,94878Mathlib.Algebra.BigOperators.Associated,20879Mathlib.LinearAlgebra.Matrix.SemiringInverse,24880Mathlib.CategoryTheory.Limits.Types.Limits,40881Mathlib.Analysis.Calculus.Deriv.Slope,30882Mathlib.Algebra.Polynomial.BigOperators,40883Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic,20884Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps,1885Mathlib.Analysis.InnerProductSpace.Continuous,7886Mathlib.Topology.Algebra.Module.LinearMapPiProd,70887Mathlib.Algebra.DirectSum.Idempotents,4888Mathlib.RingTheory.OreLocalization.NonZeroDivisors,11889Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy,25890Mathlib.Data.List.Perm.Lattice,7891Mathlib.Lean.PrettyPrinter.Delaborator,4892Mathlib.Algebra.Order.Positive.Ring,25893Mathlib.CategoryTheory.EffectiveEpi.Basic,49894Mathlib.RingTheory.Unramified.Field,7895Mathlib.Data.Nat.GCD.Prime,3896Mathlib.CategoryTheory.Limits.Preserves.Ulift,5897Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap,7898Mathlib.RingTheory.PowerSeries.Ideal,10899Mathlib.RingTheory.Jacobson.Semiprimary,11900Mathlib.RingTheory.Localization.Free,2901Mathlib.CategoryTheory.Sites.CartesianClosed,1902Mathlib.Tactic.Lemma,2903Mathlib.Geometry.Euclidean.Congruence,6904Mathlib.Algebra.Homology.HomologicalComplexBiprod,30905Mathlib.Control.Functor,44906Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory,5907Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc,24908Mathlib.Data.Nat.Init,72909Mathlib.Data.Fintype.Parity,2910Mathlib.Algebra.Group.Submonoid.Membership,115911Mathlib.NumberTheory.ClassNumber.FunctionField,3912Mathlib.Analysis.Convex.Piecewise,4913Mathlib.Order.Hom.Order,23914Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula,134915Mathlib.Algebra.Order.Sub.Unbundled.Basic,57916Mathlib.RingTheory.GradedAlgebra.FiniteType,2917Mathlib.SetTheory.Ordinal.Enum,20918Mathlib.AlgebraicTopology.SimplicialSet.Op,15919Mathlib.LinearAlgebra.Basis.MulOpposite,9920Mathlib.CategoryTheory.Abelian.Basic,99921Mathlib.Geometry.Manifold.StructureGroupoid,56922Mathlib.CategoryTheory.Limits.Shapes.Preorder.Fin,2923Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral,6924Mathlib.Algebra.Order.Monoid.Unbundled.Units,36925Mathlib.Algebra.Category.Ring.Epi,4926Mathlib.Algebra.Order.Module.Field,15927Mathlib.Tactic.ApplyFun,7928Mathlib.Dynamics.FixedPoints.Prufer,2929Mathlib.NumberTheory.Padics.Hensel,3930Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower,20931Mathlib.Data.Nat.Digits.Defs,70932Mathlib.Analysis.Calculus.Deriv.Polynomial,26933Mathlib.Analysis.Normed.Group.HomCompletion,27934Mathlib.Algebra.Azumaya.Matrix,4935Mathlib.Topology.Algebra.Group.AddTorsor,16936Mathlib.GroupTheory.Complement,176937Mathlib.Data.Matrix.Bilinear,22938Mathlib.RingTheory.Finiteness.Ideal,8939Mathlib.Logic.Small.Defs,25940Mathlib.Combinatorics.SetFamily.Compression.UV,30941Mathlib.GroupTheory.Perm.ConjAct,4942Mathlib.Data.Finsupp.MonomialOrder,28943Mathlib.NumberTheory.DirichletCharacter.Orthogonality,8944Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper,10945Mathlib.Analysis.SpecialFunctions.Gamma.Deligne,17946Mathlib.Order.Interval.Finset.Basic,252947Mathlib.FieldTheory.KummerPolynomial,10948Mathlib.Data.ENat.Basic,169949Mathlib.MeasureTheory.Function.L1Space.AEEqFun,38950Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic,40951Mathlib.Analysis.Normed.Unbundled.SeminormFromConst,23952Mathlib.FieldTheory.ChevalleyWarning,5953Mathlib.Order.Monotone.Odd,4954Mathlib.RingTheory.Spectrum.Prime.RingHom,42955Mathlib.Logic.Equiv.Fin.Basic,85956Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant,4957Mathlib.Analysis.Calculus.MeanValue,60958Mathlib.RingTheory.Extension.Cotangent.Basic,68959Mathlib.Tactic.TacticAnalysis.Declarations,37960Mathlib.Algebra.BigOperators.NatAntidiagonal,12961Mathlib.Algebra.Order.Nonneg.Field,24962Mathlib.Data.Set.UnionLift,13963Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated,51964Mathlib.Data.Nat.Sqrt,38965Mathlib.Order.Filter.Cocardinal,17966Mathlib.Order.Restriction,19967Mathlib.AlgebraicGeometry.Morphisms.Immersion,39968Mathlib.Analysis.Polynomial.CauchyBound,10969Mathlib.Order.PartialSups,33970Mathlib.LinearAlgebra.Basis.SMul,19971Mathlib.LinearAlgebra.Basis.Cardinality,5972Mathlib.NumberTheory.Padics.RingHoms,74973Mathlib.CategoryTheory.Closed.FunctorCategory.Groupoid,0974Mathlib.CategoryTheory.Limits.Shapes.Equalizers,280975Mathlib.RingTheory.RingHom.Surjective,6976Mathlib.Topology.Sets.Closeds,152977Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated,87978Mathlib.Algebra.Order.Group.Pointwise.Bounds,50979Mathlib.Algebra.Ring.CharZero,17980Mathlib.Analysis.SpecialFunctions.Log.Base,111981Mathlib.Topology.SeparatedMap,29982Mathlib.LinearAlgebra.QuadraticForm.Dual,16983Mathlib.Data.Nat.Factorial.Cast,1984Mathlib.Data.List.ProdSigma,10985Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive,7986Mathlib.Tactic.Linter.UnusedTacticExtension,4987Mathlib.CategoryTheory.Adhesive,25988Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products,58989Mathlib.Algebra.ContinuedFractions.Basic,54990Mathlib.Combinatorics.Matroid.Rank.Cardinal,61991Mathlib.RingTheory.Kaehler.TensorProduct,29992Mathlib.Topology.Algebra.Module.Determinant,6993Mathlib.Topology.Algebra.Monoid,220994Mathlib.CategoryTheory.Localization.LocallySmall,4995Mathlib.CategoryTheory.Localization.Triangulated,21996Mathlib.RingTheory.WittVector.MulCoeff,23997Mathlib.Algebra.Ring.Action.Pointwise.Finset,4998Mathlib.Data.DFinsupp.Submonoid,9999Mathlib.Analysis.Normed.Module.Span,121000Mathlib.Analysis.Normed.Unbundled.SpectralNorm,671001Mathlib.Analysis.InnerProductSpace.Projection.Reflection,221002Mathlib.Algebra.Polynomial.Degree.CardPowDegree,61003Mathlib.RingTheory.Adjoin.Polynomial,81004Mathlib.CategoryTheory.ObjectProperty.EpiMono,181005Mathlib.RingTheory.Valuation.ExtendToLocalization,31006Mathlib.Analysis.InnerProductSpace.Coalgebra,91007Mathlib.Geometry.Euclidean.NinePointCircle,201008Mathlib.Order.PropInstances,181009Mathlib.RingTheory.PowerBasis,721010Mathlib.Algebra.Order.Sub.Unbundled.Hom,61011Mathlib.Algebra.Group.Units.Equiv,801012Mathlib.RingTheory.LocalRing.Quotient,91013Mathlib.Combinatorics.SimpleGraph.Operations,311014Mathlib.Combinatorics.SimpleGraph.Copy,1121015Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders,101016Mathlib.Topology.Covering,01017Mathlib.Algebra.Ring.Submonoid.Pointwise,411018Mathlib.Analysis.Complex.LocallyUniformLimit,141019Mathlib.Algebra.ModEq,01020Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional,11021Mathlib.CategoryTheory.Sites.Spaces,51022Mathlib.LinearAlgebra.AffineSpace.Slope,281023Mathlib.GroupTheory.Frattini,61024Mathlib.CategoryTheory.Limits.Set,11025Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup,161026Mathlib.Algebra.Group.Subsemigroup.Operations,2321027Mathlib.AlgebraicGeometry.Sites.MorphismProperty,141028Mathlib.LinearAlgebra.Basis.Basic,321029Mathlib.Combinatorics.Matroid.Minor.Contract,921030Mathlib.Topology.Algebra.NonUnitalAlgebra,231031Mathlib.Topology.Metrizable.Real,11032Mathlib.NumberTheory.LSeries.Injectivity,111033Mathlib.Algebra.QuaternionBasis,461034Mathlib.Analysis.Calculus.Deriv.Linear,121035Mathlib.Probability.Density,491036Mathlib.LinearAlgebra.AffineSpace.Ceva,41037Mathlib.Algebra.Homology.Linear,61038Mathlib.Algebra.Category.ModuleCat.AB,61039Mathlib.LinearAlgebra.SymmetricAlgebra.Basis,101040Mathlib.CategoryTheory.Category.Cat.Op,131041Mathlib.Order.Interval.Finset.Defs,2141042Mathlib.Analysis.Calculus.Deriv.Pow,271043Mathlib.AlgebraicGeometry.Limits,1031044Mathlib.CategoryTheory.Subobject.HasCardinalLT,11045Mathlib.CategoryTheory.Monoidal.Braided.Reflection,51046Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver,121047Mathlib.SetTheory.ZFC.VonNeumann,271048Mathlib.Analysis.Real.OfDigits,201049Mathlib.Dynamics.FixedPoints.Basic,301050Mathlib.Algebra.Category.Ring.Basic,1971051Mathlib.Geometry.Euclidean.Sphere.Ptolemy,11052Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings,481053Mathlib.Topology.Algebra.Nonarchimedean.Completion,21054Mathlib.Algebra.Module.LocalizedModule.Away,21055Mathlib.Algebra.Homology.Factorizations.Basic,21056Mathlib.Algebra.Group.Submonoid.MulOpposite,921057Mathlib.MeasureTheory.Group.LIntegral,151058Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems,91059Mathlib.RingTheory.MvPolynomial.Localization,61060Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls,231061Mathlib.AlgebraicGeometry.RationalMap,891062Mathlib.Data.Matrix.Invertible,271063Mathlib.Probability.Kernel.RadonNikodym,701064Mathlib.Tactic.FinCases,41065Mathlib.GroupTheory.Perm.ClosureSwap,111066Mathlib.RingTheory.ClassGroup,461067Mathlib.Algebra.Ring.Action.End,51068Mathlib.Order.PrimeIdeal,361069Mathlib.Data.Finsupp.Notation,131070Mathlib.Algebra.BigOperators.Ring.Finset,491071Mathlib.Topology.MetricSpace.Bilipschitz,31072Mathlib.Combinatorics.Quiver.Cast,191073Mathlib.CategoryTheory.ObjectProperty.LimitsClosure,271074Mathlib.Data.Complex.Cardinality,01075Mathlib.CategoryTheory.Limits.Pi,81076Mathlib.CategoryTheory.Triangulated.Orthogonal,101077Mathlib.Data.Real.Pi.Irrational,01078Mathlib.Control.Random,291079Mathlib.RingTheory.DedekindDomain.AdicValuation,871080Mathlib.Geometry.Euclidean.Angle.Bisector,41081Mathlib.MeasureTheory.OuterMeasure.Defs,171082Mathlib.Analysis.Calculus.FDeriv.Symmetric,351083Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape,441084Mathlib.Analysis.Convex.Continuous,201085Mathlib.Algebra.SkewMonoidAlgebra.Support,141086Mathlib.NumberTheory.Real.Irrational,1191087Mathlib.Data.Nat.BinaryRec,321088Mathlib.Data.Multiset.Replicate,301089Mathlib.CategoryTheory.Functor.EpiMono,581090Mathlib.Algebra.Algebra.Tower,501091Mathlib.MeasureTheory.Measure.ContinuousPreimage,21092Mathlib.LinearAlgebra.Dimension.OrzechProperty,101093Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup,21094Mathlib.Tactic.ToExpr,221095Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart,31096Mathlib.MeasureTheory.Measure.FiniteMeasureProd,231097Mathlib.Topology.UniformSpace.AbstractCompletion,551098Mathlib.Analysis.Calculus.VectorField,781099Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit,351100Mathlib.Algebra.Algebra.Spectrum.Quasispectrum,961101Mathlib.Data.Multiset.Functor,141102Mathlib.Order.WellQuasiOrder,241103Mathlib.Topology.Sheaves.MayerVietoris,71104Mathlib.Geometry.Euclidean.Circumcenter,751105Mathlib.CategoryTheory.Comma.Over.Basic,3911106Mathlib.Algebra.Order.Ring.Ordering.Basic,281107Mathlib.Algebra.Order.Antidiag.Finsupp,121108Mathlib.Algebra.CharP.Lemmas,531109Mathlib.Algebra.Category.HopfAlgCat.Monoidal,181110Mathlib.Order.CompactlyGenerated.Intervals,31111Mathlib.NumberTheory.LSeries.Convergence,141112Mathlib.CategoryTheory.Monoidal.Limits,01113Mathlib.Data.EReal.Basic,1821114Mathlib.Analysis.Normed.Unbundled.FiniteExtension,131115Mathlib.Topology.KrullDimension,61116Mathlib.LinearAlgebra.Contraction,301117Mathlib.Analysis.Calculus.FDeriv.Equiv,781118Mathlib.RingTheory.RingHom.Unramified,101119Mathlib.Data.Tree.Traversable,51120Mathlib.Algebra.Polynomial.GroupRingAction,131121Mathlib.MeasureTheory.Measure.CharacteristicFunction,551122Mathlib.Order.Interval.Set.Infinite,181123Mathlib.Data.NNRat.Lemmas,91124Mathlib.Analysis.Complex.Harmonic.MeanValue,11125Mathlib.Topology.Maps.Basic,1501126Mathlib.Analysis.Convex.Contractible,31127Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects,361128Mathlib.MeasureTheory.Covering.Differentiation,331129Mathlib.Analysis.Complex.UnitDisc.Basic,851130Mathlib.Analysis.SpecialFunctions.Integrability.Basic,201131Mathlib.CategoryTheory.Sites.Hypercover.Zero,2371132Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono,461133Mathlib.Data.Nat.Squarefree,381134Mathlib.Analysis.Normed.Order.UpperLower,281135Mathlib.Algebra.MvPolynomial.Counit,121136Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator,51137Mathlib.Algebra.Homology.Embedding.ExtendHomology,741138Mathlib.CategoryTheory.Adjunction.PartialAdjoint,461139Mathlib.Analysis.Asymptotics.Lemmas,1211140Mathlib.Combinatorics.Quiver.Path.Weight,221141Mathlib.Dynamics.BirkhoffSum.Average,141142Mathlib.LinearAlgebra.Multilinear.Finsupp,51143Mathlib.RingTheory.DedekindDomain.Different,661144Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat,201145Mathlib.Data.Int.CharZero,51146Mathlib.Topology.Piecewise,191147Mathlib.RingTheory.IntegralClosure.Algebra.Defs,61148Mathlib.NumberTheory.NumberField.Ideal.Basic,91149Mathlib.Topology.MetricSpace.Pseudo.Basic,321150Mathlib.Tactic.Linter.Whitespace,41151Mathlib.RingTheory.WittVector.Identities,231152Mathlib.LinearAlgebra.RootSystem.Reduced,311153Mathlib.Order.Radical,41154Mathlib.NumberTheory.LSeries.HurwitzZeta,181155Mathlib.CategoryTheory.Triangulated.Pretriangulated,1171156Mathlib.Analysis.Normed.Operator.Compact,351157Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_,151158Mathlib.Topology.ContinuousMap.Interval,161159Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax,941160Mathlib.Data.Set.Equitable,121161Mathlib.LinearAlgebra.Eigenspace.Zero,121162Mathlib.Combinatorics.Quiver.ReflQuiver,411163Mathlib.Data.Ineq,241164Mathlib.Combinatorics.SimpleGraph.Hamiltonian,391165Mathlib.CategoryTheory.Localization.Bousfield,471166Mathlib.Analysis.Convex.Between,1621167Mathlib.Data.Int.WithZero,101168Mathlib.CategoryTheory.Sites.Point.Category,231169Mathlib.CategoryTheory.Filtered.Flat,21170Mathlib.Data.Fintype.Pigeonhole,41171Mathlib.Algebra.Order.Nonneg.Ring,131172Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings,51173Mathlib.RingTheory.Adjoin.Basic,161174Mathlib.Logic.Equiv.Pairwise,21175Mathlib.RingTheory.Jacobson.Polynomial,21176Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed,81177Mathlib.Topology.Algebra.Group.Quotient,421178Mathlib.ModelTheory.DirectLimit,561179Mathlib.Data.Set.Notation,31180Mathlib.RingTheory.PrincipalIdealDomainOfPrime,31181Mathlib.LinearAlgebra.Finsupp.VectorSpace,271182Mathlib.CategoryTheory.PUnit,121183Mathlib.Data.Finsupp.Fin,151184Mathlib.Lean.Meta.KAbstractPositions,41185Mathlib.Algebra.Polynomial.Monic,811186Mathlib.Algebra.Module.MinimalAxioms,11187Mathlib.SetTheory.Ordinal.Arithmetic,1971188Mathlib.Geometry.Euclidean.Inversion.Calculus,91189Mathlib.Order.Monotone.Basic,1391190Mathlib.MeasureTheory.OuterMeasure.Operations,691191Mathlib.LinearAlgebra.Finsupp.Supported,341192Mathlib.Analysis.Calculus.Rademacher,181193Mathlib.LinearAlgebra.CliffordAlgebra.Prod,141194Mathlib.RingTheory.Norm.Defs,81195Mathlib.CategoryTheory.Subpresheaf.Basic,01196Mathlib.Topology.Algebra.Indicator,81197Mathlib.RingTheory.Localization.BaseChange,311198Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range,121199Mathlib.CategoryTheory.Distributive.Monoidal,451200Mathlib.AlgebraicGeometry.Sites.Etale,5

Showing the first 1,200 of 7566 lines. Download the file for the rest.