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
rootv2moduleedges.csv
edges.csv20883 linesDownload Raw Back to module
1source,target,is_exported2Mathlib.Algebra.Order.Module.Equiv,Mathlib.Algebra.Order.Module.HahnEmbedding,True3Mathlib.Topology.Instances.Sign,Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle,True4Mathlib.Topology.Instances.Sign,Mathlib.Geometry.Euclidean.Incenter,True5Mathlib.LinearAlgebra.Matrix.Determinant.Misc,Mathlib.NumberTheory.NumberField.Units.Regulator,True6Mathlib.LinearAlgebra.Matrix.Stochastic,Mathlib.Analysis.Convex.DoublyStochasticMatrix,True7Mathlib.RingTheory.RingHom.FiniteType,Mathlib.RingTheory.RingHom.FinitePresentation,True8Mathlib.RingTheory.RingHom.FiniteType,Mathlib.AlgebraicGeometry.Morphisms.FiniteType,True9Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic,Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set,True10Mathlib.Logic.Equiv.Functor,Mathlib.RingTheory.FreeCommRing,True11Mathlib.Logic.Equiv.Functor,Mathlib.Order.JordanHolder,True12Mathlib.Logic.Equiv.Functor,Mathlib.Control.ULiftable,True13Mathlib.Topology.IsClosedRestrict,Mathlib,True14Mathlib.Analysis.AbsoluteValue.Equivalence,Mathlib.NumberTheory.Ostrowski,True15Mathlib.Analysis.AbsoluteValue.Equivalence,Mathlib.NumberTheory.NumberField.InfinitePlace.Basic,True16Mathlib.CategoryTheory.Monad.Algebra,Mathlib.CategoryTheory.Monad.Coequalizer,True17Mathlib.CategoryTheory.Monad.Algebra,Mathlib.CategoryTheory.Preadditive.EilenbergMoore,True18Mathlib.CategoryTheory.Monad.Algebra,Mathlib.MeasureTheory.Category.MeasCat,True19Mathlib.CategoryTheory.Monad.Algebra,Mathlib.CategoryTheory.Monad.Equalizer,True20Mathlib.CategoryTheory.Monad.Algebra,Mathlib.CategoryTheory.Monad.Products,True21Mathlib.CategoryTheory.Monad.Algebra,Mathlib.CategoryTheory.Monad.Adjunction,True22Mathlib.Algebra.PEmptyInstances,Mathlib.Algebra.Category.Semigrp.Basic,True23Mathlib.Data.Multiset.Fintype,Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure,True24Mathlib.Data.Multiset.Fintype,Mathlib.Combinatorics.Additive.ErdosGinzburgZiv,True25Mathlib.Data.Multiset.Fintype,Mathlib.RingTheory.Polynomial.IsIntegral,True26Mathlib.Data.Nat.Totient,Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual,True27Mathlib.Data.Nat.Totient,Mathlib.Topology.Instances.AddCircle.Defs,True28Mathlib.Data.Nat.Totient,Mathlib.Data.Nat.PowModTotient,True29Mathlib.Data.Nat.Totient,Mathlib.NumberTheory.PrimeCounting,True30Mathlib.Data.Nat.Totient,Mathlib.GroupTheory.SpecificGroups.Cyclic,True31Mathlib.Data.Nat.Totient,Mathlib.LinearAlgebra.Span.TensorProduct,True32Mathlib.Data.Nat.Totient,Mathlib.Analysis.NormedSpace.HahnBanach.Extension,True33Mathlib.Data.Nat.Totient,Mathlib.Analysis.NormedSpace.HahnBanach.Separation,True34Mathlib.Tactic.FastInstance,Mathlib.Algebra.Order.Positive.Ring,True35Mathlib.Tactic.FastInstance,Mathlib.GroupTheory.Congruence.Defs,True36Mathlib.Tactic.FastInstance,Mathlib.Order.Interval.Lex,True37Mathlib.Tactic.FastInstance,Mathlib.Algebra.Group.Hom.Instances,True38Mathlib.Tactic.FastInstance,Mathlib.Algebra.Order.Interval.Set.Instances,True39Mathlib.Tactic.FastInstance,Mathlib.Algebra.Group.Subsemigroup.Defs,True40Mathlib.Data.Finset.Dedup,Mathlib.Data.Finset.Insert,True41Mathlib.Data.Finset.Dedup,Mathlib.GroupTheory.FreeGroup.Reduce,True42Mathlib.Topology.EMetricSpace.Defs,Mathlib.Topology.MetricSpace.Pseudo.Defs,True43Mathlib.Topology.EMetricSpace.Defs,Mathlib.Topology.EMetricSpace.Basic,True44Mathlib.Topology.EMetricSpace.Defs,Mathlib.Topology.MetricSpace.MetricSeparated,True45Mathlib.Algebra.Polynomial.Div,Mathlib.Algebra.Polynomial.PartialFractions,True46Mathlib.Algebra.Polynomial.Div,Mathlib.Algebra.Polynomial.RingDivision,True47Mathlib.Algebra.Polynomial.Div,Mathlib.Algebra.Polynomial.CoeffMem,True48Mathlib.Algebra.Polynomial.Div,Mathlib.RingTheory.Polynomial.Nilpotent,True49Mathlib.Probability.ProbabilityMassFunction.Binomial,Mathlib,True50Mathlib.RingTheory.Adjoin.PowerBasis,Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots,True51Mathlib.Algebra.Algebra.NonUnitalSubalgebra,Mathlib.Algebra.Star.NonUnitalSubalgebra,True52Mathlib.Algebra.Algebra.NonUnitalSubalgebra,Mathlib.Topology.Algebra.NonUnitalAlgebra,True53Mathlib.Algebra.Algebra.NonUnitalSubalgebra,Mathlib.Algebra.Algebra.Subalgebra.Basic,True54Mathlib.Algebra.GroupWithZero.Action.Basic,Mathlib.Algebra.Ring.AddAut,True55Mathlib.Algebra.GroupWithZero.Action.Basic,Mathlib.Algebra.Module.Equiv.Basic,True56Mathlib.Algebra.GroupWithZero.Action.Basic,Mathlib.Algebra.GroupWithZero.Pointwise.Set.Card,True57Mathlib.Algebra.GroupWithZero.Action.Basic,Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set,True58Mathlib.Algebra.GroupWithZero.Action.Basic,Mathlib.Algebra.Ring.Action.Group,True59Mathlib.Data.PNat.Xgcd,Mathlib,True60Mathlib.Data.Nat.BitIndices,Mathlib.Combinatorics.Colex,True61Mathlib.CategoryTheory.Bicategory.Extension,Mathlib.CategoryTheory.Bicategory.Kan.IsKan,True62Mathlib.RingTheory.Spectrum.Prime.Noetherian,Mathlib.RingTheory.Ideal.Height,True63Mathlib.RingTheory.Spectrum.Prime.Noetherian,Mathlib.RingTheory.HopkinsLevitzki,True64Mathlib.RingTheory.Spectrum.Prime.Noetherian,Mathlib.RingTheory.Spectrum.Prime.Jacobson,True65Mathlib.Combinatorics.SetFamily.KruskalKatona,Mathlib,True66Mathlib.CategoryTheory.Monoidal.Free.Coherence,Mathlib,True67Mathlib.MeasureTheory.MeasurableSpace.Constructions,Mathlib.MeasureTheory.Constructions.SubmoduleQuotient,True68Mathlib.MeasureTheory.MeasurableSpace.Constructions,Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict,True69Mathlib.MeasureTheory.MeasurableSpace.Constructions,Mathlib.MeasureTheory.MeasurableSpace.Embedding,True70Mathlib.MeasureTheory.MeasurableSpace.Constructions,Mathlib.MeasureTheory.MeasurableSpace.Pi,True71Mathlib.MeasureTheory.MeasurableSpace.Constructions,Mathlib.MeasureTheory.Constructions.Cylinders,True72Mathlib.MeasureTheory.MeasurableSpace.Constructions,Mathlib.MeasureTheory.MeasurableSpace.NCard,True73Mathlib.MeasureTheory.MeasurableSpace.Constructions,Mathlib.MeasureTheory.OuterMeasure.Induced,True74Mathlib.MeasureTheory.MeasurableSpace.Constructions,Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated,True75Mathlib.Algebra.Order.CauSeq.Basic,Mathlib.Algebra.Order.CauSeq.BigOperators,True76Mathlib.Algebra.Order.CauSeq.Basic,Mathlib.Algebra.Order.CauSeq.Completion,True77Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff,Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap,True78Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff,Mathlib.LinearAlgebra.Matrix.Charpoly.Univ,True79Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff,Mathlib.LinearAlgebra.Trace,True80Mathlib.Combinatorics.SetFamily.Shadow,Mathlib.Combinatorics.SetFamily.Compression.UV,True81Mathlib.Combinatorics.SetFamily.Shadow,Mathlib.Combinatorics.SetFamily.LYM,True82Mathlib.NumberTheory.LSeries.Deriv,Mathlib.NumberTheory.LSeries.Positivity,True83Mathlib.Analysis.SpecificLimits.Fibonacci,Mathlib,True84Mathlib.Data.PNat.Notation,Mathlib.Data.PNat.Defs,True85Mathlib.Data.PNat.Notation,Mathlib.Dynamics.PeriodicPts.Defs,True86Mathlib.Algebra.Lie.IdealOperations,Mathlib.Algebra.Lie.Abelian,True87Mathlib.Analysis.Convex.Caratheodory,Mathlib,True88Mathlib.Algebra.Order.Group.Indicator,Mathlib.MeasureTheory.OuterMeasure.Operations,True89Mathlib.Algebra.Order.Group.Indicator,Mathlib.NumberTheory.SumPrimeReciprocals,True90Mathlib.Algebra.Order.Group.Indicator,Mathlib.Analysis.Normed.Group.Indicator,True91Mathlib.Algebra.Order.Group.Indicator,Mathlib.Topology.UrysohnsLemma,True92Mathlib.Algebra.Order.Group.Indicator,Mathlib.NumberTheory.Height.Basic,False93Mathlib.Algebra.Order.Group.Indicator,Mathlib.Algebra.Order.Archimedean.IndicatorCard,True94Mathlib.Algebra.Order.Group.Indicator,Mathlib.Topology.Algebra.Order.Support,True95Mathlib.CategoryTheory.Category.Pointed,Mathlib.CategoryTheory.Category.Bipointed,True96Mathlib.CategoryTheory.Category.Pointed,Mathlib.CategoryTheory.Category.PartialFun,True97Mathlib.Data.Real.ENatENNReal,Mathlib.Topology.Algebra.InfiniteSum.ENNReal,True98Mathlib.Data.Real.ENatENNReal,Mathlib.Algebra.Order.Floor.Extended,True99Mathlib.Tactic.ReduceModChar.Ext,Mathlib.Tactic.ReduceModChar,True100Mathlib.Topology.MetricSpace.Contracting,Mathlib.Analysis.ODE.PicardLindelof,True101Mathlib.Algebra.Order.Nonneg.Lattice,Mathlib.Algebra.Order.Nonneg.Ring,True102Mathlib.Condensed.Solid,Mathlib,True103Mathlib.RingTheory.RootsOfUnity.Minpoly,Mathlib.RingTheory.Polynomial.Cyclotomic.Roots,True104Mathlib.RingTheory.RootsOfUnity.Minpoly,Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter,True105Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic,Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim,True106Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic,Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic,True107Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic,Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types,True108Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic,Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected,True109Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic,Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits,True110Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic,Mathlib.CategoryTheory.Sites.Point.Basic,True111Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic,Mathlib.Algebra.Category.Grp.AB,True112Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic,Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory,True113Mathlib.Tactic.CategoryTheory.Elementwise,Mathlib.CategoryTheory.Limits.Types.Products,True114Mathlib.Tactic.CategoryTheory.Elementwise,Mathlib.CategoryTheory.ConcreteCategory.Elementwise,True115Mathlib.Tactic.CategoryTheory.Elementwise,Mathlib.CategoryTheory.Limits.Types.Coproducts,True116Mathlib.Tactic.CategoryTheory.Elementwise,Mathlib.CategoryTheory.Elementwise,True117Mathlib.Tactic.CategoryTheory.Elementwise,Mathlib.CategoryTheory.Limits.Types.Equalizers,True118Mathlib.Tactic.CategoryTheory.Elementwise,Mathlib.CategoryTheory.Limits.Types.Coequalizers,True119Mathlib.Tactic.CategoryTheory.Elementwise,Mathlib.CategoryTheory.Comma.Presheaf.Basic,True120Mathlib.Tactic.CategoryTheory.Elementwise,Mathlib.Tactic,True121Mathlib.Data.Sigma.Basic,Mathlib.Data.Sigma.Order,True122Mathlib.Data.Sigma.Basic,Mathlib.Data.PSigma.Order,True123Mathlib.Data.Sigma.Basic,Mathlib.Algebra.Group.Action.Sigma,True124Mathlib.Data.Sigma.Basic,Mathlib.Logic.Equiv.Sum,True125Mathlib.Data.Sigma.Basic,Mathlib.SetTheory.Lists,True126Mathlib.Data.Sigma.Basic,Mathlib.Data.List.Sigma,True127Mathlib.Data.Sigma.Basic,Mathlib.Tactic.NormNum.Result,True128Mathlib.Algebra.BigOperators.GroupWithZero.Finset,Mathlib.Algebra.BigOperators.Ring.Finset,True129Mathlib.Algebra.BigOperators.GroupWithZero.Finset,Mathlib.Algebra.BigOperators.WithTop,True130Mathlib.Algebra.BigOperators.GroupWithZero.Finset,Mathlib.Algebra.BigOperators.Pi,True131Mathlib.Algebra.BigOperators.GroupWithZero.Finset,Mathlib.GroupTheory.Index,True132Mathlib.Algebra.Polynomial.CoeffList,Mathlib.Algebra.Polynomial.RuleOfSigns,True133Mathlib.FieldTheory.PolynomialGaloisGroup,Mathlib.NumberTheory.Cyclotomic.Gal,True134Mathlib.FieldTheory.PolynomialGaloisGroup,Mathlib.FieldTheory.AbelRuffini,True135Mathlib.FieldTheory.PolynomialGaloisGroup,Mathlib.Analysis.Complex.Polynomial.Basic,True136Mathlib.CategoryTheory.Sites.Monoidal,Mathlib.Condensed.Light.Monoidal,True137Mathlib.Data.Nat.Factorization.Basic,Mathlib.Data.Nat.Totient,True138Mathlib.Data.Nat.Factorization.Basic,Mathlib.Data.Nat.Choose.Factorization,True139Mathlib.Data.Nat.Factorization.Basic,Mathlib.Data.Nat.Squarefree,True140Mathlib.Data.Nat.Factorization.Basic,Mathlib.Data.Nat.Factorization.PrimePow,True141Mathlib.Data.Nat.Factorization.Basic,Mathlib.Data.Nat.Factorization.LCM,True142Mathlib.Data.Nat.Factorization.Basic,Mathlib.Data.ZMod.QuotientRing,True143Mathlib.Data.Nat.Factorization.Basic,Mathlib.Algebra.CharP.LocalRing,True144Mathlib.Analysis.CStarAlgebra.Projection,Mathlib,True145Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties,Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives,True146Mathlib.Order.Filter.AtTopBot.Finset,Mathlib.Topology.Algebra.InfiniteSum.NatInt,True147Mathlib.Order.Filter.AtTopBot.Finset,Mathlib.Topology.Algebra.InfiniteSum.Constructions,True148Mathlib.Order.Filter.AtTopBot.Finset,Mathlib.Topology.Algebra.InfiniteSum.UniformOn,True149Mathlib.Algebra.Ring.Subring.Order,Mathlib.Algebra.Order.Ring.StandardPart,True150Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.HomeomorphBall,True151Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm,True152Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.Normed.Module.MStructure,True153Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual,True154Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.OperatorNorm.Mul,True155Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.Multilinear.Curry,True156Mathlib.Analysis.Normed.Group.Basic,Mathlib.Topology.Compactness.HilbertCubeEmbedding,False157Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.Extr,True158Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.RieszLemma,True159Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.Normed.Module.ENormedSpace,True160Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.Alternating.Curry,True161Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.Normed.Group.Indicator,True162Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.Normed.Order.Hom.Basic,True163Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm,True164Mathlib.Analysis.Normed.Group.Basic,Mathlib.Data.Complex.Norm,True165Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.Normed.Group.CocompactMap,True166Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.OperatorNorm.Basic,True167Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.Normed.Group.Int,True168Mathlib.Analysis.Normed.Group.Basic,Mathlib.Probability.Independence.Kernel.Indep,True169Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.OperatorNorm.Prod,True170Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.MStructure,True171Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness,True172Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.IndicatorFunction,True173Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.SphereNormEquiv,True174Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.Connected,True175Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.Extend,True176Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.SumOverResidueClass,True177Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.ConformalLinearMap,True178Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.Multilinear.Basic,True179Mathlib.Analysis.Normed.Group.Basic,Mathlib.Topology.Algebra.Module.StrongDual,True180Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.Real,True181Mathlib.Analysis.Normed.Group.Basic,Mathlib.Topology.Algebra.Module.TransferInstance,True182Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace,True183Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.Alternating.Uncurry.Fin,True184Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics,True185Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.Normed.Order.Basic,True186Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.HahnBanach.Extension,True187Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.BallAction,True188Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.Alternating.Basic,True189Mathlib.Analysis.Normed.Group.Basic,Mathlib.MeasureTheory.Integral.Lebesgue.Norm,True190Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.Normed.Group.Constructions,True191Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm,True192Mathlib.Analysis.Normed.Group.Basic,Mathlib.NumberTheory.TsumDivsorsAntidiagonal,True193Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.Normalize,True194Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.RCLike,True195Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.FunctionSeries,True196Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.HahnBanach.Separation,True197Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.Normed.Group.Submodule,True198Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.Normed.Group.Subgroup,True199Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.ENormedSpace,True200Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.Normed.Group.Continuity,True201Mathlib.Analysis.Normed.Group.Basic,Mathlib.InformationTheory.Hamming,True202Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.Complex.Norm,True203Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.Int,True204Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.Pointwise,True205Mathlib.Analysis.Normed.Group.Basic,Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear,True206Mathlib.Tactic.Explode,Mathlib.Tactic,True207Mathlib.CategoryTheory.Functor.KanExtension.Dense,Mathlib.CategoryTheory.Presentable.Dense,True208Mathlib.CategoryTheory.Functor.KanExtension.Dense,Mathlib.CategoryTheory.Presentable.StrongGenerator,True209Mathlib.Data.Sigma.Order,Mathlib.Data.Sigma.Interval,True210Mathlib.Algebra.Polynomial.Coeff,Mathlib.Algebra.Polynomial.Degree.Operations,True211Mathlib.Algebra.Polynomial.Coeff,Mathlib.Algebra.Polynomial.Eval.Coeff,True212Mathlib.Algebra.Polynomial.Coeff,Mathlib.Data.Nat.Choose.Vandermonde,True213Mathlib.GroupTheory.Coset.Defs,Mathlib.MeasureTheory.MeasurableSpace.Constructions,True214Mathlib.GroupTheory.Coset.Defs,Mathlib.Combinatorics.Tiling.Tile,True215Mathlib.GroupTheory.Coset.Defs,Mathlib.GroupTheory.QuotientGroup.Defs,True216Mathlib.GroupTheory.Coset.Defs,Mathlib.GroupTheory.Coset.Basic,True217Mathlib.Order.CompleteLattice.Chain,Mathlib.Order.Zorn,True218Mathlib.Topology.Defs.Sequences,Mathlib.Topology.Coherent,True219Mathlib.Topology.Defs.Sequences,Mathlib.Topology.Sequences,True220Mathlib.AlgebraicGeometry.Morphisms.Descent,Mathlib.AlgebraicGeometry.Morphisms.FlatDescent,True221Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal,Mathlib,True222Mathlib.AlgebraicGeometry.ResidueField,Mathlib.AlgebraicGeometry.PullbackCarrier,True223Mathlib.Geometry.RingedSpace.Stalks,Mathlib.Geometry.RingedSpace.SheafedSpace,True224Mathlib.RingTheory.Adjoin.Singleton,Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra,True225Mathlib.MeasureTheory.Measure.Haar.Disintegration,Mathlib.Analysis.Calculus.Rademacher,True226Mathlib.Topology.Algebra.Constructions.DomMulAct,Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous,True227Mathlib.Data.Set.Finite.Lattice,Mathlib.Data.Nat.PrimeFin,True228Mathlib.Data.Set.Finite.Lattice,Mathlib.Algebra.BigOperators.Finprod,True229Mathlib.Data.Set.Finite.Lattice,Mathlib.Order.PartialSups,True230Mathlib.Data.Set.Finite.Lattice,Mathlib.Order.ConditionallyCompleteLattice.Finset,True231Mathlib.Data.Set.Finite.Lattice,Mathlib.Algebra.BigOperators.Ring.Nat,True232Mathlib.Data.Set.Finite.Lattice,Mathlib.CategoryTheory.Sites.Finite,True233Mathlib.Data.Set.Finite.Lattice,Mathlib.Combinatorics.Matroid.IndepAxioms,True234Mathlib.Data.Set.Finite.Lattice,Mathlib.Order.UpperLower.LocallyFinite,True235Mathlib.Data.Set.Finite.Lattice,Mathlib.Order.Atoms.Finite,True236Mathlib.Data.Set.Finite.Lattice,Mathlib.Order.Filter.Finite,True237Mathlib.Data.Set.Finite.Lattice,Mathlib.Order.TeichmullerTukey,True238Mathlib.Data.Set.Finite.Lattice,Mathlib.Data.Set.MemPartition,True239Mathlib.Data.Set.Finite.Lattice,Mathlib.Data.Set.Finite.List,True240Mathlib.Data.Set.Finite.Lattice,Mathlib.SetTheory.Cardinal.Pigeonhole,True241Mathlib.Data.Set.Finite.Lattice,Mathlib.Data.Set.Finite.Monad,True242Mathlib.Computability.Ackermann,Mathlib,True243Mathlib.CategoryTheory.LiftingProperties.Over,Mathlib.AlgebraicTopology.ModelCategory.Over,True244Mathlib.Algebra.BigOperators.RingEquiv,Mathlib.Data.Matrix.Basic,True245Mathlib.Data.Set.SymmDiff,Mathlib.Tactic.TautoSet,True246Mathlib.Data.Set.SymmDiff,Mathlib.Data.Set.Image,True247Mathlib.RingTheory.Nakayama,Mathlib.RingTheory.LocalRing.Quotient,True248Mathlib.RingTheory.Nakayama,Mathlib.RingTheory.Ideal.Cotangent,True249Mathlib.RingTheory.Nakayama,Mathlib.RingTheory.Regular.RegularSequence,True250Mathlib.RingTheory.Nakayama,Mathlib.RingTheory.Support,True251Mathlib.RingTheory.Nakayama,Mathlib.RingTheory.Ideal.KrullsHeightTheorem,True252Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels,Mathlib,True253Mathlib.AlgebraicGeometry.RelativeGluing,Mathlib.AlgebraicGeometry.ColimitsOver,True254Mathlib.CategoryTheory.Limits.Indization.ParallelPair,Mathlib.CategoryTheory.Limits.Indization.Equalizers,True255Mathlib.Topology.ContinuousMap.Lattice,Mathlib.Topology.ContinuousMap.StoneWeierstrass,True256Mathlib.CategoryTheory.Limits.Preserves.Limits,Mathlib.CategoryTheory.Limits.Elements,True257Mathlib.CategoryTheory.Limits.Preserves.Limits,Mathlib.CategoryTheory.Limits.FunctorCategory.Basic,True258Mathlib.Algebra.DirectSum.Internal,Mathlib.RingTheory.GradedAlgebra.Basic,True259Mathlib.Algebra.Star.MonoidHom,Mathlib.Algebra.Star.Unitary,True260Mathlib.RingTheory.IntegralClosure.Algebra.Ideal,Mathlib.RingTheory.IntegralClosure.GoingDown,True261Mathlib.Data.Nat.PrimeFin,Mathlib.Data.Nat.Factorization.Defs,True262Mathlib.Data.Nat.PrimeFin,Mathlib.RingTheory.Radical,True263Mathlib.Data.Nat.PrimeFin,Mathlib.NumberTheory.Divisors,True264Mathlib.RingTheory.Polynomial.Wronskian,Mathlib.RingTheory.Polynomial.Radical,True265Mathlib.Algebra.Homology.HomotopyCategory.MappingCone,Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated,True266Mathlib.Algebra.Homology.HomotopyCategory.MappingCone,Mathlib.Algebra.Homology.Factorizations.CM5b,True267Mathlib.Analysis.InnerProductSpace.CanonicalTensor,Mathlib.Analysis.Distribution.DerivNotation,True268Mathlib.Data.NNReal.Defs,Mathlib.Analysis.Convex.NNReal,True269Mathlib.Data.NNReal.Defs,Mathlib.Data.Int.WithZero,True270Mathlib.Data.NNReal.Defs,Mathlib.Data.NNReal.Star,True271Mathlib.Data.NNReal.Defs,Mathlib.Data.ENNReal.Basic,True272Mathlib.Data.NNReal.Defs,Mathlib.Analysis.Normed.Group.Seminorm,True273Mathlib.Data.NNReal.Defs,Mathlib.RingTheory.Valuation.ValuativeRel.Basic,True274Mathlib.Data.NNReal.Defs,Mathlib.Data.NNReal.Basic,True275Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic,Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro,True276Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic,Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree,True277Mathlib.CategoryTheory.Closed.FunctorToTypes,Mathlib,True278Mathlib.CategoryTheory.Sites.Precoverage,Mathlib.CategoryTheory.Sites.Hypercover.Zero,True279Mathlib.CategoryTheory.Sites.Precoverage,Mathlib.CategoryTheory.Sites.Pretopology,True280Mathlib.CategoryTheory.Sites.Precoverage,Mathlib.CategoryTheory.Sites.JointlySurjective,True281Mathlib.GroupTheory.IsSubnormal,Mathlib,True282Mathlib.FieldTheory.RatFunc.Defs,Mathlib.FieldTheory.RatFunc.Basic,True283Mathlib.Algebra.Ring.Action.ConjAct,Mathlib.Algebra.Star.UnitaryStarAlgAut,True284Mathlib.Algebra.Ring.Action.ConjAct,Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup,True285Mathlib.Algebra.Ring.Action.ConjAct,Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv,True286Mathlib.Algebra.Ring.Action.ConjAct,Mathlib.Analysis.Normed.Algebra.Exponential,True287Mathlib.Algebra.Group.Invertible.Basic,Mathlib.Algebra.Group.Action.Basic,True288Mathlib.Algebra.Group.Invertible.Basic,Mathlib.Algebra.GroupWithZero.Invertible,True289Mathlib.Algebra.Group.Invertible.Basic,Mathlib.Algebra.Group.Center,True290Mathlib.Deprecated.RingHom,Mathlib,True291Mathlib.CategoryTheory.Galois.Topology,Mathlib.CategoryTheory.Galois.EssSurj,True292Mathlib.CategoryTheory.Galois.Topology,Mathlib.CategoryTheory.Galois.IsFundamentalgroup,True293Mathlib.Tactic.CategoryTheory.Coherence.Basic,Mathlib.Tactic.CategoryTheory.Monoidal.Basic,True294Mathlib.Tactic.CategoryTheory.Coherence.Basic,Mathlib.Tactic.CategoryTheory.Bicategory.Basic,True295Mathlib.Analysis.Distribution.Distribution,Mathlib,True296Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure,Mathlib.Analysis.Normed.Unbundled.SpectralNorm,True297Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure,Mathlib.Algebra.Lie.TraceForm,True298Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure,Mathlib.FieldTheory.SeparableDegree,True299Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure,Mathlib.FieldTheory.AbsoluteGaloisGroup,True300Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure,Mathlib.RingTheory.Nilpotent.GeometricallyReduced,True301Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure,Mathlib.RingTheory.Norm.Transitivity,True302Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure,Mathlib.FieldTheory.Differential.Liouville,True303Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure,Mathlib.ModelTheory.Algebra.Field.IsAlgClosed,True304Mathlib.Topology.ContinuousMap.Compact,Mathlib.Topology.ContinuousMap.ContinuousMapZero,True305Mathlib.Topology.ContinuousMap.Compact,Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps,True306Mathlib.Topology.ContinuousMap.Compact,Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap,True307Mathlib.Topology.ContinuousMap.Compact,Mathlib.MeasureTheory.Integral.Bochner.Set,True308Mathlib.Topology.ContinuousMap.Compact,Mathlib.Analysis.CStarAlgebra.ContinuousMap,True309Mathlib.Topology.ContinuousMap.Compact,Mathlib.Topology.MetricSpace.UniformConvergence,True310Mathlib.Topology.ContinuousMap.Compact,Mathlib.Topology.ContinuousMap.Ideals,True311Mathlib.Topology.ContinuousMap.Compact,Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions,True312Mathlib.Topology.ContinuousMap.Compact,Mathlib.Topology.ContinuousMap.Weierstrass,True313Mathlib.Algebra.Category.ModuleCat.Differentials.Basic,Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf,True314Mathlib.SetTheory.Ordinal.NaturalOps,Mathlib.SetTheory.Game.Ordinal,True315Mathlib.CategoryTheory.Monoidal.Bimon_,Mathlib.CategoryTheory.Monoidal.Hopf_,True316Mathlib.Analysis.Calculus.Implicit,Mathlib.Analysis.Calculus.ImplicitContDiff,True317Mathlib.Algebra.Field.GeomSum,Mathlib.Algebra.Order.CauSeq.BigOperators,True318Mathlib.Algebra.Field.GeomSum,Mathlib.Analysis.SpecificLimits.Basic,True319Mathlib.Algebra.Field.GeomSum,Mathlib.Algebra.Order.Field.GeomSum,True320Mathlib.Data.Finset.Insert,Mathlib.Data.Finset.SDiff,True321Mathlib.Data.Finset.Insert,Mathlib.Order.Fin.Finset,True322Mathlib.Data.Finset.Insert,Mathlib.Data.Finset.Range,True323Mathlib.Data.Finset.Insert,Mathlib.Data.Finset.Disjoint,True324Mathlib.Data.Finset.Insert,Mathlib.Data.Set.Constructions,True325Mathlib.Data.Finset.Insert,Mathlib.Data.Finset.Lattice.Lemmas,True326Mathlib.RingTheory.NoetherNormalization,Mathlib,True327Mathlib.Topology.Instances.TrivSqZeroExt,Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt,True328Mathlib.SetTheory.ZFC.Ordinal,Mathlib.SetTheory.ZFC.Class,True329Mathlib.Tactic.CategoryTheory.Monoidal.Basic,Mathlib.CategoryTheory.Monoidal.Rigid.Basic,True330Mathlib.Tactic.CategoryTheory.Monoidal.Basic,Mathlib.CategoryTheory.Monoidal.Braided.Basic,True331Mathlib.Tactic.CategoryTheory.Monoidal.Basic,Mathlib.Tactic,True332Mathlib.Tactic.Linter.DocString,Mathlib.Init,True333Mathlib.RepresentationTheory.Homological.GroupHomology.Basic,Mathlib.RepresentationTheory.Homological.GroupHomology.Shapiro,True334Mathlib.RepresentationTheory.Homological.GroupHomology.Basic,Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree,True335Mathlib.RingTheory.Invariant.Defs,Mathlib.RingTheory.Invariant.Basic,True336Mathlib.Tactic.RewriteSearch,Mathlib.Tactic,True337Mathlib.Analysis.Analytic.WithLp,Mathlib,True338Mathlib.Data.Option.NAry,Mathlib.Data.Seq.Defs,True339Mathlib.Data.Option.NAry,Mathlib.Algebra.Group.WithOne.Map,True340Mathlib.Data.Option.NAry,Mathlib.Order.WithBot,True341Mathlib.Data.Option.NAry,Mathlib.Algebra.GroupWithZero.WithZero,True342Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno,Mathlib.Analysis.Calculus.ContDiff.Basic,True343Mathlib.CategoryTheory.Limits.Preserves.Bifunctor,Mathlib.CategoryTheory.Limits.Sifted,True344Mathlib.Tactic.Generalize,Mathlib.Tactic,True345Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite,Mathlib.Combinatorics.SimpleGraph.FiveWheelLike,True346Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite,Mathlib.Combinatorics.SimpleGraph.ConcreteColorings,True347Mathlib.Algebra.Polynomial.SpecificDegree,Mathlib,True348Mathlib.Topology.Connected.Clopen,Mathlib.Topology.SeparatedMap,True349Mathlib.Topology.Connected.Clopen,Mathlib.Topology.Connected.LocallyConnected,True350Mathlib.Topology.Connected.Clopen,Mathlib.Topology.Separation.Regular,True351Mathlib.Topology.Connected.Clopen,Mathlib.Topology.Connected.TotallyDisconnected,True352Mathlib.Topology.UniformSpace.Completion,Mathlib.Topology.UniformSpace.CompareReals,True353Mathlib.Topology.UniformSpace.Completion,Mathlib.Topology.Algebra.UniformMulAction,True354Mathlib.Topology.UniformSpace.Completion,Mathlib.Topology.UniformSpace.Ultra.Completion,True355Mathlib.Topology.UniformSpace.Completion,Mathlib.Topology.Category.UniformSpace,True356Mathlib.Data.Fintype.Pi,Mathlib.Data.Fin.Tuple.Finset,True357Mathlib.Data.Fintype.Pi,Mathlib.Data.Finite.Prod,True358Mathlib.Data.Fintype.Pi,Mathlib.Order.RelSeries,True359Mathlib.Data.Fintype.Pi,Mathlib.Combinatorics.Additive.Dissociation,True360Mathlib.Data.Fintype.Pi,Mathlib.Data.Fintype.Vector,True361Mathlib.Data.Fintype.Pi,Mathlib.Data.DFinsupp.FiniteInfinite,True362Mathlib.Data.Fintype.Pi,Mathlib.Computability.TuringMachine,True363Mathlib.Data.Fintype.Pi,Mathlib.Algebra.BigOperators.Group.Finset.Pi,True364Mathlib.Data.Fintype.Pi,Mathlib.Combinatorics.Digraph.Basic,True365Mathlib.Analysis.Asymptotics.Theta,Mathlib.Analysis.Complex.Asymptotics,True366Mathlib.Analysis.Asymptotics.Theta,Mathlib.Analysis.Asymptotics.Completion,True367Mathlib.Analysis.Asymptotics.Theta,Mathlib.Analysis.Asymptotics.AsymptoticEquivalent,True368Mathlib.Data.QPF.Multivariate.Constructions.Sigma,Mathlib,True369Mathlib.GroupTheory.Subgroup.Center,Mathlib.Algebra.GroupWithZero.Action.Center,True370Mathlib.GroupTheory.Subgroup.Center,Mathlib.GroupTheory.ClassEquation,True371Mathlib.GroupTheory.Subgroup.Center,Mathlib.GroupTheory.Subgroup.Centralizer,True372Mathlib.GroupTheory.Subgroup.Center,Mathlib.Algebra.Group.Subgroup.Actions,True373Mathlib.Algebra.Central.Defs,Mathlib.Algebra.BrauerGroup.Defs,True374Mathlib.Algebra.Central.Defs,Mathlib.Algebra.Central.Matrix,True375Mathlib.Algebra.Central.Defs,Mathlib.FieldTheory.JacobsonNoether,True376Mathlib.Algebra.Central.Defs,Mathlib.Algebra.Central.Basic,True377Mathlib.Analysis.SpecialFunctions.Exp,Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic,True378Mathlib.Analysis.SpecialFunctions.Exp,Mathlib.Analysis.SpecialFunctions.ExpDeriv,True379Mathlib.Analysis.SpecialFunctions.Exp,Mathlib.Analysis.SpecialFunctions.PolynomialExp,True380Mathlib.Analysis.SpecialFunctions.Exp,Mathlib.Analysis.SpecialFunctions.Log.Basic,True381Mathlib.Algebra.Group.Action.Pointwise.Set.Finite,Mathlib.Combinatorics.Tiling.Tile,True382Mathlib.Algebra.Order.GroupWithZero.WithZero,Mathlib.RingTheory.Valuation.RankOne,True383Mathlib.Data.Multiset.AddSub,Mathlib.Data.Multiset.Replicate,True384Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol,Mathlib.Tactic.NormNum.LegendreSymbol,True385Mathlib.Order.Interval.Set.OrdConnectedLinear,Mathlib.LinearAlgebra.RootSystem.Chain,True386Mathlib.RingTheory.Localization.NormTrace,Mathlib.RingTheory.FractionalIdeal.Norm,True387Mathlib.RingTheory.Localization.NormTrace,Mathlib.NumberTheory.NumberField.Discriminant.Defs,True388Mathlib.RingTheory.Localization.NormTrace,Mathlib.NumberTheory.NumberField.Norm,True389Mathlib.RingTheory.Localization.NormTrace,Mathlib.RingTheory.IntegralClosure.IntegralRestrict,True390Mathlib.Control.Lawful,Mathlib.Control.Monad.Cont,True391Mathlib.Computability.TuringDegree,Mathlib,True392Mathlib.ModelTheory.Skolem,Mathlib.ModelTheory.Satisfiability,True393Mathlib.Tactic.Subsingleton,Mathlib.Order.Filter.AtTopBot.Basic,True394Mathlib.Tactic.Subsingleton,Mathlib.Tactic.Common,True395Mathlib.Tactic.Subsingleton,Mathlib.Algebra.Group.Units.Basic,True396Mathlib.Combinatorics.Matroid.Dual,Mathlib.Combinatorics.Matroid.Minor.Restrict,True397Mathlib.Algebra.Order.BigOperators.Ring.List,Mathlib.Algebra.Order.BigOperators.Ring.Multiset,True398Mathlib.MeasureTheory.Integral.CircleAverage,Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic,True399Mathlib.MeasureTheory.Integral.CircleAverage,Mathlib.Analysis.Complex.MeanValue,True400Mathlib.Util.DischargerAsTactic,Mathlib.Tactic.FieldSimp.Discharger,True401Mathlib.MeasureTheory.Group.Arithmetic,Mathlib.MeasureTheory.Group.Pointwise,True402Mathlib.MeasureTheory.Group.Arithmetic,Mathlib.MeasureTheory.Constructions.BorelSpace.Basic,True403Mathlib.MeasureTheory.Group.Arithmetic,Mathlib.MeasureTheory.Group.MeasurableEquiv,True404Mathlib.MeasureTheory.Group.Arithmetic,Mathlib.MeasureTheory.Order.Group.Lattice,True405Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono,Mathlib.CategoryTheory.Sites.MayerVietorisSquare,True406Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono,Mathlib.CategoryTheory.Presentable.Presheaf,True407Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono,Mathlib.CategoryTheory.Adjunction.Quadruple,True408Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono,Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda,True409Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono,Mathlib.CategoryTheory.Subfunctor.Image,True410Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono,Mathlib.CategoryTheory.Functor.RegularEpi,True411Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono,Mathlib.Algebra.Category.Grp.AB,True412Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono,Mathlib.CategoryTheory.MorphismProperty.FunctorCategory,True413Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap,Mathlib.Analysis.Calculus.DifferentialForm.Basic,True414Mathlib.Topology.MetricSpace.Similarity,Mathlib.Geometry.Euclidean.Similarity,True415Mathlib.CategoryTheory.Monad.Comonadicity,Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Complete,True416Mathlib.CategoryTheory.Monad.Comonadicity,Mathlib.Algebra.Category.ModuleCat.Descent,True417Mathlib.Data.Int.LeastGreatest,Mathlib.Algebra.Order.Floor.Defs,False418Mathlib.Data.Int.LeastGreatest,Mathlib.Data.Int.ConditionallyCompleteOrder,True419Mathlib.Topology.Instances.Discrete,Mathlib.Topology.Instances.Int,True420Mathlib.Topology.Instances.Discrete,Mathlib.Topology.Instances.ENat,True421Mathlib.Topology.Instances.Discrete,Mathlib.Topology.Category.Sequential,True422Mathlib.Algebra.Order.Ring.Archimedean,Mathlib.Algebra.Order.Ring.StandardPart,True423Mathlib.CategoryTheory.Presentable.Adjunction,Mathlib.CategoryTheory.Presentable.OrthogonalReflection,True424Mathlib.CategoryTheory.Limits.Preserves.Creates.Pullbacks,Mathlib.CategoryTheory.Sites.Precoverage,True425Mathlib.GroupTheory.Commutator.Basic,Mathlib.GroupTheory.GroupAction.Quotient,True426Mathlib.GroupTheory.Commutator.Basic,Mathlib.Topology.Algebra.Group.TopologicalAbelianization,True427Mathlib.GroupTheory.Commutator.Basic,Mathlib.GroupTheory.Abelianization.Defs,True428Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real,Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal,True429Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real,Mathlib.MeasureTheory.Measure.Prokhorov,False430Mathlib.RingTheory.Ideal.Colon,Mathlib.RingTheory.SimpleModule.Basic,True431Mathlib.RingTheory.Ideal.Colon,Mathlib.RingTheory.Ideal.Oka,True432Mathlib.RingTheory.Ideal.Colon,Mathlib.RingTheory.IdealFilter.Basic,True433Mathlib.RingTheory.Ideal.Colon,Mathlib.RingTheory.IsPrimary,True434Mathlib.RingTheory.PowerSeries.WellKnown,Mathlib.RingTheory.Polynomial.HilbertPoly,True435Mathlib.RingTheory.PowerSeries.WellKnown,Mathlib.RingTheory.PowerSeries.Binomial,True436Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification,Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex,True437Mathlib.Algebra.Algebra.Hom,Mathlib.LinearAlgebra.TensorProduct.Associator,True438Mathlib.Algebra.Algebra.Hom,Mathlib.Algebra.RingQuot,True439Mathlib.Algebra.Algebra.Hom,Mathlib.Algebra.Algebra.Hom.Rat,True440Mathlib.Algebra.Algebra.Hom,Mathlib.Algebra.Algebra.NonUnitalHom,True441Mathlib.Algebra.Algebra.Hom,Mathlib.Algebra.Algebra.Equiv,True442Mathlib.Algebra.Divisibility.Hom,Mathlib.Data.Nat.Cast.Basic,True443Mathlib.Algebra.Divisibility.Hom,Mathlib.Algebra.Prime.Lemmas,True444Mathlib.Algebra.Divisibility.Hom,Mathlib.Algebra.Ring.Divisibility.Basic,True445Mathlib.CategoryTheory.Core,Mathlib.CategoryTheory.Bicategory.LocallyGroupoid,True446Mathlib.CategoryTheory.ExtremalEpi,Mathlib.CategoryTheory.Generator.StrongGenerator,True447Mathlib.CategoryTheory.ExtremalEpi,Mathlib.CategoryTheory.RegularCategory.Basic,True448Mathlib.CategoryTheory.ObjectProperty.ShiftAdditive,Mathlib,True449Mathlib.Algebra.MvPolynomial.Variables,Mathlib.Algebra.MvPolynomial.Monad,True450Mathlib.Algebra.MvPolynomial.Variables,Mathlib.Algebra.MvPolynomial.SchwartzZippel,True451Mathlib.Algebra.MvPolynomial.Variables,Mathlib.Algebra.MvPolynomial.Supported,True452Mathlib.Algebra.MvPolynomial.Variables,Mathlib.Algebra.MvPolynomial.CommRing,True453Mathlib.Combinatorics.SimpleGraph.Walks.Maps,Mathlib.Combinatorics.SimpleGraph.Walks.Subwalks,True454Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic,Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous,True455Mathlib.InformationTheory.KullbackLeibler.KLFun,Mathlib.InformationTheory.KullbackLeibler.Basic,True456Mathlib.Order.Category.Preord,Mathlib.Order.Category.PartOrd,True457Mathlib.Order.Category.Preord,Mathlib.Topology.Specialization,True458Mathlib.CategoryTheory.Adjunction.Evaluation,Mathlib,True459Mathlib.LinearAlgebra.FreeModule.Determinant,Mathlib.RingTheory.Ideal.Norm.AbsNorm,True460Mathlib.CategoryTheory.Bicategory.LocallyGroupoid,Mathlib,True461Mathlib.Algebra.BigOperators.Finprod,Mathlib.Topology.Algebra.Monoid,True462Mathlib.Algebra.BigOperators.Finprod,Mathlib.RingTheory.Nilpotent.Basic,True463Mathlib.Algebra.BigOperators.Finprod,Mathlib.GroupTheory.ClassEquation,True464Mathlib.Algebra.BigOperators.Finprod,Mathlib.Algebra.BigOperators.GroupWithZero.Action,True465Mathlib.Algebra.BigOperators.Finprod,Mathlib.Data.Setoid.Partition.Card,True466Mathlib.Algebra.BigOperators.Finprod,Mathlib.Topology.Algebra.InfiniteSum.Defs,True467Mathlib.Algebra.BigOperators.Finprod,Mathlib.Data.Set.Card.Arithmetic,True468Mathlib.Algebra.Field.ModEq,Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality,False469Mathlib.AlgebraicGeometry.LimitsOver,Mathlib,True470Mathlib.Algebra.Group.Nat.Defs,Mathlib.Algebra.GroupWithZero.Nat,True471Mathlib.Algebra.Group.Nat.Defs,Mathlib.Algebra.Group.Nat.Even,True472Mathlib.Algebra.Group.Nat.Defs,Mathlib.Data.Int.GCD,True473Mathlib.Algebra.Group.Nat.Defs,Mathlib.Tactic.Sat.FromLRAT,True474Mathlib.Algebra.Group.Nat.Defs,Mathlib.Algebra.FreeMonoid.Basic,True475Mathlib.Algebra.Group.Nat.Defs,Mathlib.Algebra.Group.Nat.Hom,True476Mathlib.Algebra.Group.Nat.Defs,Mathlib.Algebra.Group.Nat.Units,True477Mathlib.Algebra.Group.Nat.Defs,Mathlib.Data.Nat.Size,True478Mathlib.Algebra.Group.Nat.Defs,Mathlib.Algebra.EuclideanDomain.Int,True479Mathlib.Algebra.Group.Nat.Defs,Mathlib.Algebra.Group.Nat.Range,True480Mathlib.Algebra.Group.Nat.Defs,Mathlib.Data.Nat.PSub,True481Mathlib.Algebra.Group.Nat.Defs,Mathlib.Data.Set.Enumerate,True482Mathlib.Algebra.Group.Nat.Defs,Mathlib.Data.Fintype.Perm,True483Mathlib.Algebra.Group.Nat.Defs,Mathlib.Algebra.Homology.HasNoLoop,True484Mathlib.Algebra.Group.Nat.Defs,Mathlib.Computability.Tape,True485Mathlib.Algebra.Group.Nat.Defs,Mathlib.Algebra.Group.Nat.TypeTags,True486Mathlib.Algebra.Group.Nat.Defs,Mathlib.Data.List.SplitLengths,True487Mathlib.Algebra.Group.Nat.Defs,Mathlib.Algebra.Order.Group.Nat,True488Mathlib.Algebra.Group.Nat.Defs,Mathlib.Algebra.Homology.Embedding.Basic,True489Mathlib.Algebra.Group.Nat.Defs,Mathlib.Algebra.Group.Submonoid.Operations,True490Mathlib.Algebra.Group.Nat.Defs,Mathlib.Algebra.Order.Group.Multiset,True491Mathlib.Algebra.Group.Nat.Defs,Mathlib.Algebra.Ring.Rat,True492Mathlib.Algebra.Group.Nat.Defs,Mathlib.Algebra.BigOperators.Group.List.Basic,True493Mathlib.Algebra.Group.Nat.Defs,Mathlib.CategoryTheory.ComposableArrows.Basic,True494Mathlib.Logic.Encodable.Basic,Mathlib.Data.Rat.Encodable,True495Mathlib.Logic.Encodable.Basic,Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas,True496Mathlib.Logic.Encodable.Basic,Mathlib.Logic.Denumerable,True497Mathlib.Logic.Encodable.Basic,Mathlib.Order.SuccPred.LinearLocallyFinite,True498Mathlib.Logic.Encodable.Basic,Mathlib.Order.Ideal,True499Mathlib.Logic.Encodable.Basic,Mathlib.Logic.Encodable.Lattice,True500Mathlib.Logic.Encodable.Basic,Mathlib.Tactic.DeriveEncodable,False501Mathlib.Combinatorics.Additive.SmallTripling,Mathlib.Combinatorics.Additive.ApproximateSubgroup,True502Mathlib.Algebra.BigOperators.ModEq,Mathlib,True503Mathlib.Algebra.Polynomial.PartialFractions,Mathlib,True504Mathlib.CategoryTheory.Products.Basic,Mathlib.CategoryTheory.Products.Bifunctor,True505Mathlib.CategoryTheory.Products.Basic,Mathlib.CategoryTheory.Functor.Currying,True506Mathlib.CategoryTheory.Products.Basic,Mathlib.CategoryTheory.Monoidal.Category,True507Mathlib.CategoryTheory.Products.Basic,Mathlib.CategoryTheory.Products.Associator,True508Mathlib.CategoryTheory.Products.Basic,Mathlib.CategoryTheory.Pi.Basic,True509Mathlib.CategoryTheory.Products.Basic,Mathlib.CategoryTheory.Join.Basic,True510Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point,Mathlib,True511Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization,Mathlib.CategoryTheory.Abelian.FreydMitchell,True512Mathlib.CategoryTheory.Monoidal.Closed.Functor,Mathlib,True513Mathlib.Probability.Moments.Covariance,Mathlib.Probability.Moments.Variance,True514Mathlib.LinearAlgebra.Quotient.Defs,Mathlib.RingTheory.Ideal.Colon,True515Mathlib.LinearAlgebra.Quotient.Defs,Mathlib.GroupTheory.Torsion,True516Mathlib.LinearAlgebra.Quotient.Defs,Mathlib.MeasureTheory.Constructions.SubmoduleQuotient,True517Mathlib.LinearAlgebra.Quotient.Defs,Mathlib.LinearAlgebra.Quotient.Card,True518Mathlib.LinearAlgebra.Quotient.Defs,Mathlib.RingTheory.Finiteness.Basic,True519Mathlib.LinearAlgebra.Quotient.Defs,Mathlib.RingTheory.Ideal.Quotient.Defs,True520Mathlib.LinearAlgebra.Quotient.Defs,Mathlib.LinearAlgebra.Quotient.Basic,True521Mathlib.LinearAlgebra.Quotient.Defs,Mathlib.Topology.Algebra.Module.Basic,True522Mathlib.Algebra.Category.Ring.Under.Basic,Mathlib.Algebra.Category.CommAlgCat.Basic,True523Mathlib.Algebra.Category.Ring.Under.Basic,Mathlib.Algebra.Category.Ring.Under.Limits,True524Mathlib.Data.Prod.TProd,Mathlib.MeasureTheory.MeasurableSpace.Constructions,True525Mathlib.Util.FormatTable,Mathlib,True526Mathlib.Tactic.Linter.TextBased.UnicodeLinter,Mathlib.Tactic.Linter.TextBased,True527Mathlib.Probability.Martingale.Convergence,Mathlib.Probability.Martingale.BorelCantelli,True528Mathlib.Probability.Martingale.Convergence,Mathlib.Probability.Kernel.Disintegration.Density,True529Mathlib.Analysis.Normed.Module.RCLike.Basic,Mathlib.Analysis.Calculus.UniformLimitsDeriv,True530Mathlib.Analysis.Normed.Module.RCLike.Basic,Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional,True531Mathlib.Analysis.Normed.Module.RCLike.Basic,Mathlib.Analysis.Complex.Tietze,True532Mathlib.Analysis.Normed.Module.RCLike.Basic,Mathlib.Analysis.Normed.Module.Dual,True533Mathlib.Algebra.Module.Card,Mathlib.Topology.Algebra.Module.Cardinality,True534Mathlib.MeasureTheory.Function.ConvergenceInMeasure,Mathlib.MeasureTheory.Function.LpOrder,True535Mathlib.CategoryTheory.Abelian.Projective.Basic,Mathlib.CategoryTheory.Abelian.Yoneda,True536Mathlib.LinearAlgebra.FiniteDimensional.Lemmas,Mathlib.Algebra.Category.ModuleCat.Simple,True537Mathlib.LinearAlgebra.FiniteDimensional.Lemmas,Mathlib.RingTheory.LocalRing.Module,True538Mathlib.LinearAlgebra.FiniteDimensional.Lemmas,Mathlib.Analysis.InnerProductSpace.Orthonormal,True539Mathlib.LinearAlgebra.FiniteDimensional.Lemmas,Mathlib.Algebra.Module.Lattice,True540Mathlib.LinearAlgebra.FiniteDimensional.Lemmas,Mathlib.LinearAlgebra.Eigenspace.Basic,True541Mathlib.LinearAlgebra.FiniteDimensional.Lemmas,Mathlib.RingTheory.SimpleModule.Rank,True542Mathlib.LinearAlgebra.FiniteDimensional.Lemmas,Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional,True543Mathlib.LinearAlgebra.FiniteDimensional.Lemmas,Mathlib.Topology.Instances.Complex,True544Mathlib.LinearAlgebra.FiniteDimensional.Lemmas,Mathlib.LinearAlgebra.QuadraticForm.Basic,True545Mathlib.LinearAlgebra.FiniteDimensional.Lemmas,Mathlib.LinearAlgebra.Dual.Lemmas,True546Mathlib.CategoryTheory.Monoidal.Closed.Basic,Mathlib.CategoryTheory.Monoidal.Closed.Functor,True547Mathlib.CategoryTheory.Monoidal.Closed.Basic,Mathlib.CategoryTheory.Category.Cat.CartesianClosed,True548Mathlib.CategoryTheory.Monoidal.Closed.Basic,Mathlib.CategoryTheory.Monoidal.Braided.Reflection,True549Mathlib.CategoryTheory.Monoidal.Closed.Basic,Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed,True550Mathlib.CategoryTheory.Monoidal.Closed.Basic,Mathlib.CategoryTheory.Distributive.Monoidal,True551Mathlib.CategoryTheory.Monoidal.Closed.Basic,Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes,True552Mathlib.CategoryTheory.Monoidal.Closed.Basic,Mathlib.CategoryTheory.Monoidal.Closed.Enrichment,True553Mathlib.CategoryTheory.Monoidal.Closed.Basic,Mathlib.CategoryTheory.Preadditive.Projective.Internal,True554Mathlib.CategoryTheory.Monoidal.Closed.Basic,Mathlib.CategoryTheory.LocallyCartesianClosed.Sections,True555Mathlib.CategoryTheory.Monoidal.Closed.Basic,Mathlib.CategoryTheory.Monoidal.Subcategory,True556Mathlib.CategoryTheory.Monoidal.Closed.Basic,Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid,True557Mathlib.CategoryTheory.Monoidal.Closed.Basic,Mathlib.CategoryTheory.Monoidal.Closed.Cartesian,True558Mathlib.CategoryTheory.Monoidal.Closed.Basic,Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed,True559Mathlib.CategoryTheory.Monoidal.Closed.Basic,Mathlib.CategoryTheory.Monoidal.Closed.Transport,True560Mathlib.CategoryTheory.Monoidal.Closed.Basic,Mathlib.CategoryTheory.Pi.Monoidal,True561Mathlib.CategoryTheory.Monoidal.Closed.Basic,Mathlib.CategoryTheory.Monoidal.Rigid.Basic,True562Mathlib.Data.PFunctor.Multivariate.W,Mathlib.Data.QPF.Multivariate.Constructions.Fix,True563Mathlib.Analysis.SpecialFunctions.Integrals.LogTrigonometric,Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage,True564Mathlib.Topology.Algebra.IsUniformGroup.Basic,Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete,True565Mathlib.Topology.Algebra.IsUniformGroup.Basic,Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup,True566Mathlib.Topology.Algebra.IsUniformGroup.Basic,Mathlib.Topology.Instances.ZMultiples,True567Mathlib.Topology.Algebra.IsUniformGroup.Basic,Mathlib.Topology.Instances.AddCircle.Defs,True568Mathlib.Topology.Algebra.IsUniformGroup.Basic,Mathlib.Topology.Algebra.UniformRing,True569Mathlib.Topology.Algebra.IsUniformGroup.Basic,Mathlib.Analysis.Normed.Group.Uniform,True570Mathlib.Topology.Algebra.IsUniformGroup.Basic,Mathlib.Analysis.Convex.TotallyBounded,True571Mathlib.Dynamics.Transitive,Mathlib,True572Mathlib.Algebra.GroupWithZero.Equiv,Mathlib.Algebra.Field.Equiv,True573Mathlib.Algebra.GroupWithZero.Equiv,Mathlib.Algebra.Prime.Lemmas,True574Mathlib.Algebra.GroupWithZero.Equiv,Mathlib.Algebra.Ring.Equiv,True575Mathlib.Algebra.GroupWithZero.Equiv,Mathlib.Algebra.GroupWithZero.WithZero,True576Mathlib.Topology.Category.CompHaus.Projective,Mathlib.Topology.Category.Stonean.Basic,True577Mathlib.Algebra.GroupWithZero.Nat,Mathlib.Combinatorics.SimpleGraph.Hamiltonian,True578Mathlib.Algebra.GroupWithZero.Nat,Mathlib.Order.RelSeries,True579Mathlib.Algebra.GroupWithZero.Nat,Mathlib.Data.Nat.GCD.Basic,True580Mathlib.Algebra.GroupWithZero.Nat,Mathlib.Data.Nat.Prime.Defs,True581Mathlib.Algebra.GroupWithZero.Nat,Mathlib.Algebra.GCDMonoid.Nat,True582Mathlib.Algebra.GroupWithZero.Nat,Mathlib.Algebra.Ring.Nat,True583Mathlib.Algebra.GroupWithZero.Nat,Mathlib.Data.Int.NatAbs,True584Mathlib.FieldTheory.PurelyInseparable.Exponent,Mathlib,True585Mathlib.GroupTheory.GroupAction.Quotient,Mathlib.Algebra.Polynomial.GroupRingAction,True586Mathlib.GroupTheory.GroupAction.Quotient,Mathlib.Topology.Algebra.Group.Quotient,True587Mathlib.GroupTheory.GroupAction.Quotient,Mathlib.LinearAlgebra.Alternating.DomCoprod,True588Mathlib.GroupTheory.GroupAction.Quotient,Mathlib.GroupTheory.Index,True589Mathlib.GroupTheory.GroupAction.Quotient,Mathlib.CategoryTheory.Action.Concrete,True590Mathlib.GroupTheory.GroupAction.Quotient,Mathlib.GroupTheory.GroupAction.CardCommute,True591Mathlib.GroupTheory.GroupAction.Quotient,Mathlib.LinearAlgebra.Projectivization.Cardinality,True592Mathlib.Topology.Algebra.MetricSpace.Lipschitz,Mathlib.Analysis.SpecialFunctions.Exp,True593Mathlib.Topology.Algebra.MetricSpace.Lipschitz,Mathlib.Topology.MetricSpace.PiNat,True594Mathlib.Topology.Algebra.MetricSpace.Lipschitz,Mathlib.Analysis.Normed.Module.Multilinear.Basic,True595Mathlib.Probability.Kernel.MeasurableLIntegral,Mathlib.Probability.Kernel.Composition.ParallelComp,True596Mathlib.Probability.Kernel.MeasurableLIntegral,Mathlib.Probability.Kernel.MeasurableIntegral,True597Mathlib.Probability.Kernel.MeasurableLIntegral,Mathlib.Probability.Kernel.Composition.Comp,True598Mathlib.Probability.Kernel.MeasurableLIntegral,Mathlib.Probability.Kernel.WithDensity,True599Mathlib.Topology.Instances.RealVectorSpace,Mathlib.Analysis.RCLike.Lemmas,True600Mathlib.Topology.Instances.RealVectorSpace,Mathlib.Analysis.Calculus.MeanValue,True601Mathlib.Topology.Instances.RealVectorSpace,Mathlib.Analysis.Complex.Basic,True602Mathlib.Topology.Instances.RealVectorSpace,Mathlib.Analysis.RCLike.TangentCone,True603Mathlib.Topology.Instances.RealVectorSpace,Mathlib.Analysis.Normed.Affine.MazurUlam,True604Mathlib.Topology.Instances.RealVectorSpace,Mathlib.Analysis.Normed.Affine.AddTorsor,True605Mathlib.RingTheory.Unramified.Locus,Mathlib.RingTheory.RingHom.Unramified,True606Mathlib.RingTheory.Unramified.Locus,Mathlib.RingTheory.Frobenius,True607Mathlib.RingTheory.Unramified.Locus,Mathlib.RingTheory.Unramified.LocalRing,True608Mathlib.RingTheory.Unramified.Locus,Mathlib.RingTheory.Etale.Locus,True609Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody,Mathlib.NumberTheory.NumberField.Discriminant.Basic,True610Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody,Mathlib.NumberTheory.NumberField.Units.DirichletTheorem,True611Mathlib.CategoryTheory.Sites.CompatibleSheafification,Mathlib.CategoryTheory.Sites.PreservesSheafification,True612Mathlib.Data.List.Destutter,Mathlib.Algebra.Polynomial.RuleOfSigns,True613Mathlib.Topology.Category.CompactlyGenerated,Mathlib.Condensed.TopCatAdjunction,True614Mathlib.Algebra.GroupWithZero.Divisibility,Mathlib.Algebra.GroupWithZero.Submonoid.Primal,True615Mathlib.Algebra.GroupWithZero.Divisibility,Mathlib.Algebra.BigOperators.Ring.List,True616Mathlib.Algebra.GroupWithZero.Divisibility,Mathlib.SetTheory.Ordinal.Arithmetic,True617Mathlib.Algebra.GroupWithZero.Divisibility,Mathlib.Data.Rat.Lemmas,True618Mathlib.Algebra.GroupWithZero.Divisibility,Mathlib.Data.Nat.GCD.Basic,True619Mathlib.Algebra.GroupWithZero.Divisibility,Mathlib.Algebra.EuclideanDomain.Basic,True620Mathlib.Algebra.GroupWithZero.Divisibility,Mathlib.Data.PNat.Basic,True621Mathlib.Algebra.GroupWithZero.Divisibility,Mathlib.Algebra.Prime.Defs,True622Mathlib.Analysis.Convolution,Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension,True623Mathlib.Analysis.Convolution,Mathlib.Analysis.SpecialFunctions.Gamma.Beta,True624Mathlib.MeasureTheory.Measure.DiracProba,Mathlib,True625Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating,Mathlib.Algebra.ContinuedFractions.Computation.Approximations,True626Mathlib.Algebra.Star.NonUnitalSubalgebra,Mathlib.Algebra.Star.Subalgebra,True627Mathlib.Algebra.Star.NonUnitalSubalgebra,Mathlib.Topology.Algebra.NonUnitalStarAlgebra,True628Mathlib.Algebra.Star.NonUnitalSubalgebra,Mathlib.Algebra.Algebra.Unitization,True629Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap,Mathlib.RingTheory.IntegralClosure.Algebra.Basic,True630Mathlib.ModelTheory.Ultraproducts,Mathlib.ModelTheory.Satisfiability,True631Mathlib.MeasureTheory.Function.ConvergenceInDistribution,Mathlib,True632Mathlib.Analysis.Calculus.FDeriv.Comp,Mathlib.Analysis.Calculus.FDeriv.Prod,True633Mathlib.Analysis.Calculus.FDeriv.Comp,Mathlib.Analysis.Calculus.Deriv.Comp,True634Mathlib.Analysis.Calculus.FDeriv.Comp,Mathlib.Analysis.Calculus.FDeriv.Add,True635Mathlib.RingTheory.Valuation.Basic,Mathlib.Algebra.Order.Ring.Archimedean,True636Mathlib.RingTheory.Valuation.Basic,Mathlib.NumberTheory.Padics.PadicNumbers,True637Mathlib.RingTheory.Valuation.Basic,Mathlib.RingTheory.Valuation.ExtendToLocalization,True638Mathlib.RingTheory.Valuation.Basic,Mathlib.RingTheory.HahnSeries.Valuation,True639Mathlib.RingTheory.Valuation.Basic,Mathlib.RingTheory.Valuation.Minpoly,True640Mathlib.RingTheory.Valuation.Basic,Mathlib.RingTheory.Valuation.Integers,True641Mathlib.RingTheory.Valuation.Basic,Mathlib.RingTheory.Valuation.Quotient,True642Mathlib.RingTheory.Valuation.Basic,Mathlib.RingTheory.Valuation.ValuativeRel.Basic,True643Mathlib.RingTheory.Valuation.Basic,Mathlib.RingTheory.Valuation.FiniteField,True644Mathlib.RingTheory.Valuation.Basic,Mathlib.RingTheory.Valuation.PrimeMultiplicity,True645Mathlib.CategoryTheory.Comma.Over.OverClass,Mathlib.AlgebraicGeometry.Over,True646Mathlib.Algebra.Group.Pointwise.Set.Scalar,Mathlib.Algebra.Group.Action.Pointwise.Set.Finite,True647Mathlib.Algebra.Group.Pointwise.Set.Scalar,Mathlib.Algebra.Order.Group.Pointwise.Interval,True648Mathlib.Algebra.Group.Pointwise.Set.Scalar,Mathlib.Algebra.Group.Pointwise.Set.Lattice,True649Mathlib.Algebra.Group.Pointwise.Set.Scalar,Mathlib.GroupTheory.GroupAction.Pointwise,True650Mathlib.Algebra.Group.Pointwise.Set.Scalar,Mathlib.Algebra.Group.Pointwise.Set.Finite,True651Mathlib.Algebra.Group.Pointwise.Set.Scalar,Mathlib.Algebra.AddTorsor.Basic,True652Mathlib.Algebra.Group.Pointwise.Set.Scalar,Mathlib.Algebra.Module.PointwisePi,True653Mathlib.Algebra.Group.Pointwise.Set.Scalar,Mathlib.Algebra.GroupWithZero.Pointwise.Set.Card,True654Mathlib.Algebra.Group.Pointwise.Set.Scalar,Mathlib.Combinatorics.Additive.AP.Three.Defs,True655Mathlib.Algebra.Group.Pointwise.Set.Scalar,Mathlib.RingTheory.Localization.Integer,True656Mathlib.Algebra.Group.Pointwise.Set.Scalar,Mathlib.Algebra.Order.Field.Pointwise,True657Mathlib.Algebra.Group.Pointwise.Set.Scalar,Mathlib.Algebra.Group.Action.Pointwise.Set.Basic,True658Mathlib.Algebra.Group.Pointwise.Set.Scalar,Mathlib.GroupTheory.GroupAction.Defs,True659Mathlib.Algebra.Group.Pointwise.Set.Scalar,Mathlib.Algebra.Order.Module.Pointwise,True660Mathlib.Algebra.Group.Pointwise.Set.Scalar,Mathlib.GroupTheory.GroupAction.Support,True661Mathlib.Algebra.Group.Pointwise.Set.Scalar,Mathlib.Data.Finset.SMulAntidiagonal,True662Mathlib.Data.PEquiv,Mathlib.Data.Matrix.PEquiv,True663Mathlib.Algebra.Category.ModuleCat.Limits,Mathlib.Algebra.Category.AlgCat.Limits,True664Mathlib.Algebra.Category.ModuleCat.Limits,Mathlib.Algebra.Category.ModuleCat.Abelian,True665Mathlib.Algebra.Category.ModuleCat.Limits,Mathlib.Algebra.Category.FGModuleCat.Limits,True666Mathlib.Algebra.Category.ModuleCat.Limits,Mathlib.RepresentationTheory.Rep,True667Mathlib.Algebra.Category.ModuleCat.Limits,Mathlib.Algebra.Category.ModuleCat.ChangeOfRings,True668Mathlib.Algebra.Category.ModuleCat.Limits,Mathlib.Algebra.Category.ModuleCat.Topology.Basic,True669Mathlib.RingTheory.WittVector.Frobenius,Mathlib.RingTheory.WittVector.Identities,True670Mathlib.RingTheory.QuotSMulTop,Mathlib.RingTheory.Regular.IsSMulRegular,True671Mathlib.RingTheory.QuotSMulTop,Mathlib.RingTheory.Regular.Category,True672Mathlib.RingTheory.QuotSMulTop,Mathlib.RingTheory.Support,True673Mathlib.Algebra.Group.Pointwise.Finset.Scalar,Mathlib.RingTheory.Finiteness.Ideal,True674Mathlib.Algebra.Group.Pointwise.Finset.Scalar,Mathlib.Algebra.Ring.Action.Pointwise.Finset,True675Mathlib.Algebra.Group.Pointwise.Finset.Scalar,Mathlib.Algebra.Group.Action.Pointwise.Finset,True676Mathlib.Algebra.Group.Pointwise.Finset.Scalar,Mathlib.NumberTheory.FactorisationProperties,True677Mathlib.Algebra.Group.Pointwise.Finset.Scalar,Mathlib.Algebra.Order.Antidiag.Pi,True678Mathlib.Algebra.Group.Pointwise.Finset.Scalar,Mathlib.Combinatorics.Additive.CovBySMul,True679Mathlib.Algebra.Group.Pointwise.Finset.Scalar,Mathlib.Combinatorics.Additive.SubsetSum,True680Mathlib.Algebra.Category.CommAlgCat.FiniteType,Mathlib,True681Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic,Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels,True682Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic,Mathlib.CategoryTheory.Sites.Precoverage,True683Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic,Mathlib.CategoryTheory.Limits.Types.Pushouts,True684Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic,Mathlib.CategoryTheory.Limits.Shapes.KernelPair,True685Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic,Mathlib.AlgebraicTopology.SimplicialSet.HornColimits,True686Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic,Mathlib.CategoryTheory.Subobject.Basic,True687Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic,Mathlib.CategoryTheory.Monoidal.Cartesian.Over,True688Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic,Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered,True689Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic,Mathlib.Algebra.Category.Ring.Constructions,True690Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic,Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq,True691Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic,Mathlib.CategoryTheory.Limits.FormalCoproducts,True692Mathlib.Analysis.CStarAlgebra.Unitary.Connected,Mathlib,True693Mathlib.RingTheory.Smooth.StandardSmoothCotangent,Mathlib.RingTheory.Extension.Cotangent.LocalizationAway,True694Mathlib.RingTheory.Smooth.StandardSmoothCotangent,Mathlib.RingTheory.Polynomial.UniversalFactorizationRing,True695Mathlib.CategoryTheory.Sites.Hypercover.One,Mathlib.CategoryTheory.Sites.Hypercover.Homotopy,True696Mathlib.CategoryTheory.Sites.Hypercover.One,Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf,True697Mathlib.CategoryTheory.Sites.Hypercover.One,Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical,True698Mathlib.Geometry.Manifold.VectorBundle.Pullback,Mathlib,True699Mathlib.LinearAlgebra.QuadraticForm.Real,Mathlib,True700Mathlib.RingTheory.FreeCommRing,Mathlib.ModelTheory.Algebra.Ring.FreeCommRing,True701Mathlib.RingTheory.FreeCommRing,Mathlib.RingTheory.MvPolynomial.FreeCommRing,True702Mathlib.RingTheory.FreeCommRing,Mathlib.SetTheory.Cardinal.Free,True703Mathlib.RingTheory.FreeCommRing,Mathlib.Algebra.Colimit.Ring,True704Mathlib.CategoryTheory.Idempotents.Karoubi,Mathlib.CategoryTheory.Idempotents.FunctorCategories,True705Mathlib.CategoryTheory.Idempotents.Karoubi,Mathlib.CategoryTheory.Idempotents.HomologicalComplex,True706Mathlib.CategoryTheory.Idempotents.Karoubi,Mathlib.CategoryTheory.Idempotents.Biproducts,True707Mathlib.CategoryTheory.Idempotents.Karoubi,Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi,True708Mathlib.CategoryTheory.Idempotents.Karoubi,Mathlib.CategoryTheory.Idempotents.FunctorExtension,True709Mathlib.Topology.Hom.Open,Mathlib,True710Mathlib.Algebra.MvPolynomial.Invertible,Mathlib.RingTheory.WittVector.Basic,True711Mathlib.RingTheory.Morita.Matrix,Mathlib,True712Mathlib.CategoryTheory.Retract,Mathlib.CategoryTheory.ObjectProperty.Retract,True713Mathlib.CategoryTheory.Retract,Mathlib.CategoryTheory.MorphismProperty.Retract,True714Mathlib.CategoryTheory.Retract,Mathlib.CategoryTheory.LiftingProperties.Basic,True715Mathlib.Topology.Algebra.Star.Real,Mathlib.Topology.ContinuousMap.StoneWeierstrass,True716Mathlib.Topology.Algebra.Star.Real,Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital,True717Mathlib.AlgebraicGeometry.Morphisms.Integral,Mathlib.AlgebraicGeometry.Morphisms.Finite,True718Mathlib.AlgebraicGeometry.Morphisms.Integral,Mathlib.AlgebraicGeometry.Normalization,True719Mathlib.Topology.ContinuousOn,Mathlib.Topology.OpenPartialHomeomorph.Defs,True720Mathlib.Topology.ContinuousOn,Mathlib.Topology.Piecewise,True721Mathlib.Topology.ContinuousOn,Mathlib.Topology.UniformSpace.Basic,True722Mathlib.Topology.ContinuousOn,Mathlib.Topology.Clopen,True723Mathlib.Topology.ContinuousOn,Mathlib.Topology.Inseparable,True724Mathlib.Topology.ContinuousOn,Mathlib.Topology.LocallyFinite,True725Mathlib.Topology.ContinuousOn,Mathlib.Topology.Coherent,True726Mathlib.Topology.ContinuousOn,Mathlib.Topology.Compactness.Compact,True727Mathlib.Topology.ContinuousOn,Mathlib.Topology.Order.LeftRight,True728Mathlib.Topology.ContinuousOn,Mathlib.Topology.Order.LocalExtr,True729Mathlib.Topology.ContinuousOn,Mathlib.Topology.Semicontinuity.Defs,False730Mathlib.Tactic.Basic,Mathlib.Control.Lawful,True731Mathlib.Tactic.Basic,Mathlib.Data.Nat.Init,True732Mathlib.Tactic.Basic,Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Note,True733Mathlib.Tactic.Basic,Mathlib.Tactic.Says,True734Mathlib.Tactic.Basic,Mathlib.Tactic.Ext,True735Mathlib.Tactic.Basic,Mathlib.Tactic.Widget.CongrM,True736Mathlib.Tactic.Basic,Mathlib.Data.String.Lemmas,True737Mathlib.Tactic.Basic,Mathlib.Logic.Basic,True738Mathlib.Tactic.Basic,Mathlib.Algebra.HierarchyDesign,True739Mathlib.Tactic.Basic,Mathlib.Tactic.Widget.GCongr,True740Mathlib.Tactic.Basic,Mathlib.Tactic.Simps.Basic,True741Mathlib.Tactic.Basic,Mathlib.Tactic.SetLike,True742Mathlib.Tactic.Basic,Mathlib.Tactic.RSuffices,True743Mathlib.Tactic.Basic,Mathlib.Tactic.Lift,True744Mathlib.Tactic.Basic,Mathlib.Tactic.ArithMult,True745Mathlib.Tactic.Basic,Mathlib.Deprecated.Order,True746Mathlib.Tactic.Basic,Mathlib.Algebra.Order.Field.Defs,True747Mathlib.Tactic.Basic,Mathlib.Tactic.Hint,True748Mathlib.Tactic.Basic,Mathlib.Tactic.DefEqTransformations,True749Mathlib.NumberTheory.NumberField.Discriminant.Basic,Mathlib.NumberTheory.NumberField.Discriminant.Different,True750Mathlib.NumberTheory.NumberField.Discriminant.Basic,Mathlib.NumberTheory.NumberField.ClassNumber,True751Mathlib.FieldTheory.IsPerfectClosure,Mathlib,True752Mathlib.Data.Pi.Interval,Mathlib.NumberTheory.MahlerMeasure,True753Mathlib.Data.Pi.Interval,Mathlib.NumberTheory.SiegelsLemma,True754Mathlib.Data.Pi.Interval,Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic,False755Mathlib.Algebra.Homology.Embedding.TruncLEHomology,Mathlib.Algebra.Homology.Embedding.AreComplementary,True756Mathlib.Data.Analysis.Filter,Mathlib.Data.Analysis.Topology,True757Mathlib.NumberTheory.ArithmeticFunction.Misc,Mathlib.NumberTheory.Cyclotomic.Three,True758Mathlib.NumberTheory.ArithmeticFunction.Misc,Mathlib.NumberTheory.Cyclotomic.Embeddings,True759Mathlib.NumberTheory.ArithmeticFunction.Misc,Mathlib.NumberTheory.Cyclotomic.Rat,True760Mathlib.NumberTheory.ArithmeticFunction.Misc,Mathlib.NumberTheory.ArithmeticFunction.Moebius,True761Mathlib.NumberTheory.ArithmeticFunction.Misc,Mathlib.NumberTheory.VonMangoldt,True762Mathlib.NumberTheory.ArithmeticFunction.Misc,Mathlib.NumberTheory.Cyclotomic.PID,True763Mathlib.NumberTheory.ArithmeticFunction.Misc,Mathlib.Algebra.Order.Antidiag.Nat,True764Mathlib.NumberTheory.ArithmeticFunction.Misc,Mathlib.NumberTheory.TsumDivsorsAntidiagonal,True765Mathlib.NumberTheory.ArithmeticFunction.Misc,Mathlib.NumberTheory.TsumDivisorsAntidiagonal,True766Mathlib.NumberTheory.LSeries.ZMod,Mathlib.NumberTheory.LSeries.DirichletContinuation,True767Mathlib.LinearAlgebra.TensorProduct.Associator,Mathlib.RingTheory.Coalgebra.Basic,True768Mathlib.LinearAlgebra.TensorProduct.Associator,Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic,True769Mathlib.LinearAlgebra.TensorProduct.Associator,Mathlib.LinearAlgebra.TensorProduct.Tower,True770Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan,Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan,True771Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan,Mathlib.Data.Real.Pi.Bounds,True772Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan,Mathlib.Data.Real.Pi.Irrational,True773Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan,Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn,True774Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan,Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle,True775Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan,Mathlib.Data.Real.Pi.Leibniz,True776Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan,Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv,True777Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan,Mathlib.Analysis.Real.Pi.Chudnovsky,True778Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan,Mathlib.Data.Real.Pi.Wallis,True779Mathlib.Algebra.Category.ModuleCat.Basic,Mathlib.Algebra.Category.ModuleCat.Limits,True780Mathlib.Algebra.Category.ModuleCat.Basic,Mathlib.Algebra.Category.CoalgCat.Basic,True781Mathlib.Algebra.Category.ModuleCat.Basic,Mathlib.Algebra.Category.AlgCat.Basic,True782Mathlib.Algebra.Category.ModuleCat.Basic,Mathlib.Algebra.Category.Grp.ZModuleEquivalence,True783Mathlib.Algebra.Category.ModuleCat.Basic,Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures,True784Mathlib.Algebra.Category.ModuleCat.Basic,Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat,True785Mathlib.Algebra.Category.ModuleCat.Basic,Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic,True786Mathlib.Algebra.Category.ModuleCat.Basic,Mathlib.Algebra.Category.ModuleCat.Algebra,True787Mathlib.Algebra.Category.ModuleCat.Basic,Mathlib.CategoryTheory.Preadditive.Yoneda.Basic,True788Mathlib.Algebra.Category.ModuleCat.Basic,Mathlib.Algebra.Category.ModuleCat.Products,True789Mathlib.Algebra.Category.ModuleCat.Basic,Mathlib.Algebra.Category.ModuleCat.EpiMono,True790Mathlib.Algebra.Category.ModuleCat.Basic,Mathlib.Algebra.Category.ModuleCat.ExteriorPower,True791Mathlib.Algebra.Category.ModuleCat.Basic,Mathlib.Algebra.Category.ModuleCat.Colimits,True792Mathlib.Algebra.Category.ModuleCat.Basic,Mathlib.Algebra.Category.ModuleCat.Tannaka,True793Mathlib.CategoryTheory.Category.Grpd,Mathlib,True794Mathlib.CategoryTheory.Sites.CartesianMonoidal,Mathlib.CategoryTheory.Sites.CartesianClosed,True795Mathlib.Order.Types.Defs,Mathlib,True796Mathlib.LinearAlgebra.SModEq.Pointwise,Mathlib.RingTheory.AdicCompletion.Functoriality,True797Mathlib.CategoryTheory.Localization.Monoidal.Braided,Mathlib.CategoryTheory.Sites.Monoidal,True798Mathlib.Data.Fintype.Sets,Mathlib.Data.Fintype.Basic,True799Mathlib.Data.Fintype.Sets,Mathlib.Algebra.BigOperators.Group.Finset.Defs,True800Mathlib.Tactic.NormNum.NatLog,Mathlib.Tactic,True801Mathlib.Analysis.Calculus.Monotone,Mathlib.Analysis.BoundedVariation,True802Mathlib.LinearAlgebra.BilinearForm.Orthogonal,Mathlib.Algebra.Lie.InvariantForm,True803Mathlib.LinearAlgebra.BilinearForm.Orthogonal,Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate,True804Mathlib.GroupTheory.Perm.MaximalSubgroups,Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups,True805Mathlib.RingTheory.AdjoinRoot,Mathlib.RingTheory.Spectrum.Prime.Polynomial,True806Mathlib.RingTheory.AdjoinRoot,Mathlib.LinearAlgebra.FreeModule.Norm,True807Mathlib.RingTheory.AdjoinRoot,Mathlib.RingTheory.Finiteness.ModuleFinitePresentation,True808Mathlib.RingTheory.AdjoinRoot,Mathlib.FieldTheory.KummerPolynomial,True809Mathlib.RingTheory.AdjoinRoot,Mathlib.Algebra.Polynomial.Bivariate,True810Mathlib.RingTheory.AdjoinRoot,Mathlib.RingTheory.Localization.Away.AdjoinRoot,True811Mathlib.RingTheory.AdjoinRoot,Mathlib.RingTheory.Adjoin.Field,True812Mathlib.RingTheory.AdjoinRoot,Mathlib.RingTheory.Polynomial.IsIntegral,True813Mathlib.Order.OmegaCompletePartialOrder,Mathlib.Topology.OmegaCompletePartialOrder,True814Mathlib.Order.OmegaCompletePartialOrder,Mathlib.Order.CompletePartialOrder,True815Mathlib.Order.OmegaCompletePartialOrder,Mathlib.Order.FixedPoints,True816Mathlib.Order.OmegaCompletePartialOrder,Mathlib.Order.BourbakiWitt,True817Mathlib.Order.OmegaCompletePartialOrder,Mathlib.Order.SaddlePoint,True818Mathlib.Order.OmegaCompletePartialOrder,Mathlib.Control.LawfulFix,True819Mathlib.Order.OmegaCompletePartialOrder,Mathlib.LinearAlgebra.Span.Basic,True820Mathlib.Order.OmegaCompletePartialOrder,Mathlib.Order.Category.OmegaCompletePartialOrder,True821Mathlib.RingTheory.Nilpotent.Lemmas,Mathlib.RingTheory.Ideal.Quotient.Nilpotent,True822Mathlib.RingTheory.Nilpotent.Lemmas,Mathlib.LinearAlgebra.Eigenspace.Basic,True823Mathlib.RingTheory.Nilpotent.Lemmas,Mathlib.RingTheory.Noetherian.Nilpotent,True824Mathlib.RingTheory.Nilpotent.Lemmas,Mathlib.RingTheory.Spectrum.Prime.Basic,True825Mathlib.RingTheory.Nilpotent.Lemmas,Mathlib.RingTheory.Finiteness.Nilpotent,True826Mathlib.RingTheory.Nilpotent.Lemmas,Mathlib.RingTheory.Polynomial.Nilpotent,True827Mathlib.RingTheory.Nilpotent.Lemmas,Mathlib.RingTheory.ZMod,True828Mathlib.GroupTheory.MonoidLocalization.Cardinality,Mathlib.RingTheory.Localization.Cardinality,True829Mathlib.Algebra.Star.Unitary,Mathlib.Analysis.CStarAlgebra.Basic,True830Mathlib.Algebra.Star.Unitary,Mathlib.Algebra.QuadraticAlgebra.Basic,True831Mathlib.Algebra.Star.Unitary,Mathlib.Topology.Algebra.Star.Unitary,True832Mathlib.Algebra.Star.Unitary,Mathlib.NumberTheory.Zsqrtd.Basic,True833Mathlib.Algebra.Star.Unitary,Mathlib.LinearAlgebra.UnitaryGroup,True834Mathlib.Algebra.Star.Unitary,Mathlib.Algebra.Star.UnitaryStarAlgAut,True835Mathlib.Algebra.Star.Unitary,Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup,True836Mathlib.Algebra.Group.Submonoid.BigOperators,Mathlib.Data.DFinsupp.Submonoid,True837Mathlib.Algebra.Group.Submonoid.BigOperators,Mathlib.Algebra.BigOperators.Finsupp.Basic,True838Mathlib.Algebra.Group.Submonoid.BigOperators,Mathlib.Algebra.Ring.Subsemiring.Basic,True839Mathlib.Algebra.Group.Submonoid.BigOperators,Mathlib.Algebra.Module.Submodule.Basic,True840Mathlib.Algebra.Group.Submonoid.BigOperators,Mathlib.GroupTheory.Finiteness,True841Mathlib.Algebra.Group.Submonoid.BigOperators,Mathlib.GroupTheory.Perm.Sign,True842Mathlib.Algebra.Group.Submonoid.BigOperators,Mathlib.Algebra.Group.Subgroup.Finite,True843Mathlib.Algebra.Group.Submonoid.BigOperators,Mathlib.RingTheory.UniqueFactorizationDomain.Defs,True844Mathlib.Algebra.Group.Submonoid.BigOperators,Mathlib.Algebra.Module.Submodule.Lattice,True845Mathlib.Algebra.Group.Submonoid.BigOperators,Mathlib.RingTheory.NonUnitalSubring.Basic,True846Mathlib.Algebra.Homology.TotalComplexShift,Mathlib.Algebra.Homology.BifunctorShift,True847Mathlib.Geometry.RingedSpace.PresheafedSpace,Mathlib.Geometry.RingedSpace.Stalks,True848Mathlib.Geometry.RingedSpace.PresheafedSpace,Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits,True849Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1,Mathlib,True850Mathlib.RingTheory.Coalgebra.Hom,Mathlib.RingTheory.Bialgebra.Hom,True851Mathlib.RingTheory.Coalgebra.Hom,Mathlib.RingTheory.Coalgebra.Equiv,True852Mathlib.AlgebraicGeometry.Stalk,Mathlib.AlgebraicGeometry.ResidueField,True853Mathlib.Analysis.InnerProductSpace.Basic,Mathlib.Analysis.InnerProductSpace.Continuous,True854Mathlib.Analysis.InnerProductSpace.Basic,Mathlib.Geometry.Euclidean.Inversion.Basic,True855Mathlib.Analysis.InnerProductSpace.Basic,Mathlib.Analysis.InnerProductSpace.GramMatrix,True856Mathlib.Analysis.InnerProductSpace.Basic,Mathlib.Analysis.SpecialFunctions.Sigmoid,True857Mathlib.Analysis.InnerProductSpace.Basic,Mathlib.Analysis.InnerProductSpace.Projection.Minimal,True858Mathlib.Analysis.InnerProductSpace.Basic,Mathlib.Analysis.InnerProductSpace.Affine,True859Mathlib.Analysis.InnerProductSpace.Basic,Mathlib.Analysis.Convex.Strong,True860Mathlib.Analysis.InnerProductSpace.Basic,Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar,True861Mathlib.Analysis.InnerProductSpace.Basic,Mathlib.Analysis.InnerProductSpace.Convex,True862Mathlib.Analysis.Normed.Algebra.Basic,Mathlib.Analysis.CStarAlgebra.GelfandDuality,True863Mathlib.Algebra.MvPolynomial.Expand,Mathlib.RingTheory.MvPolynomial.Expand,True864Mathlib.Algebra.MvPolynomial.Expand,Mathlib.RingTheory.WittVector.WittPolynomial,True865Mathlib.Algebra.MvPolynomial.Expand,Mathlib.FieldTheory.Finite.Polynomial,True866Mathlib.GroupTheory.MonoidLocalization.Basic,Mathlib.GroupTheory.MonoidLocalization.Cardinality,True867Mathlib.GroupTheory.MonoidLocalization.Basic,Mathlib.GroupTheory.MonoidLocalization.Order,True868Mathlib.GroupTheory.MonoidLocalization.Basic,Mathlib.Topology.Algebra.Localization,True869Mathlib.GroupTheory.MonoidLocalization.Basic,Mathlib.GroupTheory.MonoidLocalization.DivPairs,True870Mathlib.GroupTheory.MonoidLocalization.Basic,Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero,True871Mathlib.GroupTheory.MonoidLocalization.Basic,Mathlib.GroupTheory.MonoidLocalization.Lemmas,True872Mathlib.GroupTheory.MonoidLocalization.Basic,Mathlib.GroupTheory.MonoidLocalization.Away,True873Mathlib.GroupTheory.MonoidLocalization.Basic,Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup,True874Mathlib.Data.PSigma.Order,Mathlib,True875Mathlib.Analysis.Analytic.IteratedFDeriv,Mathlib.Analysis.Calculus.FDeriv.Symmetric,True876Mathlib.Data.Nat.Choose.Factorization,Mathlib.Data.Nat.Multiplicity,True877Mathlib.Data.Nat.Choose.Factorization,Mathlib.NumberTheory.Bertrand,True878Mathlib.Data.PNat.Find,Mathlib,True879Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho,Mathlib.Analysis.Matrix.LDL,True880Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho,Mathlib.Analysis.InnerProductSpace.Orientation,True881Mathlib.LinearAlgebra.FreeModule.IdealQuotient,Mathlib.LinearAlgebra.FreeModule.Norm,True882Mathlib.LinearAlgebra.FreeModule.IdealQuotient,Mathlib.NumberTheory.NumberField.FinitePlaces,True883Mathlib.LinearAlgebra.FreeModule.IdealQuotient,Mathlib.NumberTheory.RamificationInertia.Unramified,True884Mathlib.GroupTheory.FreeGroup.Reduce,Mathlib.GroupTheory.FreeGroup.CyclicallyReduced,True885Mathlib.GroupTheory.FreeGroup.Reduce,Mathlib.SetTheory.Cardinal.Free,True886Mathlib.GroupTheory.FreeGroup.Reduce,Mathlib.GroupTheory.FreeGroup.Orbit,True887Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim,Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject,True888Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim,Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms,True889Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order,Mathlib.Analysis.CStarAlgebra.Unitary.Connected,True890Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order,Mathlib.Analysis.CStarAlgebra.Module.Defs,False891Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order,Mathlib.Analysis.CStarAlgebra.ApproximateUnit,True892Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order,Mathlib.Analysis.CStarAlgebra.Unitary.Span,True893Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order,Mathlib.Analysis.CStarAlgebra.Hom,True894Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order,Mathlib.Analysis.CStarAlgebra.PositiveLinearMap,True895Mathlib.Algebra.Homology.ShortComplex.Abelian,Mathlib.Algebra.Category.ModuleCat.Topology.Homology,True896Mathlib.Algebra.Homology.ShortComplex.Abelian,Mathlib.Algebra.Homology.ShortComplex.Exact,True897Mathlib.SetTheory.Cardinal.Arithmetic,Mathlib.Combinatorics.Matroid.Rank.Cardinal,True898Mathlib.SetTheory.Cardinal.Arithmetic,Mathlib.SetTheory.ZFC.VonNeumann,True899Mathlib.SetTheory.Cardinal.Arithmetic,Mathlib.Data.W.Cardinal,True900Mathlib.SetTheory.Cardinal.Arithmetic,Mathlib.SetTheory.Cardinal.Finsupp,True901Mathlib.SetTheory.Cardinal.Arithmetic,Mathlib.SetTheory.Cardinal.CountableCover,True902Mathlib.SetTheory.Cardinal.Arithmetic,Mathlib.RingTheory.HahnSeries.Cardinal,True903Mathlib.SetTheory.Cardinal.Arithmetic,Mathlib.SetTheory.Cardinal.Ordinal,True904Mathlib.SetTheory.Cardinal.Arithmetic,Mathlib.SetTheory.Cardinal.Cofinality,True905Mathlib.SetTheory.Cardinal.Arithmetic,Mathlib.GroupTheory.GroupAction.MultipleTransitivity,True906Mathlib.SetTheory.Cardinal.Arithmetic,Mathlib.ModelTheory.Encoding,True907Mathlib.SetTheory.Cardinal.Arithmetic,Mathlib.SetTheory.Cardinal.Continuum,True908Mathlib.SetTheory.Cardinal.Arithmetic,Mathlib.SetTheory.Cardinal.Divisibility,True909Mathlib.SetTheory.Cardinal.Arithmetic,Mathlib.GroupTheory.OreLocalization.Cardinality,True910Mathlib.SetTheory.Cardinal.Arithmetic,Mathlib.Data.Set.Card.Arithmetic,True911Mathlib.Analysis.Complex.Asymptotics,Mathlib.Analysis.SpecialFunctions.Exp,True912Mathlib.Algebra.Module.Presentation.Tensor,Mathlib,True913Mathlib.Topology.UniformSpace.Compact,Mathlib.Topology.UniformSpace.Closeds,False914Mathlib.Topology.UniformSpace.Compact,Mathlib.Topology.UniformSpace.CompactConvergence,True915Mathlib.Topology.UniformSpace.Compact,Mathlib.Topology.EMetricSpace.Basic,True916Mathlib.Topology.UniformSpace.Compact,Mathlib.Topology.UniformSpace.HeineCantor,True917Mathlib.Topology.UniformSpace.Compact,Mathlib.Topology.MetricSpace.Pseudo.Lemmas,True918Mathlib.RingTheory.KrullDimension.Zero,Mathlib.RingTheory.Localization.Pi,True919Mathlib.RingTheory.KrullDimension.Zero,Mathlib.RingTheory.HopkinsLevitzki,True920Mathlib.RingTheory.KrullDimension.Zero,Mathlib.RingTheory.KrullDimension.LocalRing,True921Mathlib.RingTheory.KrullDimension.Zero,Mathlib.RingTheory.Algebraic.StronglyTranscendental,True922Mathlib.RingTheory.KrullDimension.Zero,Mathlib.RingTheory.KrullDimension.PID,True923Mathlib.Data.Nat.Factorial.DoubleFactorial,Mathlib.Analysis.Distribution.FourierSchwartz,True924Mathlib.Data.Nat.Factorial.DoubleFactorial,Mathlib.NumberTheory.Cyclotomic.Three,True925Mathlib.Data.Nat.Factorial.DoubleFactorial,Mathlib.NumberTheory.Cyclotomic.Rat,True926Mathlib.Data.Nat.Factorial.DoubleFactorial,Mathlib.RingTheory.Polynomial.Hermite.Basic,True927Mathlib.Data.Nat.Factorial.DoubleFactorial,Mathlib.NumberTheory.Cyclotomic.PID,True928Mathlib.Data.Nat.Factorial.DoubleFactorial,Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral,True929Mathlib.Data.Nat.Factorial.DoubleFactorial,Mathlib.Data.Nat.Choose.Multinomial,True930Mathlib.Analysis.LocallyConvex.StrongTopology,Mathlib.Analysis.LocallyConvex.PointwiseConvergence,True931Mathlib.CategoryTheory.Functor.ReflectsIso.Basic,Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy,True932Mathlib.CategoryTheory.Functor.ReflectsIso.Basic,Mathlib.CategoryTheory.FiberedCategory.BasedCategory,True933Mathlib.CategoryTheory.Functor.ReflectsIso.Basic,Mathlib.CategoryTheory.Groupoid,True934Mathlib.Topology.Category.LightProfinite.Injective,Mathlib,True935Mathlib.Algebra.Order.Monoid.ToMulBot,Mathlib,True936Mathlib.Data.Array.Defs,Mathlib.Tactic.Translate.Core,True937Mathlib.Tactic.Nontriviality.Core,Mathlib.Tactic.Nontriviality,True938Mathlib.CategoryTheory.Groupoid.Discrete,Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Complete,True939Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp,Mathlib.Topology.EMetricSpace.PairReduction,True940Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp,Mathlib.Analysis.Asymptotics.ExpGrowth,True941Mathlib.CategoryTheory.Limits.Shapes.Connected,Mathlib.CategoryTheory.Sites.Over,True942Mathlib.Topology.Algebra.Valued.ValuativeRel,Mathlib.NumberTheory.LocalField.Basic,True943Mathlib.MeasureTheory.Function.LpSpace.Basic,Mathlib.MeasureTheory.Function.LpSpace.Complete,True944Mathlib.MeasureTheory.Function.LpSpace.Basic,Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions,True945Mathlib.MeasureTheory.Function.LpSpace.Basic,Mathlib.MeasureTheory.Function.LpSpace.Indicator,True946Mathlib.Topology.ContinuousMap.Sigma,Mathlib,True947Mathlib.AlgebraicGeometry.Fiber,Mathlib,True948Mathlib.Data.PFunctor.Univariate.M,Mathlib.Data.QPF.Univariate.Basic,True949Mathlib.Data.PFunctor.Univariate.M,Mathlib.Data.PFunctor.Multivariate.M,True950Mathlib.Algebra.Category.CoalgCat.Basic,Mathlib.Algebra.Category.CoalgCat.Monoidal,True951Mathlib.Algebra.Category.CoalgCat.Basic,Mathlib.Algebra.Category.CoalgCat.ComonEquivalence,True952Mathlib.Algebra.Category.CoalgCat.Basic,Mathlib.Algebra.Category.BialgCat.Basic,True953Mathlib.MeasureTheory.Integral.CircleIntegral,Mathlib.MeasureTheory.Integral.CircleAverage,True954Mathlib.MeasureTheory.Integral.CircleIntegral,Mathlib.MeasureTheory.Integral.TorusIntegral,True955Mathlib.MeasureTheory.Integral.CircleIntegral,Mathlib.MeasureTheory.Integral.CircleTransform,True956Mathlib.MeasureTheory.Integral.CircleIntegral,Mathlib.Analysis.Complex.CauchyIntegral,True957Mathlib.MeasureTheory.Integral.CircleIntegral,Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic,True958Mathlib.Algebra.Group.Pi.Basic,Mathlib.Algebra.Category.MonCat.Limits,True959Mathlib.Algebra.Group.Pi.Basic,Mathlib.Algebra.GroupWithZero.Pi,True960Mathlib.Algebra.Group.Pi.Basic,Mathlib.Algebra.GroupWithZero.Indicator,True961Mathlib.Algebra.Group.Pi.Basic,Mathlib.Algebra.Group.Action.Basic,True962Mathlib.Algebra.Group.Pi.Basic,Mathlib.Algebra.Divisibility.Prod,True963Mathlib.Algebra.Group.Pi.Basic,Mathlib.Algebra.Group.Pi.Units,True964Mathlib.Algebra.Group.Pi.Basic,Mathlib.Algebra.Group.Hom.Instances,True965Mathlib.Algebra.Group.Pi.Basic,Mathlib.Algebra.Group.Action.Pi,True966Mathlib.Algebra.Group.Pi.Basic,Mathlib.Algebra.Group.Indicator,True967Mathlib.Algebra.Group.Pi.Basic,Mathlib.Data.DFinsupp.Defs,True968Mathlib.Algebra.Group.Pi.Basic,Mathlib.Order.Filter.Basic,True969Mathlib.Algebra.Group.Pi.Basic,Mathlib.Data.Matrix.DMatrix,True970Mathlib.Algebra.Group.Pi.Basic,Mathlib.Algebra.Order.Group.PiLex,True971Mathlib.Algebra.Group.Pi.Basic,Mathlib.Algebra.Order.Group.Unbundled.Abs,True972Mathlib.Algebra.Group.Pi.Basic,Mathlib.Algebra.Group.End,True973Mathlib.Data.Option.Basic,Mathlib.Data.PEquiv,True974Mathlib.Data.Option.Basic,Mathlib.Logic.Equiv.Option,True975Mathlib.Data.Option.Basic,Mathlib.Algebra.Group.WithOne.Defs,True976Mathlib.Data.Option.Basic,Mathlib.Data.List.GetD,True977Mathlib.Data.Option.Basic,Mathlib.Order.WithBot,True978Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic,Mathlib.Analysis.Complex.Circle,True979Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic,Mathlib.Analysis.Convex.SpecificFunctions.Deriv,True980Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic,Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal,True981Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic,Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle,True982Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic,Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp,True983Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic,Mathlib.NumberTheory.Niven,True984Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic,Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse,True985Mathlib.Algebra.EuclideanDomain.Field,Mathlib.RingTheory.Polynomial.Dickson,True986Mathlib.Algebra.EuclideanDomain.Field,Mathlib.RingTheory.PrincipalIdealDomain,True987Mathlib.Algebra.EuclideanDomain.Field,Mathlib.Analysis.Calculus.Taylor,True988Mathlib.Algebra.Order.Monoid.NatCast,Mathlib.Order.RelSeries,True989Mathlib.Algebra.Order.Monoid.NatCast,Mathlib.Algebra.Order.Ring.Unbundled.Basic,True990Mathlib.Algebra.Order.Monoid.NatCast,Mathlib.SetTheory.Lists,True991Mathlib.Algebra.Order.Monoid.NatCast,Mathlib.Data.Bool.Count,True992Mathlib.Algebra.GCDMonoid.Finset,Mathlib.Algebra.GCDMonoid.FinsetLemmas,True993Mathlib.Algebra.GCDMonoid.Finset,Mathlib.NumberTheory.FLT.Basic,True994Mathlib.Algebra.GCDMonoid.Finset,Mathlib.LinearAlgebra.Matrix.Integer,True995Mathlib.Algebra.GCDMonoid.Finset,Mathlib.Dynamics.PeriodicPts.Lemmas,True996Mathlib.Algebra.GCDMonoid.Finset,Mathlib.RingTheory.Polynomial.Content,True997Mathlib.Algebra.MonoidAlgebra.Lift,Mathlib.Algebra.MonoidAlgebra.Module,True998Mathlib.Topology.Order.LiminfLimsup,Mathlib.Topology.Algebra.Order.LiminfLimsup,True999Mathlib.Topology.Order.LiminfLimsup,Mathlib.Topology.Instances.ENNReal.Lemmas,True1000Mathlib.Topology.Order.LiminfLimsup,Mathlib.Order.Filter.ENNReal,True1001Mathlib.Topology.Order.LiminfLimsup,Mathlib.Topology.MetricSpace.Algebra,False1002Mathlib.AlgebraicGeometry.GammaSpecAdjunction,Mathlib.AlgebraicGeometry.AffineScheme,True1003Mathlib.AlgebraicGeometry.GammaSpecAdjunction,Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme,True1004Mathlib.Algebra.GroupWithZero.Pointwise.Finset,Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset,True1005Mathlib.Algebra.DirectSum.AddChar,Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality,True1006Mathlib.Logic.Nontrivial.Defs,Mathlib.Logic.Function.Basic,True1007Mathlib.Logic.Nontrivial.Defs,Mathlib.Algebra.GroupWithZero.Defs,True1008Mathlib.Logic.Nontrivial.Defs,Mathlib.Data.TwoPointing,True1009Mathlib.Logic.Nontrivial.Defs,Mathlib.Data.Nat.Basic,True1010Mathlib.Algebra.Category.MonCat.Yoneda,Mathlib,True1011Mathlib.Analysis.InnerProductSpace.Dual,Mathlib.MeasureTheory.Measure.CharacteristicFunction,True1012Mathlib.Analysis.InnerProductSpace.Dual,Mathlib.Analysis.InnerProductSpace.Adjoint,True1013Mathlib.Analysis.InnerProductSpace.Dual,Mathlib.Analysis.Fourier.RiemannLebesgueLemma,True1014Mathlib.Analysis.InnerProductSpace.Dual,Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology,True1015Mathlib.Analysis.InnerProductSpace.Dual,Mathlib.Analysis.InnerProductSpace.TwoDim,True1016Mathlib.Analysis.InnerProductSpace.Dual,Mathlib.Analysis.InnerProductSpace.LaxMilgram,True1017Mathlib.Analysis.InnerProductSpace.Dual,Mathlib.Analysis.Calculus.Gradient.Basic,True1018Mathlib.Data.Nat.Cast.Basic,Mathlib.Data.Nat.ModEq,False1019Mathlib.Data.Nat.Cast.Basic,Mathlib.Algebra.CharP.Defs,True1020Mathlib.Data.Nat.Cast.Basic,Mathlib.Algebra.Ring.CharZero,True1021Mathlib.Data.Nat.Cast.Basic,Mathlib.Data.Nat.Factorial.Cast,True1022Mathlib.Data.Nat.Cast.Basic,Mathlib.Algebra.Ring.Submonoid.Pointwise,True1023Mathlib.Data.Nat.Cast.Basic,Mathlib.Data.Nat.Cast.Order.Basic,True1024Mathlib.Data.Nat.Cast.Basic,Mathlib.Data.Matrix.Diagonal,True1025Mathlib.Data.Nat.Cast.Basic,Mathlib.Order.Filter.Germ.Basic,True1026Mathlib.Data.Nat.Cast.Basic,Mathlib.Data.Nat.Cast.Field,True1027Mathlib.Data.Nat.Cast.Basic,Mathlib.MeasureTheory.MeasurableSpace.Basic,True1028Mathlib.Data.Nat.Cast.Basic,Mathlib.Algebra.Group.NatPowAssoc,True1029Mathlib.Data.Nat.Cast.Basic,Mathlib.Algebra.Ring.Parity,True1030Mathlib.Data.Nat.Cast.Basic,Mathlib.Tactic.NormNum.Basic,True1031Mathlib.Data.Nat.Cast.Basic,Mathlib.Algebra.CharZero.AddMonoidHom,True1032Mathlib.Topology.Category.Compactum,Mathlib,True1033Mathlib.Data.Multiset.FinsetOps,Mathlib.Data.Finset.Insert,True1034Mathlib.Data.Multiset.FinsetOps,Mathlib.Algebra.GCDMonoid.Multiset,True1035Mathlib.Data.Multiset.FinsetOps,Mathlib.Data.Finset.Lattice.Basic,True1036Mathlib.Data.Multiset.FinsetOps,Mathlib.Data.Multiset.Lattice,True1037Mathlib.Combinatorics.SimpleGraph.DegreeSum,Mathlib.Combinatorics.SimpleGraph.Matching,True1038Mathlib.Combinatorics.SimpleGraph.DegreeSum,Mathlib.Combinatorics.SimpleGraph.Extremal.Turan,True1039Mathlib.Combinatorics.SimpleGraph.DegreeSum,Mathlib.Combinatorics.SimpleGraph.Triangle.Removal,True1040Mathlib.Combinatorics.SimpleGraph.DegreeSum,Mathlib.Combinatorics.SimpleGraph.Bipartite,True1041Mathlib.Algebra.Group.Finsupp,Mathlib.Data.Finsupp.Ext,True1042Mathlib.Algebra.Group.Finsupp,Mathlib.Data.List.ToFinsupp,True1043Mathlib.Algebra.Group.Finsupp,Mathlib.Algebra.Group.UniqueProds.Basic,True1044Mathlib.Algebra.Group.Finsupp,Mathlib.Data.Finsupp.NeLocus,True1045Mathlib.Algebra.Group.Finsupp,Mathlib.Data.Finsupp.SMulWithZero,True1046Mathlib.Algebra.Group.Finsupp,Mathlib.Data.Finsupp.BigOperators,True1047Mathlib.Algebra.Group.Finsupp,Mathlib.Data.Finsupp.Pointwise,True1048Mathlib.Analysis.SpecialFunctions.Complex.LogBounds,Mathlib.Analysis.SpecialFunctions.Complex.Arctan,True1049Mathlib.Analysis.SpecialFunctions.Complex.LogBounds,Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral,True1050Mathlib.Analysis.SpecialFunctions.Complex.LogBounds,Mathlib.Analysis.SpecialFunctions.Gamma.Beta,True1051Mathlib.Analysis.SpecialFunctions.Complex.LogBounds,Mathlib.Analysis.SpecialFunctions.Log.Summable,True1052Mathlib.Algebra.Order.Nonneg.Module,Mathlib.Data.NNReal.Defs,True1053Mathlib.Algebra.Order.Nonneg.Module,Mathlib.RingTheory.Finiteness.Basic,True1054Mathlib.Algebra.Order.Nonneg.Module,Mathlib.Topology.Algebra.Order.Module,True1055Mathlib.Algebra.Order.Nonneg.Module,Mathlib.Geometry.Convex.Cone.Pointed,True1056Mathlib.AlgebraicGeometry.OpenImmersion,Mathlib.AlgebraicGeometry.Sites.MorphismProperty,True1057Mathlib.AlgebraicGeometry.OpenImmersion,Mathlib.AlgebraicGeometry.Modules.Sheaf,True1058Mathlib.AlgebraicTopology.SimplicialSet.CompStruct,Mathlib.AlgebraicTopology.SimplicialSet.Nerve,True1059Mathlib.Tactic.Ring,Mathlib.Data.PNat.Xgcd,True1060Mathlib.Tactic.Ring,Mathlib.Computability.Ackermann,True1061Mathlib.Tactic.Ring,Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating,True1062Mathlib.Tactic.Ring,Mathlib.Data.Nat.Factorial.DoubleFactorial,True1063Mathlib.Tactic.Ring,Mathlib.Combinatorics.Derangements.Finite,True1064Mathlib.Tactic.Ring,Mathlib.Algebra.Quandle,True1065Mathlib.Tactic.Ring,Mathlib.Algebra.ContinuedFractions.Determinant,True1066Mathlib.Tactic.Ring,Mathlib.Data.Nat.Digits.Defs,True1067Mathlib.Tactic.Ring,Mathlib.Algebra.Order.Ring.Ordering.Basic,True1068Mathlib.Tactic.Ring,Mathlib.Combinatorics.SimpleGraph.Density,True1069Mathlib.Tactic.Ring,Mathlib.Data.Nat.Factorial.SuperFactorial,True1070Mathlib.Tactic.Ring,Mathlib.Algebra.Order.BigOperators.Ring.Finset,True1071Mathlib.Tactic.Ring,Mathlib.Data.Complex.Basic,True1072Mathlib.Tactic.Ring,Mathlib.Data.Nat.Choose.Sum,True1073Mathlib.Tactic.Ring,Mathlib.Tactic.Group,True1074Mathlib.Tactic.Ring,Mathlib.Combinatorics.Additive.PluenneckeRuzsa,True1075Mathlib.Tactic.Ring,Mathlib.RingTheory.Localization.Defs,True1076Mathlib.Tactic.Ring,Mathlib.Combinatorics.SetFamily.FourFunctions,True1077Mathlib.Tactic.Ring,Mathlib.AlgebraicTopology.DoldKan.Faces,True1078Mathlib.Tactic.Ring,Mathlib.Order.Interval.Finset.Box,True1079Mathlib.Tactic.Ring,Mathlib.Tactic.LinearCombination',True1080Mathlib.Tactic.Ring,Mathlib.Data.Rat.Floor,True1081Mathlib.Tactic.Ring,Mathlib.Data.Nat.Fib.Basic,True1082Mathlib.Tactic.Ring,Mathlib.Algebra.Ring.Identities,True1083Mathlib.Tactic.Ring,Mathlib.Algebra.Ring.BooleanRing,True1084Mathlib.Tactic.Ring,Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet,True1085Mathlib.Tactic.Ring,Mathlib.Data.Nat.Choose.Central,True1086Mathlib.Tactic.Ring,Mathlib.RingTheory.Coprime.Basic,True1087Mathlib.Tactic.Ring,Mathlib.RingTheory.Ideal.Span,True1088Mathlib.Analysis.SpecialFunctions.Gamma.Basic,Mathlib.Analysis.Distribution.FourierSchwartz,True1089Mathlib.Analysis.SpecialFunctions.Gamma.Basic,Mathlib.MeasureTheory.Integral.Gamma,True1090Mathlib.Analysis.SpecialFunctions.Gamma.Basic,Mathlib.NumberTheory.Cyclotomic.Three,True1091Mathlib.Analysis.SpecialFunctions.Gamma.Basic,Mathlib.Analysis.SpecialFunctions.Gamma.Deriv,True1092Mathlib.Analysis.SpecialFunctions.Gamma.Basic,Mathlib.NumberTheory.Cyclotomic.Rat,True1093Mathlib.Analysis.SpecialFunctions.Gamma.Basic,Mathlib.NumberTheory.Cyclotomic.PID,True1094Mathlib.Analysis.SpecialFunctions.Gamma.Basic,Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral,True1095Mathlib.Analysis.SpecialFunctions.Gamma.Basic,Mathlib.Probability.Distributions.Gamma,True1096Mathlib.Analysis.Normed.Group.SeparationQuotient,Mathlib,True1097Mathlib.Probability.Martingale.Centering,Mathlib.Probability.Martingale.BorelCantelli,True1098Mathlib.Algebra.Group.Submonoid.Pointwise,Mathlib.Algebra.Ring.Submonoid.Pointwise,True1099Mathlib.Algebra.Group.Submonoid.Pointwise,Mathlib.Algebra.Group.Subgroup.Pointwise,True1100Mathlib.Algebra.Group.Submonoid.Pointwise,Mathlib.GroupTheory.Submonoid.Inverses,True1101Mathlib.Algebra.Group.Submonoid.Pointwise,Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise,True1102Mathlib.Algebra.Group.Submonoid.Pointwise,Mathlib.Algebra.Group.Submonoid.Units,True1103Mathlib.Util.Simp,Mathlib,True1104Mathlib.AlgebraicGeometry.Morphisms.Preimmersion,Mathlib.AlgebraicGeometry.Stalk,True1105Mathlib.AlgebraicGeometry.Morphisms.Preimmersion,Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme,True1106Mathlib.RingTheory.Ideal.Maps,Mathlib.RingTheory.Ideal.Colon,True1107Mathlib.RingTheory.Ideal.Maps,Mathlib.RingTheory.Valuation.Basic,True1108Mathlib.RingTheory.Ideal.Maps,Mathlib.RingTheory.Nilpotent.Lemmas,True1109Mathlib.RingTheory.Ideal.Maps,Mathlib.Algebra.Polynomial.Module.AEval,True1110Mathlib.RingTheory.Ideal.Maps,Mathlib.RingTheory.Finiteness.Ideal,True1111Mathlib.RingTheory.Ideal.Maps,Mathlib.RingTheory.Ideal.Quotient.PowTransition,True1112Mathlib.RingTheory.Ideal.Maps,Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology,True1113Mathlib.RingTheory.Ideal.Maps,Mathlib.LinearAlgebra.TensorProduct.Quotient,True1114Mathlib.RingTheory.Ideal.Maps,Mathlib.RingTheory.Polynomial.Ideal,True1115Mathlib.RingTheory.Ideal.Maps,Mathlib.RingTheory.Localization.Away.Basic,True1116Mathlib.RingTheory.Ideal.Maps,Mathlib.Algebra.CharP.Quotient,True1117Mathlib.RingTheory.Ideal.Maps,Mathlib.RingTheory.Ideal.Prod,True1118Mathlib.RingTheory.Ideal.Maps,Mathlib.RingTheory.Jacobson.Radical,True1119Mathlib.RingTheory.Ideal.Maps,Mathlib.Algebra.Colimit.Ring,True1120Mathlib.RingTheory.Ideal.Maps,Mathlib.RingTheory.AlgebraicIndependent.Basic,True1121Mathlib.RingTheory.Ideal.Maps,Mathlib.Algebra.Algebra.Subalgebra.Operations,True1122Mathlib.RingTheory.Ideal.Maps,Mathlib.Combinatorics.Nullstellensatz,True1123Mathlib.RingTheory.Ideal.Maps,Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal,True1124Mathlib.RingTheory.Ideal.Maps,Mathlib.Algebra.Algebra.Spectrum.Basic,True1125Mathlib.RingTheory.Ideal.Maps,Mathlib.RingTheory.Ideal.Pointwise,True1126Mathlib.RingTheory.Ideal.Maps,Mathlib.LinearAlgebra.TensorProduct.RightExactness,True1127Mathlib.RingTheory.Ideal.Maps,Mathlib.RingTheory.DividedPowers.Basic,True1128Mathlib.RingTheory.Ideal.Maps,Mathlib.RingTheory.PowerSeries.NoZeroDivisors,True1129Mathlib.RingTheory.Spectrum.Prime.Polynomial,Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity,True1130Mathlib.Topology.Algebra.GroupWithZero,Mathlib.Topology.Algebra.Field,True1131Mathlib.Topology.Algebra.GroupWithZero,Mathlib.Topology.Algebra.InfiniteSum.Ring,True1132Mathlib.Topology.Algebra.GroupWithZero,Mathlib.Topology.Algebra.WithZeroTopology,True1133Mathlib.Topology.Algebra.GroupWithZero,Mathlib.Topology.Algebra.IsOpenUnits,True1134Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass,Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ,True1135Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass,Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange,True1136Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology,Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom,True1137Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology,Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle,True1138Mathlib.Data.List.Enum,Mathlib.Data.List.OffDiag,False1139Mathlib.Probability.Independence.Kernel.IndepFun,Mathlib.Probability.Independence.Basic,True1140Mathlib.Probability.Independence.Kernel.IndepFun,Mathlib.Probability.Independence.Conditional,True1141Mathlib.Probability.Independence.Kernel.IndepFun,Mathlib.Probability.Independence.Kernel,True1142Mathlib.Analysis.NormedSpace.HomeomorphBall,Mathlib,True1143Mathlib.Combinatorics.Derangements.Exponential,Mathlib,True1144Mathlib.Algebra.Ring.Action.Pointwise.Set,Mathlib.RingTheory.Ideal.Colon,True1145Mathlib.Algebra.Ring.Action.Pointwise.Set,Mathlib.Algebra.Ring.Action.Pointwise.Finset,True1146Mathlib.Algebra.Ring.Action.Pointwise.Set,Mathlib.Analysis.Convex.Basic,True1147Mathlib.Algebra.Ring.Action.Pointwise.Set,Mathlib.Analysis.Normed.Module.Ball.RadialEquiv,True1148Mathlib.Algebra.Ring.Action.Pointwise.Set,Mathlib.Topology.Bornology.Absorbs,True1149Mathlib.Probability.Process.Stopping,Mathlib.Probability.Process.HittingTime,True1150Mathlib.Probability.Process.Stopping,Mathlib.Probability.Martingale.Basic,True1151Mathlib.CategoryTheory.Monoidal.Functor,Mathlib.CategoryTheory.Monoidal.Closed.Basic,True1152Mathlib.CategoryTheory.Monoidal.Functor,Mathlib.CategoryTheory.Localization.Monoidal.Basic,True1153Mathlib.CategoryTheory.Monoidal.Functor,Mathlib.CategoryTheory.Monoidal.Opposite,True1154Mathlib.CategoryTheory.Monoidal.Functor,Mathlib.CategoryTheory.Monoidal.End,True1155Mathlib.CategoryTheory.Monoidal.Functor,Mathlib.CategoryTheory.Monoidal.Free.Basic,True1156Mathlib.CategoryTheory.Monoidal.Functor,Mathlib.CategoryTheory.Monoidal.Preadditive,True1157Mathlib.CategoryTheory.Monoidal.Functor,Mathlib.CategoryTheory.Monoidal.NaturalTransformation,True1158Mathlib.CategoryTheory.Monoidal.Functor,Mathlib.CategoryTheory.Monoidal.Multifunctor,True1159Mathlib.CategoryTheory.Monoidal.Functor,Mathlib.CategoryTheory.Bicategory.SingleObj,True1160Mathlib.CategoryTheory.Bicategory.InducedBicategory,Mathlib,True1161Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle,Mathlib.Geometry.Euclidean.Angle.Sphere,True1162Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift,Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology,True1163Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift,Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated,True1164Mathlib.Data.Int.Fib.Lemmas,Mathlib,True1165Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu,Mathlib,True1166Mathlib.Topology.Algebra.Module.Multilinear.Topology,Mathlib.Topology.Algebra.Module.Alternating.Topology,True1167Mathlib.Topology.Algebra.Module.Multilinear.Topology,Mathlib.Analysis.Normed.Module.Multilinear.Basic,True1168Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing,Mathlib.AlgebraicGeometry.Gluing,True1169Mathlib.LinearAlgebra.Projectivization.Independence,Mathlib,True1170Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four,Mathlib.Algebra.Homology.HomologySequenceLemmas,True1171Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four,Mathlib.CategoryTheory.Abelian.Yoneda,True1172Mathlib.Algebra.Group.ConjFinite,Mathlib.GroupTheory.ClassEquation,True1173Mathlib.Algebra.Group.ConjFinite,Mathlib.GroupTheory.GroupAction.CardCommute,True1174Mathlib.CategoryTheory.Sites.Localization,Mathlib.CategoryTheory.Sites.PreservesSheafification,True1175Mathlib.Data.Set.Inclusion,Mathlib.Data.Set.Image,True1176Mathlib.Data.Set.Inclusion,Mathlib.Algebra.Group.Subgroup.Defs,True1177Mathlib.Algebra.Group.Torsion,Mathlib.Algebra.Group.Opposite,True1178Mathlib.Algebra.Group.Torsion,Mathlib.Algebra.Ring.Idempotent,True1179Mathlib.Algebra.Group.Torsion,Mathlib.Algebra.Group.TypeTags.Basic,True1180Mathlib.Algebra.Group.Torsion,Mathlib.Algebra.Group.Pi.Lemmas,True1181Mathlib.Algebra.Group.Torsion,Mathlib.Algebra.Group.ModEq,False1182Mathlib.Algebra.Group.Torsion,Mathlib.Algebra.Ring.Torsion,True1183Mathlib.Order.Interval.Set.OrderEmbedding,Mathlib.Order.UpperLower.Basic,True1184Mathlib.Order.Interval.Set.OrderEmbedding,Mathlib.Order.Interval.Set.OrdConnected,True1185Mathlib.MeasureTheory.OuterMeasure.AE,Mathlib.MeasureTheory.OuterMeasure.BorelCantelli,True1186Mathlib.MeasureTheory.OuterMeasure.AE,Mathlib.MeasureTheory.Measure.MeasureSpaceDef,True1187Mathlib.Analysis.Calculus.UniformLimitsDeriv,Mathlib.Analysis.Complex.LocallyUniformLimit,True1188Mathlib.Analysis.Calculus.UniformLimitsDeriv,Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn,True1189Mathlib.Analysis.Calculus.UniformLimitsDeriv,Mathlib.Analysis.Calculus.SmoothSeries,True1190Mathlib.Data.Finset.Lattice.Pi,Mathlib,True1191Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono,Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms,True1192Mathlib.LinearAlgebra.FreeModule.ModN,Mathlib,True1193Mathlib.Topology.Algebra.Order.UpperLower,Mathlib.Analysis.Normed.Order.UpperLower,True1194Mathlib.Tactic.ToFun,Mathlib.Tactic.Common,True1195Mathlib.LinearAlgebra.FreeModule.Basic,Mathlib.LinearAlgebra.Finsupp.VectorSpace,True1196Mathlib.LinearAlgebra.FreeModule.Basic,Mathlib.RingTheory.TensorProduct.IsBaseChangeFree,True1197Mathlib.LinearAlgebra.FreeModule.Basic,Mathlib.RingTheory.Localization.AsSubring,True1198Mathlib.LinearAlgebra.FreeModule.Basic,Mathlib.Algebra.Central.End,True1199Mathlib.LinearAlgebra.FreeModule.Basic,Mathlib.LinearAlgebra.Basis.VectorSpace,True1200Mathlib.LinearAlgebra.FreeModule.Basic,Mathlib.Algebra.SkewMonoidAlgebra.Basic,True
Showing the first 1,200 of 20883 lines. Download the file for the rest.