feat(Analysis/NormedSpace/MStructure): M-ideals#26337
Draft
mans0954 wants to merge 172 commits intoleanprover-community:masterfrom
Draft
feat(Analysis/NormedSpace/MStructure): M-ideals#26337mans0954 wants to merge 172 commits intoleanprover-community:masterfrom
mans0954 wants to merge 172 commits intoleanprover-community:masterfrom
Conversation
Collaborator
Author
Comments from Original PR #14369This section contains 1 comment(s) from the original PR, excluding bot comments. @github-actions (2024-07-02 21:47 UTC): PR summary 8b2141b23dImport changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Analysis.NormedSpace.MStructure | 1074 | 1969 | +895 (+83.33%) |
| Mathlib.Algebra.Module.End | 388 | 476 | +88 (+22.68%) |
| Mathlib.Algebra.Module.Hom | 442 | 490 | +48 (+10.86%) |
| Mathlib.Algebra.Module.LinearMap.End | 452 | 453 | +1 (+0.22%) |
Import changes for all files
| Files | Import difference |
|---|---|
8 filesMathlib.Algebra.Module.LinearMap.End Mathlib.Algebra.Module.Submodule.EqLocus Mathlib.Algebra.Module.Submodule.Equiv Mathlib.Algebra.Module.Submodule.IterateMapComap Mathlib.Algebra.Module.Submodule.Ker Mathlib.Algebra.Module.Submodule.LinearMap Mathlib.Algebra.Module.Submodule.Map Mathlib.Algebra.Module.Submodule.Range |
1 |
1225 filesMathlib.Algebra.Algebra.Basic Mathlib.Algebra.Algebra.Bilinear Mathlib.Algebra.Algebra.Equiv Mathlib.Algebra.Algebra.Hom.Rat Mathlib.Algebra.Algebra.Hom Mathlib.Algebra.Algebra.NonUnitalHom Mathlib.Algebra.Algebra.NonUnitalSubalgebra Mathlib.Algebra.Algebra.Operations Mathlib.Algebra.Algebra.Opposite Mathlib.Algebra.Algebra.Pi Mathlib.Algebra.Algebra.Prod Mathlib.Algebra.Algebra.RestrictScalars Mathlib.Algebra.Algebra.Subalgebra.Basic Mathlib.Algebra.Algebra.Subalgebra.Centralizer Mathlib.Algebra.Algebra.Subalgebra.Directed Mathlib.Algebra.Algebra.Subalgebra.Lattice Mathlib.Algebra.Algebra.Subalgebra.MulOpposite Mathlib.Algebra.Algebra.Subalgebra.Order Mathlib.Algebra.Algebra.Subalgebra.Pi Mathlib.Algebra.Algebra.Subalgebra.Pointwise Mathlib.Algebra.Algebra.Subalgebra.Prod Mathlib.Algebra.Algebra.Subalgebra.Tower Mathlib.Algebra.Algebra.Subalgebra.Unitization Mathlib.Algebra.Algebra.Tower Mathlib.Algebra.Algebra.Unitization Mathlib.Algebra.Algebra.ZMod Mathlib.Algebra.Category.AlgCat.Basic Mathlib.Algebra.Category.AlgCat.Limits Mathlib.Algebra.Category.AlgCat.Monoidal Mathlib.Algebra.Category.AlgCat.Symmetric Mathlib.Algebra.Category.AlgebraCat.Symmetric Mathlib.Algebra.Category.Grp.AB Mathlib.Algebra.Category.Grp.Abelian Mathlib.Algebra.Category.Grp.Adjunctions Mathlib.Algebra.Category.Grp.Biproducts Mathlib.Algebra.Category.Grp.CartesianMonoidal Mathlib.Algebra.Category.Grp.ChosenFiniteProducts Mathlib.Algebra.Category.Grp.Colimits Mathlib.Algebra.Category.Grp.Images Mathlib.Algebra.Category.Grp.IsFinite Mathlib.Algebra.Category.Grp.LeftExactFunctor Mathlib.Algebra.Category.Grp.Limits Mathlib.Algebra.Category.Grp.Subobject Mathlib.Algebra.Category.ModuleCat.AB Mathlib.Algebra.Category.ModuleCat.Abelian Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.Algebra.Category.ModuleCat.Algebra Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Colimits Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.Algebra.Category.ModuleCat.FilteredColimits Mathlib.Algebra.Category.ModuleCat.Images Mathlib.Algebra.Category.ModuleCat.Injective Mathlib.Algebra.Category.ModuleCat.Kernels Mathlib.Algebra.Category.ModuleCat.Limits Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono Mathlib.Algebra.Category.ModuleCat.Presheaf.Free Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.Algebra.Category.ModuleCat.Products Mathlib.Algebra.Category.ModuleCat.Projective Mathlib.Algebra.Category.ModuleCat.Pseudofunctor Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.Algebra.Category.ModuleCat.Tannaka Mathlib.Algebra.Category.MonCat.Limits Mathlib.Algebra.Category.Ring.Adjunctions Mathlib.Algebra.Category.Ring.Limits Mathlib.Algebra.Central.Basic Mathlib.Algebra.Central.Defs Mathlib.Algebra.Central.Matrix Mathlib.Algebra.CharP.Algebra Mathlib.Algebra.CharP.CharAndCard Mathlib.Algebra.CharP.Subring Mathlib.Algebra.Colimit.Module Mathlib.Algebra.DirectSum.AddChar Mathlib.Algebra.DirectSum.Algebra Mathlib.Algebra.DirectSum.Decomposition Mathlib.Algebra.DirectSum.Finsupp Mathlib.Algebra.DirectSum.Internal Mathlib.Algebra.DirectSum.Module Mathlib.Algebra.DualNumber Mathlib.Algebra.Equiv.TransferInstance Mathlib.Algebra.Exact Mathlib.Algebra.Field.NegOnePow Mathlib.Algebra.Field.Periodic Mathlib.Algebra.Field.ZMod Mathlib.Algebra.FiveLemma Mathlib.Algebra.FreeAbelianGroup.Finsupp Mathlib.Algebra.FreeAbelianGroup.UniqueSums Mathlib.Algebra.FreeAlgebra.Cardinality Mathlib.Algebra.FreeAlgebra Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra Mathlib.Algebra.Group.AddChar Mathlib.Algebra.Group.ForwardDiff Mathlib.Algebra.Group.UniqueProds.VectorSpace Mathlib.Algebra.Homology.AlternatingConst Mathlib.Algebra.Homology.BifunctorAssociator Mathlib.Algebra.Homology.BifunctorFlip Mathlib.Algebra.Homology.BifunctorHomotopy Mathlib.Algebra.Homology.BifunctorShift Mathlib.Algebra.Homology.Bifunctor Mathlib.Algebra.Homology.ComplexShapeSigns Mathlib.Algebra.Homology.ConcreteCategory Mathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass Mathlib.Algebra.Homology.DerivedCategory.Fractions Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.Algebra.Homology.Embedding.CochainComplex Mathlib.Algebra.Homology.Embedding.ExtendHomology Mathlib.Algebra.Homology.Embedding.Extend Mathlib.Algebra.Homology.Embedding.HomEquiv Mathlib.Algebra.Homology.Embedding.IsSupported Mathlib.Algebra.Homology.Embedding.RestrictionHomology Mathlib.Algebra.Homology.Embedding.StupidTrunc Mathlib.Algebra.Homology.Embedding.TruncGEHomology Mathlib.Algebra.Homology.Embedding.TruncGE Mathlib.Algebra.Homology.Embedding.TruncLEHomology Mathlib.Algebra.Homology.Embedding.TruncLE Mathlib.Algebra.Homology.ExactSequence Mathlib.Algebra.Homology.Factorizations.Basic Mathlib.Algebra.Homology.GrothendieckAbelian Mathlib.Algebra.Homology.HomologicalComplexAbelian Mathlib.Algebra.Homology.HomologySequenceLemmas Mathlib.Algebra.Homology.HomologySequence Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift Mathlib.Algebra.Homology.HomotopyCategory.HomComplex Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor Mathlib.Algebra.Homology.HomotopyCategory.MappingCone Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence Mathlib.Algebra.Homology.HomotopyCategory.Shift Mathlib.Algebra.Homology.HomotopyCategory.ShortExact Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors Mathlib.Algebra.Homology.HomotopyCategory.Triangulated Mathlib.Algebra.Homology.HomotopyCategory Mathlib.Algebra.Homology.HomotopyCofiber Mathlib.Algebra.Homology.Homotopy Mathlib.Algebra.Homology.Localization Mathlib.Algebra.Homology.Monoidal Mathlib.Algebra.Homology.Opposite Mathlib.Algebra.Homology.QuasiIso Mathlib.Algebra.Homology.Refinements Mathlib.Algebra.Homology.ShortComplex.Ab Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.Algebra.Homology.ShortComplex.ExactFunctor Mathlib.Algebra.Homology.ShortComplex.Exact Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex Mathlib.Algebra.Homology.ShortComplex.Linear Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.Algebra.Homology.ShortComplex.Preadditive Mathlib.Algebra.Homology.ShortComplex.ShortExact Mathlib.Algebra.Homology.ShortComplex.SnakeLemma Mathlib.Algebra.Homology.SingleHomology Mathlib.Algebra.Homology.TotalComplexShift Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.Algebra.Homology.TotalComplex Mathlib.Algebra.Lie.Basic Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra Mathlib.Algebra.Module.Bimodule Mathlib.Algebra.Module.GradedModule Mathlib.Algebra.Module.Injective Mathlib.Algebra.Module.LocalizedModule.AtPrime Mathlib.Algebra.Module.LocalizedModule.Away Mathlib.Algebra.Module.LocalizedModule.Basic Mathlib.Algebra.Module.LocalizedModule.Exact Mathlib.Algebra.Module.LocalizedModule.Int Mathlib.Algebra.Module.LocalizedModule.IsLocalization Mathlib.Algebra.Module.LocalizedModule.Submodule Mathlib.Algebra.Module.Presentation.Basic Mathlib.Algebra.Module.Presentation.Cokernel Mathlib.Algebra.Module.Presentation.DirectSum Mathlib.Algebra.Module.Presentation.Free Mathlib.Algebra.Module.Presentation.RestrictScalars Mathlib.Algebra.Module.Presentation.Tautological Mathlib.Algebra.Module.Presentation.Tensor Mathlib.Algebra.Module.Projective Mathlib.Algebra.Module.SnakeLemma Mathlib.Algebra.Module.Submodule.Bilinear Mathlib.Algebra.Module.Submodule.Pointwise Mathlib.Algebra.Module.ZMod Mathlib.Algebra.MonoidAlgebra.Basic Mathlib.Algebra.MonoidAlgebra.Degree Mathlib.Algebra.MonoidAlgebra.Grading Mathlib.Algebra.MonoidAlgebra.Support Mathlib.Algebra.MonoidAlgebra.ToDirectSum Mathlib.Algebra.MvPolynomial.Basic Mathlib.Algebra.MvPolynomial.Cardinal Mathlib.Algebra.MvPolynomial.Comap Mathlib.Algebra.MvPolynomial.CommRing Mathlib.Algebra.MvPolynomial.Counit Mathlib.Algebra.MvPolynomial.Degrees Mathlib.Algebra.MvPolynomial.Derivation Mathlib.Algebra.MvPolynomial.Division Mathlib.Algebra.MvPolynomial.Equiv Mathlib.Algebra.MvPolynomial.Eval Mathlib.Algebra.MvPolynomial.Expand Mathlib.Algebra.MvPolynomial.Invertible Mathlib.Algebra.MvPolynomial.Monad Mathlib.Algebra.MvPolynomial.PDeriv Mathlib.Algebra.MvPolynomial.Polynomial Mathlib.Algebra.MvPolynomial.Rename Mathlib.Algebra.MvPolynomial.SchwartzZippel Mathlib.Algebra.MvPolynomial.Supported Mathlib.Algebra.MvPolynomial.Variables Mathlib.Algebra.Order.Chebyshev Mathlib.Algebra.Order.Group.Cyclic Mathlib.Algebra.Order.ToIntervalMod Mathlib.Algebra.Polynomial.AlgebraMap Mathlib.Algebra.Polynomial.Basis Mathlib.Algebra.Polynomial.BigOperators Mathlib.Algebra.Polynomial.CancelLeads Mathlib.Algebra.Polynomial.CoeffList Mathlib.Algebra.Polynomial.Coeff Mathlib.Algebra.Polynomial.Degree.Definitions Mathlib.Algebra.Polynomial.Degree.Domain Mathlib.Algebra.Polynomial.Degree.Lemmas Mathlib.Algebra.Polynomial.Degree.Monomial Mathlib.Algebra.Polynomial.Degree.Operations Mathlib.Algebra.Polynomial.Degree.SmallDegree Mathlib.Algebra.Polynomial.Degree.Support Mathlib.Algebra.Polynomial.Degree.TrailingDegree Mathlib.Algebra.Polynomial.Degree.Units Mathlib.Algebra.Polynomial.DenomsClearable Mathlib.Algebra.Polynomial.Derivative Mathlib.Algebra.Polynomial.Div Mathlib.Algebra.Polynomial.EraseLead Mathlib.Algebra.Polynomial.Eval.Coeff Mathlib.Algebra.Polynomial.Eval.Degree Mathlib.Algebra.Polynomial.Eval.Irreducible Mathlib.Algebra.Polynomial.Eval.SMul Mathlib.Algebra.Polynomial.Eval.Subring Mathlib.Algebra.Polynomial.GroupRingAction Mathlib.Algebra.Polynomial.HasseDeriv Mathlib.Algebra.Polynomial.Identities Mathlib.Algebra.Polynomial.Inductions Mathlib.Algebra.Polynomial.Lifts Mathlib.Algebra.Polynomial.Mirror Mathlib.Algebra.Polynomial.Monic Mathlib.Algebra.Polynomial.OfFn Mathlib.Algebra.Polynomial.PartialFractions Mathlib.Algebra.Polynomial.Reverse Mathlib.Algebra.Polynomial.RingDivision Mathlib.Algebra.Polynomial.Roots Mathlib.Algebra.Polynomial.Sequence Mathlib.Algebra.Polynomial.Smeval Mathlib.Algebra.Polynomial.SumIteratedDerivative Mathlib.Algebra.Polynomial.Taylor Mathlib.Algebra.Polynomial.UnitTrinomial Mathlib.Algebra.Ring.NegOnePow Mathlib.Algebra.Ring.Periodic Mathlib.Algebra.Ring.Subring.IntPolynomial Mathlib.Algebra.Small.Group Mathlib.Algebra.Small.Module Mathlib.Algebra.Small.Ring Mathlib.Algebra.Star.CHSH Mathlib.Algebra.Star.Free Mathlib.Algebra.Star.Module Mathlib.Algebra.Star.NonUnitalSubalgebra Mathlib.Algebra.Star.StarAlgHom Mathlib.Algebra.Star.Subalgebra Mathlib.Algebra.TrivSqZeroExt Mathlib.Algebra.Vertex.HVertexOperator Mathlib.Algebra.Vertex.VertexOperator Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.AlgebraicTopology.DoldKan.Equivalence Mathlib.AlgebraicTopology.DoldKan.Faces Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.AlgebraicTopology.DoldKan.GammaCompN Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit Mathlib.AlgebraicTopology.FundamentalGroupoid.Product Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected Mathlib.AlgebraicTopology.SingularHomology.Basic Mathlib.AlgebraicTopology.SingularSet Mathlib.AlgebraicTopology.TopologicalSimplex Mathlib.Analysis.Analytic.Basic Mathlib.Analysis.Analytic.CPolynomialDef Mathlib.Analysis.Analytic.ChangeOrigin Mathlib.Analysis.Analytic.Composition Mathlib.Analysis.Analytic.Inverse Mathlib.Analysis.Analytic.Linear Mathlib.Analysis.Analytic.OfScalars Mathlib.Analysis.Asymptotics.AsymptoticEquivalent Mathlib.Analysis.Asymptotics.Completion Mathlib.Analysis.Asymptotics.Defs Mathlib.Analysis.Asymptotics.Lemmas Mathlib.Analysis.Asymptotics.LinearGrowth Mathlib.Analysis.Asymptotics.SpecificAsymptotics Mathlib.Analysis.Asymptotics.SuperpolynomialDecay Mathlib.Analysis.Asymptotics.TVS Mathlib.Analysis.Asymptotics.Theta Mathlib.Analysis.BoxIntegral.Box.SubboxInduction Mathlib.Analysis.BoxIntegral.Partition.Additive Mathlib.Analysis.BoxIntegral.Partition.Filter Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction Mathlib.Analysis.Calculus.Deriv.Basic Mathlib.Analysis.Calculus.Deriv.Comp Mathlib.Analysis.Calculus.Deriv.Slope Mathlib.Analysis.Calculus.Deriv.Support Mathlib.Analysis.Calculus.FDeriv.Basic Mathlib.Analysis.Calculus.FDeriv.Comp Mathlib.Analysis.Calculus.FDeriv.Congr Mathlib.Analysis.Calculus.FDeriv.Const Mathlib.Analysis.Calculus.FDeriv.Defs Mathlib.Analysis.Calculus.FDeriv.RestrictScalars Mathlib.Analysis.Calculus.FormalMultilinearSeries Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn Mathlib.Analysis.Calculus.TangentCone Mathlib.Analysis.Convex.Basic Mathlib.Analysis.Convex.Birkhoff Mathlib.Analysis.Convex.Body Mathlib.Analysis.Convex.Caratheodory Mathlib.Analysis.Convex.Combination Mathlib.Analysis.Convex.Cone.Extension Mathlib.Analysis.Convex.Contractible Mathlib.Analysis.Convex.EGauge Mathlib.Analysis.Convex.Exposed Mathlib.Analysis.Convex.Extrema Mathlib.Analysis.Convex.Extreme Mathlib.Analysis.Convex.Function Mathlib.Analysis.Convex.Hull Mathlib.Analysis.Convex.Independent Mathlib.Analysis.Convex.Jensen Mathlib.Analysis.Convex.Join Mathlib.Analysis.Convex.Mul Mathlib.Analysis.Convex.PartitionOfUnity Mathlib.Analysis.Convex.PathConnected Mathlib.Analysis.Convex.Piecewise Mathlib.Analysis.Convex.Quasiconvex Mathlib.Analysis.Convex.Segment Mathlib.Analysis.Convex.SimplicialComplex.Basic Mathlib.Analysis.Convex.Slope Mathlib.Analysis.Convex.Star Mathlib.Analysis.Convex.StoneSeparation Mathlib.Analysis.Convex.StrictConvexSpace Mathlib.Analysis.Convex.Strict Mathlib.Analysis.Convex.Topology Mathlib.Analysis.Convex.TotallyBounded Mathlib.Analysis.Convex.Uniform Mathlib.Analysis.Hofer Mathlib.Analysis.LConvolution Mathlib.Analysis.LocallyConvex.AbsConvex Mathlib.Analysis.LocallyConvex.BalancedCoreHull Mathlib.Analysis.LocallyConvex.Barrelled Mathlib.Analysis.LocallyConvex.Basic Mathlib.Analysis.LocallyConvex.Bounded Mathlib.Analysis.LocallyConvex.Polar Mathlib.Analysis.LocallyConvex.StrongTopology Mathlib.Analysis.LocallyConvex.WeakDual Mathlib.Analysis.LocallyConvex.WithSeminorms Mathlib.Analysis.Normed.Affine.AddTorsor Mathlib.Analysis.Normed.Affine.ContinuousAffineMap Mathlib.Analysis.Normed.Affine.Isometry Mathlib.Analysis.Normed.Affine.MazurUlam Mathlib.Analysis.Normed.Affine.Simplex Mathlib.Analysis.Normed.Algebra.Ultra Mathlib.Analysis.Normed.Algebra.Unitization Mathlib.Analysis.Normed.Field.Basic Mathlib.Analysis.Normed.Field.Instances Mathlib.Analysis.Normed.Field.Lemmas Mathlib.Analysis.Normed.Field.ProperSpace Mathlib.Analysis.Normed.Field.Ultra Mathlib.Analysis.Normed.Field.UnitBall Mathlib.Analysis.Normed.Field.WithAbs Mathlib.Analysis.Normed.Group.AddTorsor Mathlib.Analysis.Normed.Group.BallSphere Mathlib.Analysis.Normed.Group.Bounded Mathlib.Analysis.Normed.Group.Completeness Mathlib.Analysis.Normed.Group.Completion Mathlib.Analysis.Normed.Group.Continuity Mathlib.Analysis.Normed.Group.ControlledClosure Mathlib.Analysis.Normed.Group.HomCompletion Mathlib.Analysis.Normed.Group.Hom Mathlib.Analysis.Normed.Group.InfiniteSum Mathlib.Analysis.Normed.Group.Lemmas Mathlib.Analysis.Normed.Group.NullSubmodule Mathlib.Analysis.Normed.Group.Pointwise Mathlib.Analysis.Normed.Group.Rat Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion Mathlib.Analysis.Normed.Group.SemiNormedGrp Mathlib.Analysis.Normed.Group.SeparationQuotient Mathlib.Analysis.Normed.Group.Ultra Mathlib.Analysis.Normed.Group.Uniform Mathlib.Analysis.Normed.Module.Basic Mathlib.Analysis.Normed.Module.Completion Mathlib.Analysis.Normed.Module.Convex Mathlib.Analysis.Normed.Module.Ray Mathlib.Analysis.Normed.Module.Span Mathlib.Analysis.Normed.MulAction Mathlib.Analysis.Normed.Operator.BanachSteinhaus Mathlib.Analysis.Normed.Operator.Banach Mathlib.Analysis.Normed.Operator.Compact Mathlib.Analysis.Normed.Operator.ContinuousLinearMap Mathlib.Analysis.Normed.Operator.LinearIsometry Mathlib.Analysis.Normed.Order.Lattice Mathlib.Analysis.Normed.Order.UpperLower Mathlib.Analysis.Normed.Ring.Basic Mathlib.Analysis.Normed.Ring.InfiniteSum Mathlib.Analysis.Normed.Ring.Lemmas Mathlib.Analysis.Normed.Ring.Ultra Mathlib.Analysis.Normed.Ring.WithAbs Mathlib.Analysis.NormedSpace.Alternating.Basic Mathlib.Analysis.NormedSpace.Alternating.Curry Mathlib.Analysis.NormedSpace.BallAction Mathlib.Analysis.NormedSpace.ConformalLinearMap Mathlib.Analysis.NormedSpace.ENormedSpace Mathlib.Analysis.NormedSpace.Extr Mathlib.Analysis.NormedSpace.FunctionSeries Mathlib.Analysis.NormedSpace.HomeomorphBall Mathlib.Analysis.NormedSpace.Int Mathlib.Analysis.NormedSpace.Multilinear.Basic Mathlib.Analysis.NormedSpace.Multilinear.Curry Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics Mathlib.Analysis.NormedSpace.OperatorNorm.Basic Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness Mathlib.Analysis.NormedSpace.OperatorNorm.Mul Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace Mathlib.Analysis.NormedSpace.OperatorNorm.Prod Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm Mathlib.Analysis.NormedSpace.Pointwise Mathlib.Analysis.NormedSpace.Real Mathlib.Analysis.NormedSpace.RieszLemma Mathlib.Analysis.NormedSpace.SphereNormEquiv Mathlib.Analysis.Polynomial.Basic Mathlib.Analysis.Polynomial.CauchyBound Mathlib.Analysis.Seminorm Mathlib.Analysis.SpecialFunctions.Choose Mathlib.Analysis.SpecialFunctions.Log.ERealExp Mathlib.Analysis.SpecificLimits.Basic Mathlib.Analysis.SpecificLimits.Normed Mathlib.Analysis.Subadditive Mathlib.Analysis.SumOverResidueClass Mathlib.CategoryTheory.Abelian.CommSq Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel Mathlib.CategoryTheory.Abelian.Exact Mathlib.CategoryTheory.Abelian.Ext Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject Mathlib.CategoryTheory.Abelian.Indization Mathlib.CategoryTheory.Abelian.Injective.Basic Mathlib.CategoryTheory.Abelian.Injective.Resolution Mathlib.CategoryTheory.Abelian.LeftDerived Mathlib.CategoryTheory.Abelian.Opposite Mathlib.CategoryTheory.Abelian.Projective.Basic Mathlib.CategoryTheory.Abelian.Projective.Dimension Mathlib.CategoryTheory.Abelian.Projective.Resolution Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Abelian.Refinements Mathlib.CategoryTheory.Abelian.RightDerived Mathlib.CategoryTheory.Abelian.SerreClass.Basic Mathlib.CategoryTheory.Abelian.Transfer Mathlib.CategoryTheory.Abelian.Yoneda Mathlib.CategoryTheory.Action.Limits Mathlib.CategoryTheory.Action.Monoidal Mathlib.CategoryTheory.Adjunction.Additive Mathlib.CategoryTheory.Galois.Action Mathlib.CategoryTheory.Galois.Basic Mathlib.CategoryTheory.Galois.Decomposition Mathlib.CategoryTheory.Galois.Equivalence Mathlib.CategoryTheory.Galois.EssSurj Mathlib.CategoryTheory.Galois.Examples Mathlib.CategoryTheory.Galois.Full Mathlib.CategoryTheory.Galois.GaloisObjects Mathlib.CategoryTheory.Galois.IsFundamentalgroup Mathlib.CategoryTheory.Galois.Prorepresentability Mathlib.CategoryTheory.Galois.Topology Mathlib.CategoryTheory.Generator.Abelian Mathlib.CategoryTheory.Generator.Indization Mathlib.CategoryTheory.Generator.Preadditive Mathlib.CategoryTheory.Linear.Yoneda Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive Mathlib.CategoryTheory.Localization.Triangulated Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_ Mathlib.CategoryTheory.Monoidal.Cartesian.CommMon_ Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_ Mathlib.CategoryTheory.Monoidal.Cartesian.Mon_ Mathlib.CategoryTheory.Monoidal.CommGrp_ Mathlib.CategoryTheory.Monoidal.Grp_ Mathlib.CategoryTheory.Monoidal.Internal.Module Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_ Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp_ Mathlib.CategoryTheory.Monoidal.Tor Mathlib.CategoryTheory.ObjectProperty.EpiMono Mathlib.CategoryTheory.ObjectProperty.Extensions Mathlib.CategoryTheory.Preadditive.CommGrp_ Mathlib.CategoryTheory.Preadditive.Indization Mathlib.CategoryTheory.Preadditive.Injective.Resolution Mathlib.CategoryTheory.Preadditive.Opposite Mathlib.CategoryTheory.Preadditive.Projective.Resolution Mathlib.CategoryTheory.Preadditive.Transfer Mathlib.CategoryTheory.Preadditive.Yoneda.Basic Mathlib.CategoryTheory.Preadditive.Yoneda.Injective Mathlib.CategoryTheory.Preadditive.Yoneda.Limits Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.CategoryTheory.Shift.Opposite Mathlib.CategoryTheory.Shift.ShiftedHomOpposite Mathlib.CategoryTheory.Sites.Abelian Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.CategoryTheory.Subobject.NoetherianObject Mathlib.CategoryTheory.Triangulated.Adjunction Mathlib.CategoryTheory.Triangulated.Functor Mathlib.CategoryTheory.Triangulated.HomologicalFunctor Mathlib.CategoryTheory.Triangulated.Opposite.Basic Mathlib.CategoryTheory.Triangulated.Opposite.Functor Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated Mathlib.CategoryTheory.Triangulated.Opposite.Triangle Mathlib.CategoryTheory.Triangulated.Pretriangulated Mathlib.CategoryTheory.Triangulated.Subcategory Mathlib.CategoryTheory.Triangulated.TStructure.Basic Mathlib.CategoryTheory.Triangulated.TriangleShift Mathlib.CategoryTheory.Triangulated.Triangulated Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.Combinatorics.Additive.CauchyDavenport Mathlib.Combinatorics.Optimization.ValuedCSP Mathlib.Combinatorics.SimpleGraph.AdjMatrix Mathlib.Combinatorics.SimpleGraph.Bipartite Mathlib.Combinatorics.SimpleGraph.DegreeSum Mathlib.Combinatorics.SimpleGraph.Matching Mathlib.Combinatorics.SimpleGraph.StronglyRegular Mathlib.Combinatorics.SimpleGraph.Tutte Mathlib.Combinatorics.SimpleGraph.UniversalVerts Mathlib.Condensed.AB Mathlib.Condensed.Basic Mathlib.Condensed.CartesianClosed Mathlib.Condensed.Discrete.Basic Mathlib.Condensed.Discrete.Characterization Mathlib.Condensed.Discrete.Colimit Mathlib.Condensed.Discrete.LocallyConstant Mathlib.Condensed.Discrete.Module Mathlib.Condensed.Epi Mathlib.Condensed.Equivalence Mathlib.Condensed.Explicit Mathlib.Condensed.Functors Mathlib.Condensed.Light.AB Mathlib.Condensed.Light.Basic Mathlib.Condensed.Light.CartesianClosed Mathlib.Condensed.Light.Epi Mathlib.Condensed.Light.Explicit Mathlib.Condensed.Light.Functors Mathlib.Condensed.Light.Limits Mathlib.Condensed.Light.Module Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.Limits Mathlib.Condensed.Module Mathlib.Condensed.Solid Mathlib.Condensed.TopCatAdjunction Mathlib.Condensed.TopComparison Mathlib.Data.Complex.Cardinality Mathlib.Data.Complex.Exponential Mathlib.Data.Complex.Norm Mathlib.Data.Complex.Order Mathlib.Data.Complex.Trigonometric Mathlib.Data.Finsupp.MonomialOrder.DegLex Mathlib.Data.Finsupp.Weight Mathlib.Data.Matrix.Auto Mathlib.Data.Matrix.Basic Mathlib.Data.Matrix.Basis Mathlib.Data.Matrix.Bilinear Mathlib.Data.Matrix.Block Mathlib.Data.Matrix.ColumnRowPartitioned Mathlib.Data.Matrix.Composition Mathlib.Data.Matrix.ConjTranspose Mathlib.Data.Matrix.DoublyStochastic Mathlib.Data.Matrix.DualNumber Mathlib.Data.Matrix.Hadamard Mathlib.Data.Matrix.Invertible Mathlib.Data.Matrix.Kronecker Mathlib.Data.Matrix.Notation Mathlib.Data.Matrix.Reflection Mathlib.Data.Matrix.RowCol Mathlib.Data.Matrix.Vec Mathlib.Data.Nat.Choose.Cast Mathlib.Data.Nat.Choose.Vandermonde Mathlib.Data.Nat.Factorial.Cast Mathlib.Data.Nat.Periodic Mathlib.Data.Nat.Totient Mathlib.Data.Real.Cardinality Mathlib.Data.Real.CompleteField Mathlib.Data.Real.Hyperreal Mathlib.Data.Real.Sqrt Mathlib.Data.Real.StarOrdered Mathlib.Data.ZMod.Aut Mathlib.Data.ZMod.Basic Mathlib.Data.ZMod.Factorial Mathlib.Data.ZMod.IntUnitsPower Mathlib.Data.ZMod.QuotientGroup Mathlib.Data.ZMod.Units Mathlib.Data.ZMod.ValMinAbs Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber Mathlib.Dynamics.Ergodic.Action.Basic Mathlib.Dynamics.Ergodic.Action.Regular Mathlib.Dynamics.Ergodic.Conservative Mathlib.Dynamics.Ergodic.Ergodic Mathlib.Dynamics.Ergodic.Function Mathlib.Dynamics.Ergodic.MeasurePreserving Mathlib.FieldTheory.RatFunc.Defs Mathlib.Geometry.Convex.Cone.Basic Mathlib.Geometry.Manifold.ChartedSpace Mathlib.Geometry.Manifold.LocalInvariantProperties Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.Geometry.RingedSpace.Basic Mathlib.GroupTheory.CommutingProbability Mathlib.GroupTheory.CosetCover Mathlib.GroupTheory.Coxeter.Basic Mathlib.GroupTheory.Coxeter.Inversion Mathlib.GroupTheory.Coxeter.Length Mathlib.GroupTheory.Coxeter.Matrix Mathlib.GroupTheory.Exponent Mathlib.GroupTheory.FixedPointFree Mathlib.GroupTheory.Frattini Mathlib.GroupTheory.GroupAction.Iwasawa Mathlib.GroupTheory.GroupAction.MultipleTransitivity Mathlib.GroupTheory.GroupAction.Period Mathlib.GroupTheory.GroupAction.Primitive Mathlib.GroupTheory.Nilpotent Mathlib.GroupTheory.Order.Min Mathlib.GroupTheory.PGroup Mathlib.GroupTheory.Perm.Centralizer Mathlib.GroupTheory.Perm.Closure Mathlib.GroupTheory.Perm.ConjAct Mathlib.GroupTheory.Perm.Cycle.Basic Mathlib.GroupTheory.Perm.Cycle.Concrete Mathlib.GroupTheory.Perm.Cycle.Factors Mathlib.GroupTheory.Perm.Cycle.PossibleTypes Mathlib.GroupTheory.Perm.Cycle.Type Mathlib.GroupTheory.Perm.Fin Mathlib.GroupTheory.Schreier Mathlib.GroupTheory.SchurZassenhaus Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer Mathlib.GroupTheory.SpecificGroups.Alternating Mathlib.GroupTheory.SpecificGroups.Cyclic Mathlib.GroupTheory.SpecificGroups.Dihedral Mathlib.GroupTheory.SpecificGroups.KleinFour Mathlib.GroupTheory.SpecificGroups.Quaternion Mathlib.GroupTheory.Sylow Mathlib.GroupTheory.Torsion Mathlib.GroupTheory.Transfer Mathlib.LinearAlgebra.AffineSpace.AffineEquiv Mathlib.LinearAlgebra.AffineSpace.AffineMap Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic Mathlib.LinearAlgebra.AffineSpace.Basis Mathlib.LinearAlgebra.AffineSpace.Combination Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv Mathlib.LinearAlgebra.AffineSpace.Independent Mathlib.LinearAlgebra.AffineSpace.MidpointZero Mathlib.LinearAlgebra.AffineSpace.Midpoint Mathlib.LinearAlgebra.AffineSpace.Ordered Mathlib.LinearAlgebra.AffineSpace.Pointwise Mathlib.LinearAlgebra.AffineSpace.Restrict Mathlib.LinearAlgebra.AffineSpace.Slope Mathlib.LinearAlgebra.Alternating.Basic Mathlib.LinearAlgebra.Alternating.Curry Mathlib.LinearAlgebra.Alternating.DomCoprod Mathlib.LinearAlgebra.Alternating.Uncurry.Fin Mathlib.LinearAlgebra.Basis.Basic Mathlib.LinearAlgebra.Basis.Bilinear Mathlib.LinearAlgebra.Basis.Cardinality Mathlib.LinearAlgebra.Basis.Defs Mathlib.LinearAlgebra.Basis.Exact Mathlib.LinearAlgebra.Basis.Fin Mathlib.LinearAlgebra.Basis.Flag Mathlib.LinearAlgebra.Basis.Prod Mathlib.LinearAlgebra.Basis.SMul Mathlib.LinearAlgebra.Basis.Submodule Mathlib.LinearAlgebra.Basis.VectorSpace Mathlib.LinearAlgebra.BilinearForm.Basic Mathlib.LinearAlgebra.BilinearForm.Hom Mathlib.LinearAlgebra.BilinearMap Mathlib.LinearAlgebra.Countable Mathlib.LinearAlgebra.CrossProduct Mathlib.LinearAlgebra.DFinsupp Mathlib.LinearAlgebra.Dimension.Basic Mathlib.LinearAlgebra.Dimension.Finrank Mathlib.LinearAlgebra.Dimension.Subsingleton Mathlib.LinearAlgebra.DirectSum.Basis Mathlib.LinearAlgebra.DirectSum.Finsupp Mathlib.LinearAlgebra.DirectSum.TensorProduct Mathlib.LinearAlgebra.Dual.Basis Mathlib.LinearAlgebra.Dual.Defs Mathlib.LinearAlgebra.FiniteSpan Mathlib.LinearAlgebra.Finsupp.LinearCombination Mathlib.LinearAlgebra.Finsupp.Pi Mathlib.LinearAlgebra.Finsupp.Span Mathlib.LinearAlgebra.Finsupp.Supported Mathlib.LinearAlgebra.Finsupp.VectorSpace Mathlib.LinearAlgebra.FreeModule.Basic Mathlib.LinearAlgebra.Goursat Mathlib.LinearAlgebra.Isomorphisms Mathlib.LinearAlgebra.LinearIndependent.Basic Mathlib.LinearAlgebra.LinearIndependent.Defs Mathlib.LinearAlgebra.LinearIndependent.Lemmas Mathlib.LinearAlgebra.LinearPMap Mathlib.LinearAlgebra.Matrix.AbsoluteValue Mathlib.LinearAlgebra.Matrix.Circulant Mathlib.LinearAlgebra.Matrix.Determinant.Basic Mathlib.LinearAlgebra.Matrix.Determinant.Misc Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular Mathlib.LinearAlgebra.Matrix.DotProduct Mathlib.LinearAlgebra.Matrix.IsDiag Mathlib.LinearAlgebra.Matrix.MvPolynomial Mathlib.LinearAlgebra.Matrix.Permanent Mathlib.LinearAlgebra.Matrix.Permutation Mathlib.LinearAlgebra.Matrix.Polynomial Mathlib.LinearAlgebra.Matrix.Reindex Mathlib.LinearAlgebra.Matrix.StdBasis Mathlib.LinearAlgebra.Matrix.Symmetric Mathlib.LinearAlgebra.Matrix.Trace Mathlib.LinearAlgebra.Matrix.Transvection Mathlib.LinearAlgebra.Matrix.Unique Mathlib.LinearAlgebra.Multilinear.Basic Mathlib.LinearAlgebra.Multilinear.Basis Mathlib.LinearAlgebra.Multilinear.Curry Mathlib.LinearAlgebra.Multilinear.DFinsupp Mathlib.LinearAlgebra.Multilinear.Pi Mathlib.LinearAlgebra.Multilinear.TensorProduct Mathlib.LinearAlgebra.PiTensorProduct Mathlib.LinearAlgebra.Pi Mathlib.LinearAlgebra.Prod Mathlib.LinearAlgebra.Projection Mathlib.LinearAlgebra.Quotient.Basic Mathlib.LinearAlgebra.Quotient.Pi Mathlib.LinearAlgebra.Ray Mathlib.LinearAlgebra.SModEq Mathlib.LinearAlgebra.SesquilinearForm Mathlib.LinearAlgebra.Span.Basic Mathlib.LinearAlgebra.StdBasis Mathlib.LinearAlgebra.TensorPower.Basic Mathlib.LinearAlgebra.TensorPower.Pairing Mathlib.LinearAlgebra.TensorProduct.Associator Mathlib.LinearAlgebra.TensorProduct.Basic Mathlib.LinearAlgebra.TensorProduct.Basis Mathlib.LinearAlgebra.TensorProduct.DirectLimit Mathlib.LinearAlgebra.TensorProduct.Graded.External Mathlib.LinearAlgebra.TensorProduct.Graded.Internal Mathlib.LinearAlgebra.TensorProduct.Opposite Mathlib.LinearAlgebra.TensorProduct.Pi Mathlib.LinearAlgebra.TensorProduct.Prod Mathlib.LinearAlgebra.TensorProduct.Subalgebra Mathlib.LinearAlgebra.TensorProduct.Submodule Mathlib.LinearAlgebra.TensorProduct.Tower Mathlib.MeasureTheory.Category.MeasCat Mathlib.MeasureTheory.Constructions.AddChar Mathlib.MeasureTheory.Constructions.BorelSpace.Basic Mathlib.MeasureTheory.Constructions.BorelSpace.Metric Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable Mathlib.MeasureTheory.Constructions.BorelSpace.Order Mathlib.MeasureTheory.Constructions.BorelSpace.Real Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders Mathlib.MeasureTheory.Constructions.Pi Mathlib.MeasureTheory.Constructions.Polish.Basic Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent Mathlib.MeasureTheory.Constructions.Projective Mathlib.MeasureTheory.Covering.VitaliFamily Mathlib.MeasureTheory.Covering.Vitali Mathlib.MeasureTheory.Function.AEEqFun Mathlib.MeasureTheory.Function.AEEqOfLIntegral Mathlib.MeasureTheory.Function.AEMeasurableOrder Mathlib.MeasureTheory.Function.AEMeasurableSequence Mathlib.MeasureTheory.Function.Egorov Mathlib.MeasureTheory.Function.EssSup Mathlib.MeasureTheory.Function.Floor Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral Mathlib.MeasureTheory.Function.SimpleFuncDense Mathlib.MeasureTheory.Function.SimpleFunc Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal Mathlib.MeasureTheory.Group.AEStabilizer Mathlib.MeasureTheory.Group.Action Mathlib.MeasureTheory.Group.Arithmetic Mathlib.MeasureTheory.Group.Convolution Mathlib.MeasureTheory.Group.Defs Mathlib.MeasureTheory.Group.LIntegral Mathlib.MeasureTheory.Group.MeasurableEquiv Mathlib.MeasureTheory.Group.Measure Mathlib.MeasureTheory.Group.Pointwise Mathlib.MeasureTheory.Group.Prod Mathlib.MeasureTheory.Integral.Indicator Mathlib.MeasureTheory.Integral.Lebesgue.Add Mathlib.MeasureTheory.Integral.Lebesgue.Basic Mathlib.MeasureTheory.Integral.Lebesgue.Countable Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence Mathlib.MeasureTheory.Integral.Lebesgue.Map Mathlib.MeasureTheory.Integral.Lebesgue.Markov Mathlib.MeasureTheory.Integral.Lebesgue.MeasurePreserving Mathlib.MeasureTheory.Integral.Lebesgue.Norm Mathlib.MeasureTheory.Integral.Lebesgue.Sub Mathlib.MeasureTheory.Integral.LebesgueNormedSpace Mathlib.MeasureTheory.Integral.Lebesgue Mathlib.MeasureTheory.Integral.Marginal Mathlib.MeasureTheory.Measure.AEDisjoint Mathlib.MeasureTheory.Measure.AEMeasurable Mathlib.MeasureTheory.Measure.AbsolutelyContinuous Mathlib.MeasureTheory.Measure.AddContent Mathlib.MeasureTheory.Measure.Comap Mathlib.MeasureTheory.Measure.Content Mathlib.MeasureTheory.Measure.ContinuousPreimage Mathlib.MeasureTheory.Measure.Count Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion Mathlib.MeasureTheory.Measure.Decomposition.Hahn Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue Mathlib.MeasureTheory.Measure.Dirac Mathlib.MeasureTheory.Measure.EverywherePos Mathlib.MeasureTheory.Measure.GiryMonad Mathlib.MeasureTheory.Measure.Haar.Basic Mathlib.MeasureTheory.Measure.Map Mathlib.MeasureTheory.Measure.MeasureSpaceDef Mathlib.MeasureTheory.Measure.MeasureSpace Mathlib.MeasureTheory.Measure.MutuallySingular Mathlib.MeasureTheory.Measure.NullMeasurable Mathlib.MeasureTheory.Measure.OpenPos Mathlib.MeasureTheory.Measure.Prod Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving Mathlib.MeasureTheory.Measure.Real Mathlib.MeasureTheory.Measure.Regular Mathlib.MeasureTheory.Measure.RegularityCompacts Mathlib.MeasureTheory.Measure.Restrict Mathlib.MeasureTheory.Measure.Stieltjes Mathlib.MeasureTheory.Measure.Sub Mathlib.MeasureTheory.Measure.Tight Mathlib.MeasureTheory.Measure.Trim Mathlib.MeasureTheory.Measure.Typeclasses.Finite Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms Mathlib.MeasureTheory.Measure.Typeclasses.Probability Mathlib.MeasureTheory.Measure.Typeclasses.SFinite Mathlib.MeasureTheory.Measure.Typeclasses Mathlib.MeasureTheory.Measure.WithDensityFinite Mathlib.MeasureTheory.Measure.WithDensity Mathlib.MeasureTheory.Order.Group.Lattice Mathlib.MeasureTheory.Order.Lattice Mathlib.MeasureTheory.OuterMeasure.AE Mathlib.MeasureTheory.OuterMeasure.Basic Mathlib.MeasureTheory.OuterMeasure.BorelCantelli Mathlib.MeasureTheory.OuterMeasure.Caratheodory Mathlib.MeasureTheory.OuterMeasure.Induced Mathlib.MeasureTheory.OuterMeasure.OfAddContent Mathlib.MeasureTheory.OuterMeasure.OfFunction Mathlib.MeasureTheory.OuterMeasure.Operations Mathlib.MeasureTheory.Topology Mathlib.MeasureTheory.VectorMeasure.Basic Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan Mathlib.ModelTheory.Algebra.Field.CharP Mathlib.ModelTheory.Algebra.Ring.FreeCommRing Mathlib.NumberTheory.ClassNumber.AdmissibleAbs Mathlib.NumberTheory.DirichletCharacter.Basic Mathlib.NumberTheory.EulerProduct.Basic Mathlib.NumberTheory.LegendreSymbol.ZModChar Mathlib.NumberTheory.LucasLehmer Mathlib.NumberTheory.LucasPrimality Mathlib.NumberTheory.PrimeCounting Mathlib.NumberTheory.SelbergSieve Mathlib.Order.Filter.ENNReal Mathlib.Order.Filter.ZeroAndBoundedAtFilter Mathlib.Probability.ConditionalProbability Mathlib.Probability.Distributions.Geometric Mathlib.Probability.Independence.Basic Mathlib.Probability.Independence.Kernel Mathlib.Probability.Kernel.Basic Mathlib.Probability.Kernel.Composition.CompMap Mathlib.Probability.Kernel.Composition.CompNotation Mathlib.Probability.Kernel.Composition.CompProd Mathlib.Probability.Kernel.Composition.Comp Mathlib.Probability.Kernel.Composition.Lemmas Mathlib.Probability.Kernel.Composition.MapComap Mathlib.Probability.Kernel.Composition.MeasureCompProd Mathlib.Probability.Kernel.Composition.MeasureComp Mathlib.Probability.Kernel.Composition.ParallelComp Mathlib.Probability.Kernel.Composition.Prod Mathlib.Probability.Kernel.Defs Mathlib.Probability.Kernel.Disintegration.Basic Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes Mathlib.Probability.Kernel.Invariance Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj Mathlib.Probability.Kernel.MeasurableLIntegral Mathlib.Probability.Kernel.Proper Mathlib.Probability.ProbabilityMassFunction.Basic Mathlib.Probability.ProbabilityMassFunction.Binomial Mathlib.Probability.ProbabilityMassFunction.Constructions Mathlib.Probability.ProbabilityMassFunction.Monad Mathlib.Probability.UniformOn Mathlib.RingTheory.Adjoin.Basic Mathlib.RingTheory.Adjoin.Polynomial Mathlib.RingTheory.AlgebraTower Mathlib.RingTheory.Algebraic.Cardinality Mathlib.RingTheory.Algebraic.Defs Mathlib.RingTheory.Algebraic.LinearIndependent Mathlib.RingTheory.Algebraic.Pi Mathlib.RingTheory.AlgebraicIndependent.Defs Mathlib.RingTheory.Binomial Mathlib.RingTheory.Derivation.Basic Mathlib.RingTheory.Derivation.DifferentialRing Mathlib.RingTheory.Fintype Mathlib.RingTheory.FreeCommRing Mathlib.RingTheory.GradedAlgebra.Basic Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule Mathlib.RingTheory.HahnSeries.Multiplication Mathlib.RingTheory.HahnSeries.Summable Mathlib.RingTheory.IntegralClosure.Algebra.Defs Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs Mathlib.RingTheory.IntegralDomain Mathlib.RingTheory.IsTensorProduct Mathlib.RingTheory.Localization.Basic Mathlib.RingTheory.Localization.Cardinality Mathlib.RingTheory.Localization.FractionRing Mathlib.RingTheory.Localization.Module Mathlib.RingTheory.Localization.NumDen Mathlib.RingTheory.Localization.Pi Mathlib.RingTheory.MatrixAlgebra Mathlib.RingTheory.MatrixPolynomialAlgebra Mathlib.RingTheory.Morita.Basic Mathlib.RingTheory.MvPolynomial.EulerIdentity Mathlib.RingTheory.MvPolynomial.FreeCommRing Mathlib.RingTheory.MvPolynomial.Groebner Mathlib.RingTheory.MvPolynomial.Homogeneous Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex Mathlib.RingTheory.MvPolynomial.MonomialOrder Mathlib.RingTheory.MvPolynomial.Symmetric.Defs Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities Mathlib.RingTheory.MvPolynomial.Tower Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous Mathlib.RingTheory.MvPowerSeries.Basic Mathlib.RingTheory.MvPowerSeries.LexOrder Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors Mathlib.RingTheory.MvPowerSeries.Order Mathlib.RingTheory.MvPowerSeries.Trunc Mathlib.RingTheory.Nilpotent.Exp Mathlib.RingTheory.PiTensorProduct Mathlib.RingTheory.Polynomial.Bernstein Mathlib.RingTheory.Polynomial.Chebyshev Mathlib.RingTheory.Polynomial.Dickson Mathlib.RingTheory.Polynomial.Hermite.Basic Mathlib.RingTheory.Polynomial.IntegralNormalization Mathlib.RingTheory.Polynomial.Opposites Mathlib.RingTheory.Polynomial.Pochhammer Mathlib.RingTheory.Polynomial.ScaleRoots Mathlib.RingTheory.Polynomial.ShiftedLegendre Mathlib.RingTheory.Polynomial.Tower Mathlib.RingTheory.Polynomial.Wronskian Mathlib.RingTheory.PolynomialAlgebra Mathlib.RingTheory.PolynomialLaw.Basic Mathlib.RingTheory.RootsOfUnity.Basic Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots Mathlib.RingTheory.TensorProduct.Basic Mathlib.RingTheory.TensorProduct.MvPolynomial Mathlib.RingTheory.TensorProduct.Pi Mathlib.RingTheory.WittVector.WittPolynomial Mathlib.SetTheory.Cardinal.Free Mathlib.Tactic.Algebraize Mathlib.Tactic.ComputeDegree Mathlib.Tactic.Module Mathlib.Tactic.NormNum.RealSqrt Mathlib.Topology.Algebra.AffineSubspace Mathlib.Topology.Algebra.Affine Mathlib.Topology.Algebra.Algebra.Equiv Mathlib.Topology.Algebra.Algebra Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits Mathlib.Topology.Algebra.ClopenNhdofOne Mathlib.Topology.Algebra.ClosedSubgroup Mathlib.Topology.Algebra.ContinuousAffineMap Mathlib.Topology.Algebra.Equicontinuity Mathlib.Topology.Algebra.Field Mathlib.Topology.Algebra.FilterBasis Mathlib.Topology.Algebra.Group.Basic Mathlib.Topology.Algebra.Group.ClosedSubgroup Mathlib.Topology.Algebra.Group.CompactOpen Mathlib.Topology.Algebra.Group.Compact Mathlib.Topology.Algebra.Group.GroupTopology Mathlib.Topology.Algebra.Group.OpenMapping Mathlib.Topology.Algebra.Group.Pointwise Mathlib.Topology.Algebra.Group.Quotient Mathlib.Topology.Algebra.Group.SubmonoidClosure Mathlib.Topology.Algebra.Group.TopologicalAbelianization Mathlib.Topology.Algebra.GroupCompletion Mathlib.Topology.Algebra.InfiniteSum.Constructions Mathlib.Topology.Algebra.InfiniteSum.ENNReal Mathlib.Topology.Algebra.InfiniteSum.Field Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion Mathlib.Topology.Algebra.InfiniteSum.Group Mathlib.Topology.Algebra.InfiniteSum.Module Mathlib.Topology.Algebra.InfiniteSum.NatInt Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean Mathlib.Topology.Algebra.InfiniteSum.Order Mathlib.Topology.Algebra.InfiniteSum.Real Mathlib.Topology.Algebra.InfiniteSum.Ring Mathlib.Topology.Algebra.InfiniteSum.UniformOn Mathlib.Topology.Algebra.IsUniformGroup.Basic Mathlib.Topology.Algebra.IsUniformGroup.Defs Mathlib.Topology.Algebra.IsUniformGroup.Order Mathlib.Topology.Algebra.LinearTopology Mathlib.Topology.Algebra.Localization Mathlib.Topology.Algebra.Module.Alternating.Basic Mathlib.Topology.Algebra.Module.Alternating.Topology Mathlib.Topology.Algebra.Module.Basic Mathlib.Topology.Algebra.Module.Cardinality Mathlib.Topology.Algebra.Module.ClosedSubmodule Mathlib.Topology.Algebra.Module.Equiv Mathlib.Topology.Algebra.Module.LinearMapPiProd Mathlib.Topology.Algebra.Module.LinearMap Mathlib.Topology.Algebra.Module.LinearPMap Mathlib.Topology.Algebra.Module.LocallyConvex Mathlib.Topology.Algebra.Module.Multilinear.Basic Mathlib.Topology.Algebra.Module.Multilinear.Bounded Mathlib.Topology.Algebra.Module.Multilinear.Topology Mathlib.Topology.Algebra.Module.Star Mathlib.Topology.Algebra.Module.StrongTopology Mathlib.Topology.Algebra.Module.UniformConvergence Mathlib.Topology.Algebra.Module.WeakBilin Mathlib.Topology.Algebra.Module.WeakDual Mathlib.Topology.Algebra.Monoid.AddChar Mathlib.Topology.Algebra.MvPolynomial Mathlib.Topology.Algebra.NonUnitalAlgebra Mathlib.Topology.Algebra.NonUnitalStarAlgebra Mathlib.Topology.Algebra.Nonarchimedean.Bases Mathlib.Topology.Algebra.Nonarchimedean.Basic Mathlib.Topology.Algebra.Nonarchimedean.Completion Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected Mathlib.Topology.Algebra.OpenSubgroup Mathlib.Topology.Algebra.Order.Field Mathlib.Topology.Algebra.Order.LiminfLimsup Mathlib.Topology.Algebra.Order.UpperLower Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace Mathlib.Topology.Algebra.RestrictedProduct Mathlib.Topology.Algebra.Ring.Basic Mathlib.Topology.Algebra.Ring.Ideal Mathlib.Topology.Algebra.Ring.Real Mathlib.Topology.Algebra.SeparationQuotient.Basic Mathlib.Topology.Algebra.SeparationQuotient.Hom Mathlib.Topology.Algebra.SeparationQuotient.Section Mathlib.Topology.Algebra.StarSubalgebra Mathlib.Topology.Algebra.UniformConvergence Mathlib.Topology.Algebra.UniformField Mathlib.Topology.Algebra.UniformFilterBasis Mathlib.Topology.Algebra.UniformMulAction Mathlib.Topology.Algebra.UniformRing Mathlib.Topology.Baire.BaireMeasurable Mathlib.Topology.Baire.CompleteMetrizable Mathlib.Topology.Bornology.BoundedOperation Mathlib.Topology.CWComplex.Classical.Basic Mathlib.Topology.CWComplex.Classical.Finite Mathlib.Topology.Category.CompHaus.Basic Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.Topology.Category.CompHaus.Frm Mathlib.Topology.Category.CompHaus.Limits Mathlib.Topology.Category.CompHaus.Projective Mathlib.Topology.Category.CompactlyGenerated Mathlib.Topology.Category.Compactum Mathlib.Topology.Category.DeltaGenerated Mathlib.Topology.Category.LightProfinite.AsLimit Mathlib.Topology.Category.LightProfinite.Basic Mathlib.Topology.Category.LightProfinite.EffectiveEpi Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Topology.Category.LightProfinite.Limits Mathlib.Topology.Category.LightProfinite.Sequence Mathlib.Topology.Category.Locale Mathlib.Topology.Category.Profinite.AsLimit Mathlib.Topology.Category.Profinite.Basic Mathlib.Topology.Category.Profinite.CofilteredLimit Mathlib.Topology.Category.Profinite.EffectiveEpi Mathlib.Topology.Category.Profinite.Extend Mathlib.Topology.Category.Profinite.Limits Mathlib.Topology.Category.Profinite.Nobeling.Basic Mathlib.Topology.Category.Profinite.Nobeling.Span Mathlib.Topology.Category.Profinite.Nobeling.Successor Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit Mathlib.Topology.Category.Profinite.Product Mathlib.Topology.Category.Profinite.Projective Mathlib.Topology.Category.Stonean.Adjunctions Mathlib.Topology.Category.Stonean.Basic Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Topology.Category.Stonean.Limits Mathlib.Topology.Category.TopCommRingCat Mathlib.Topology.Compactness.CompactlyGeneratedSpace Mathlib.Topology.Compactness.DeltaGeneratedSpace Mathlib.Topology.Connected.LocPathConnected Mathlib.Topology.Connected.PathComponentOne Mathlib.Topology.Connected.PathConnected Mathlib.Topology.ContinuousMap.Algebra Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli Mathlib.Topology.ContinuousMap.Bounded.Basic Mathlib.Topology.ContinuousMap.Bounded.Normed Mathlib.Topology.ContinuousMap.BoundedCompactlySupported Mathlib.Topology.ContinuousMap.Lattice Mathlib.Topology.ContinuousMap.LocallyConstant Mathlib.Topology.ContinuousMap.LocallyConvex Mathlib.Topology.ContinuousMap.Periodic Mathlib.Topology.ContinuousMap.Star Mathlib.Topology.EMetricSpace.BoundedVariation Mathlib.Topology.GDelta.MetrizableSpace Mathlib.Topology.GDelta.UniformSpace Mathlib.Topology.Germ Mathlib.Topology.Homotopy.Basic Mathlib.Topology.Homotopy.Contractible Mathlib.Topology.Homotopy.Equiv Mathlib.Topology.Homotopy.HSpaces Mathlib.Topology.Homotopy.HomotopyGroup Mathlib.Topology.Homotopy.Lifting Mathlib.Topology.Homotopy.Path Mathlib.Topology.Homotopy.Product Mathlib.Topology.Instances.AddCircle.Defs Mathlib.Topology.Instances.AddCircle.Real Mathlib.Topology.Instances.CantorSet Mathlib.Topology.Instances.ENNReal.Lemmas Mathlib.Topology.Instances.EReal.Lemmas Mathlib.Topology.Instances.NNReal.Lemmas Mathlib.Topology.Instances.Rat Mathlib.Topology.Instances.Real.Lemmas Mathlib.Topology.Instances.RealVectorSpace Mathlib.Topology.Instances.TrivSqZeroExt Mathlib.Topology.Instances.ZMultiples Mathlib.Topology.LocallyConstant.Algebra Mathlib.Topology.Maps.Proper.CompactlyGenerated Mathlib.Topology.MetricSpace.Algebra Mathlib.Topology.MetricSpace.Bilipschitz Mathlib.Topology.MetricSpace.CantorScheme Mathlib.Topology.MetricSpace.CauSeqFilter Mathlib.Topology.MetricSpace.Closeds Mathlib.Topology.MetricSpace.Completion Mathlib.Topology.MetricSpace.Contracting Mathlib.Topology.MetricSpace.DilationEquiv Mathlib.Topology.MetricSpace.Dilation Mathlib.Topology.MetricSpace.GromovHausdorffRealized Mathlib.Topology.MetricSpace.HausdorffDistance Mathlib.Topology.MetricSpace.IsometricSMul Mathlib.Topology.MetricSpace.Lipschitz Mathlib.Topology.MetricSpace.PartitionOfUnity Mathlib.Topology.MetricSpace.Perfect Mathlib.Topology.MetricSpace.PiNat Mathlib.Topology.MetricSpace.Polish Mathlib.Topology.MetricSpace.ThickenedIndicator Mathlib.Topology.MetricSpace.Thickening Mathlib.Topology.Metrizable.Urysohn Mathlib.Topology.Order.Category.FrameAdjunction Mathlib.Topology.PartitionOfUnity Mathlib.Topology.Path Mathlib.Topology.Semicontinuous Mathlib.Topology.Separation.CompletelyRegular Mathlib.Topology.Separation.NotNormal Mathlib.Topology.Sheaves.MayerVietoris Mathlib.Topology.TietzeExtension Mathlib.Topology.UniformSpace.CompareReals Mathlib.Topology.UniformSpace.Dini Mathlib.Topology.UniformSpace.DiscreteUniformity Mathlib.Topology.UniformSpace.Matrix Mathlib.Topology.UniformSpace.ProdApproximation Mathlib.Topology.UnitInterval Mathlib.Topology.UrysohnsBounded Mathlib.Topology.UrysohnsLemma |
2 |
3 filesMathlib.Algebra.Category.Grp.Kernels Mathlib.Algebra.ModEq Mathlib.GroupTheory.ClassEquation |
3 |
Mathlib.Algebra.Module.Submodule.Invariant |
4 |
Mathlib.LinearAlgebra.Matrix.SemiringInverse Mathlib.RingTheory.Localization.Integer |
5 |
21 filesMathlib.Algebra.Order.Antidiag.Nat Mathlib.Algebra.Polynomial.Basic Mathlib.Algebra.Polynomial.Cardinal Mathlib.Algebra.Polynomial.Eval.Algebra Mathlib.Algebra.Polynomial.Eval.Defs Mathlib.Algebra.Polynomial.Monomial Mathlib.Algebra.Ring.CentroidHom Mathlib.Algebra.Squarefree.Basic Mathlib.Algebra.Star.CentroidHom Mathlib.Computability.TMComputable Mathlib.Data.Nat.Squarefree Mathlib.NumberTheory.ArithmeticFunction Mathlib.NumberTheory.MaricaSchoenheim Mathlib.NumberTheory.SmoothNumbers Mathlib.RingTheory.Localization.Defs Mathlib.RingTheory.OreLocalization.Cardinality Mathlib.RingTheory.Radical Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid Mathlib.SetTheory.Surreal.Dyadic |
6 |
18 filesMathlib.Algebra.DirectSum.Basic Mathlib.Algebra.DirectSum.Ring Mathlib.Algebra.MonoidAlgebra.Defs Mathlib.Algebra.MonoidAlgebra.Division Mathlib.Algebra.MonoidAlgebra.MapDomain Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors Mathlib.Algebra.SkewMonoidAlgebra.Basic Mathlib.Analysis.Normed.Group.Submodule Mathlib.Data.DFinsupp.Submonoid Mathlib.Dynamics.Flow Mathlib.Dynamics.OmegaLimit Mathlib.LinearAlgebra.Finsupp.LSum Mathlib.RingTheory.Nilpotent.Basic Mathlib.RingTheory.OreLocalization.Ring Mathlib.Topology.Algebra.GroupWithZero Mathlib.Topology.Algebra.Monoid Mathlib.Topology.Algebra.WithZeroTopology Mathlib.Topology.ApproximateUnit |
7 |
19 filesMathlib.Combinatorics.Enumerative.Bell Mathlib.Data.DFinsupp.Interval Mathlib.Data.Finsupp.Antidiagonal Mathlib.Data.Finsupp.Interval Mathlib.Data.Finsupp.MonomialOrder Mathlib.Data.Finsupp.Multiset Mathlib.Data.Finsupp.WellFounded Mathlib.Data.Multiset.Interval Mathlib.Data.Nat.Choose.Factorization Mathlib.Data.Nat.Choose.Multinomial Mathlib.Data.Nat.Factorization.Basic Mathlib.Data.Nat.Factorization.Defs Mathlib.Data.Nat.Factorization.Induction Mathlib.Data.Nat.Factorization.PrimePow Mathlib.Data.Nat.Factorization.Root Mathlib.Logic.Hydra Mathlib.SetTheory.Cardinal.Finsupp Mathlib.SetTheory.Surreal.Multiplication Mathlib.Topology.Algebra.Algebra.Rat |
9 |
7 filesMathlib.Algebra.Order.Floor.Div Mathlib.Analysis.Normed.Group.Subgroup Mathlib.Data.DFinsupp.BigOperators Mathlib.Data.DFinsupp.Multiset Mathlib.Data.Finsupp.Lex Mathlib.Data.Finsupp.Order Mathlib.Data.Finsupp.PWO |
10 |
70 filesMathlib.Algebra.BigOperators.Balance Mathlib.Algebra.BigOperators.Expect Mathlib.Algebra.Order.BigOperators.Expect Mathlib.AlgebraicTopology.MooreComplex Mathlib.Analysis.BoxIntegral.Box.Basic Mathlib.Analysis.BoxIntegral.Partition.Basic Mathlib.Analysis.BoxIntegral.Partition.Split Mathlib.Analysis.BoxIntegral.Partition.Tagged Mathlib.Analysis.Normed.Group.Basic Mathlib.Analysis.Normed.Group.CocompactMap Mathlib.Analysis.Normed.Group.Constructions Mathlib.Analysis.Normed.Group.Int Mathlib.Analysis.Normed.Order.Basic Mathlib.Analysis.Normed.Order.Hom.Basic Mathlib.Analysis.Normed.Order.Hom.Ultra Mathlib.Analysis.NormedSpace.IndicatorFunction Mathlib.Analysis.Oscillation Mathlib.CategoryTheory.Idempotents.SimplicialObject Mathlib.Data.Complex.BigOperators Mathlib.Data.ENNReal.BigOperators Mathlib.Data.EReal.Inv Mathlib.Data.NNReal.Basic Mathlib.InformationTheory.Hamming Mathlib.MeasureTheory.OuterMeasure.Defs Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue Mathlib.Topology.Algebra.Star.Real Mathlib.Topology.Bornology.Real Mathlib.Topology.Compactness.PseudometrizableLindelof Mathlib.Topology.EMetricSpace.Basic Mathlib.Topology.EMetricSpace.Defs Mathlib.Topology.EMetricSpace.Diam Mathlib.Topology.EMetricSpace.Lipschitz Mathlib.Topology.EMetricSpace.Paracompact Mathlib.Topology.EMetricSpace.Pi Mathlib.Topology.Instances.Int Mathlib.Topology.Instances.Nat Mathlib.Topology.Instances.PNat Mathlib.Topology.MetricSpace.Antilipschitz Mathlib.Topology.MetricSpace.Basic Mathlib.Topology.MetricSpace.Bounded Mathlib.Topology.MetricSpace.Cauchy Mathlib.Topology.MetricSpace.Congruence Mathlib.Topology.MetricSpace.Defs Mathlib.Topology.MetricSpace.Equicontinuity Mathlib.Topology.MetricSpace.Gluing Mathlib.Topology.MetricSpace.Infsep Mathlib.Topology.MetricSpace.Isometry Mathlib.Topology.MetricSpace.MetricSeparated Mathlib.Topology.MetricSpace.ProperSpace.Lemmas Mathlib.Topology.MetricSpace.ProperSpace.Real Mathlib.Topology.MetricSpace.ProperSpace Mathlib.Topology.MetricSpace.Pseudo.Basic Mathlib.Topology.MetricSpace.Pseudo.Constructions Mathlib.Topology.MetricSpace.Pseudo.Defs Mathlib.Topology.MetricSpace.Pseudo.Lemmas Mathlib.Topology.MetricSpace.Pseudo.Pi Mathlib.Topology.MetricSpace.Pseudo.Real Mathlib.Topology.MetricSpace.Sequences Mathlib.Topology.MetricSpace.ShrinkingLemma Mathlib.Topology.MetricSpace.Similarity Mathlib.Topology.MetricSpace.Ultra.Basic Mathlib.Topology.MetricSpace.Ultra.Pi Mathlib.Topology.MetricSpace.Ultra.TotallySeparated Mathlib.Topology.Metrizable.Basic Mathlib.Topology.Metrizable.CompletelyMetrizable Mathlib.Topology.Metrizable.ContinuousMap Mathlib.Topology.Metrizable.Real Mathlib.Topology.Metrizable.Uniformity Mathlib.Topology.Order.Real Mathlib.Topology.UniformSpace.Real |
13 |
78 filesMathlib.Algebra.Module.Card Mathlib.Analysis.Normed.Group.Seminorm Mathlib.CategoryTheory.Noetherian Mathlib.CategoryTheory.Simple Mathlib.CategoryTheory.Sites.Coherent.Basic Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology Mathlib.CategoryTheory.Sites.Coherent.Comparison Mathlib.CategoryTheory.Sites.Coherent.Equivalence Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves Mathlib.CategoryTheory.Sites.Coherent.RegularTopology Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit Mathlib.CategoryTheory.Sites.Coherent.SheafComparison Mathlib.CategoryTheory.Sites.ConstantSheaf Mathlib.CategoryTheory.Sites.DenseSubsite.Basic Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv Mathlib.CategoryTheory.Sites.EpiMono Mathlib.CategoryTheory.Sites.Equivalence Mathlib.CategoryTheory.Sites.GlobalSections Mathlib.CategoryTheory.Sites.LeftExact Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.CategoryTheory.Sites.Pullback Mathlib.Combinatorics.Enumerative.IncidenceAlgebra Mathlib.Combinatorics.Pigeonhole Mathlib.Combinatorics.SimpleGraph.IncMatrix Mathlib.Data.DFinsupp.WellFounded Mathlib.Data.ENNReal.Action Mathlib.Data.ENNReal.Basic Mathlib.Data.ENNReal.Holder Mathlib.Data.ENNReal.Inv Mathlib.Data.ENNReal.Lemmas Mathlib.Data.ENNReal.Operations Mathlib.Data.ENNReal.Order Mathlib.Data.ENNReal.Real Mathlib.Data.EReal.Basic Mathlib.Data.EReal.Operations Mathlib.Data.Int.WithZero Mathlib.Data.NNReal.Defs Mathlib.Data.NNReal.Star Mathlib.Data.Real.ConjExponents Mathlib.Data.Real.ENatENNReal Mathlib.Data.Real.EReal Mathlib.Data.Real.Pointwise Mathlib.Data.Setoid.Partition.Card Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.Geometry.RingedSpace.Stalks Mathlib.Topology.Algebra.InfiniteSum.Basic Mathlib.Topology.Algebra.InfiniteSum.Defs Mathlib.Topology.Category.CompHausLike.EffectiveEpi Mathlib.Topology.Sheaves.Alexandrov Mathlib.Topology.Sheaves.Forget Mathlib.Topology.Sheaves.Functors Mathlib.Topology.Sheaves.Limits Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Topology.Sheaves.PUnit Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.Topology.Sheaves.SheafCondition.Sites Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.Topology.Sheaves.Sheaf Mathlib.Topology.Sheaves.Sheafify Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.Sheaves.Stalks |
14 |
Mathlib.Data.DFinsupp.Lex Mathlib.NumberTheory.EllipticDivisibilitySequence |
15 |
13 filesMathlib.Algebra.Module.BigOperators Mathlib.Algebra.Order.Module.Rat Mathlib.Algebra.QuadraticDiscriminant Mathlib.CategoryTheory.Abelian.Monomorphisms Mathlib.CategoryTheory.Abelian.Subobject Mathlib.CategoryTheory.Idempotents.HomologicalComplex Mathlib.CategoryTheory.Preadditive.Mat Mathlib.CategoryTheory.Sites.Subsheaf Mathlib.Combinatorics.Enumerative.InclusionExclusion Mathlib.Data.Matrix.Mul Mathlib.Data.Matrix.PEquiv Mathlib.LinearAlgebra.Matrix.Integer Mathlib.LinearAlgebra.Matrix.Orthogonal |
16 |
42 filesMathlib.Algebra.BigOperators.Finprod Mathlib.Algebra.BigOperators.GroupWithZero.Action Mathlib.Algebra.Homology.ShortComplex.Abelian Mathlib.CategoryTheory.Abelian.Basic Mathlib.CategoryTheory.Abelian.FunctorCategory Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems Mathlib.CategoryTheory.Generator.Sheaf Mathlib.CategoryTheory.Idempotents.Basic Mathlib.CategoryTheory.Idempotents.Biproducts Mathlib.CategoryTheory.Idempotents.FunctorCategories Mathlib.CategoryTheory.Idempotents.FunctorExtension Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi Mathlib.CategoryTheory.Idempotents.Karoubi Mathlib.CategoryTheory.Preadditive.LeftExact Mathlib.CategoryTheory.Preadditive.LiftToFinset Mathlib.CategoryTheory.Sites.Adjunction Mathlib.CategoryTheory.Sites.Canonical Mathlib.CategoryTheory.Sites.CartesianClosed Mathlib.CategoryTheory.Sites.CartesianMonoidal Mathlib.CategoryTheory.Sites.ChosenFiniteProducts Mathlib.CategoryTheory.Sites.CompatiblePlus Mathlib.CategoryTheory.Sites.CompatibleSheafification Mathlib.CategoryTheory.Sites.ConcreteSheafification Mathlib.CategoryTheory.Sites.Continuous Mathlib.CategoryTheory.Sites.CoverLifting Mathlib.CategoryTheory.Sites.CoverPreserving Mathlib.CategoryTheory.Sites.Coverage Mathlib.CategoryTheory.Sites.CoversTop Mathlib.CategoryTheory.Sites.IsSheafOneHypercover Mathlib.CategoryTheory.Sites.Limits Mathlib.CategoryTheory.Sites.Localization Mathlib.CategoryTheory.Sites.Monoidal Mathlib.CategoryTheory.Sites.OneHypercover Mathlib.CategoryTheory.Sites.Over Mathlib.CategoryTheory.Sites.Plus Mathlib.CategoryTheory.Sites.PreservesSheafification Mathlib.CategoryTheory.Sites.SheafHom Mathlib.CategoryTheory.Sites.Sheaf Mathlib.CategoryTheory.Sites.Sheafification Mathlib.CategoryTheory.Sites.Subcanonical Mathlib.CategoryTheory.Sites.Types Mathlib.CategoryTheory.Sites.Whiskering |
17 |
21 filesMathlib.Algebra.Homology.Additive Mathlib.Algebra.Homology.Augment Mathlib.Algebra.Homology.DifferentialObject Mathlib.Algebra.Homology.Double Mathlib.Algebra.Homology.Embedding.Boundary Mathlib.Algebra.Homology.Embedding.Connect Mathlib.Algebra.Homology.Embedding.Restriction Mathlib.Algebra.Homology.Functor Mathlib.Algebra.Homology.HomologicalBicomplex Mathlib.Algebra.Homology.HomologicalComplexBiprod Mathlib.Algebra.Homology.HomologicalComplexLimits Mathlib.Algebra.Homology.HomologicalComplex Mathlib.Algebra.Homology.ImageToKernel Mathlib.Algebra.Homology.Linear Mathlib.Algebra.Homology.Single Mathlib.CategoryTheory.Dialectica.Monoidal Mathlib.CategoryTheory.Generator.Basic Mathlib.CategoryTheory.Generator.HomologicalComplex Mathlib.CategoryTheory.Generator.Presheaf Mathlib.CategoryTheory.Subobject.Lattice Mathlib.CategoryTheory.Subobject.Limits |
18 |
7 filesMathlib.Algebra.Homology.Square Mathlib.Algebra.Order.Rearrangement Mathlib.CategoryTheory.Distributive.Cartesian Mathlib.CategoryTheory.Distributive.Monoidal Mathlib.CategoryTheory.Monoidal.Subcategory Mathlib.CategoryTheory.Shift.Pullback Mathlib.CategoryTheory.Subobject.FactorThru |
19 |
30 filesMathlib.Algebra.Category.Grp.Preadditive Mathlib.Algebra.Category.Grp.ZModuleEquivalence Mathlib.Algebra.Category.ModuleCat.Basic Mathlib.Algebra.Homology.CommSq Mathlib.CategoryTheory.Abelian.NonPreadditive Mathlib.CategoryTheory.Center.Linear Mathlib.CategoryTheory.Center.Localization Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures Mathlib.CategoryTheory.Linear.Basic Mathlib.CategoryTheory.Linear.FunctorCategory Mathlib.CategoryTheory.Linear.LinearFunctor Mathlib.CategoryTheory.Localization.Linear Mathlib.CategoryTheory.Localization.Preadditive Mathlib.CategoryTheory.Localization.SmallShiftedHom Mathlib.CategoryTheory.Monoidal.Linear Mathlib.CategoryTheory.Monoidal.Preadditive Mathlib.CategoryTheory.Preadditive.AdditiveFunctor Mathlib.CategoryTheory.Preadditive.Basic Mathlib.CategoryTheory.Preadditive.Biproducts Mathlib.CategoryTheory.Preadditive.EilenbergMoore Mathlib.CategoryTheory.Preadditive.EndoFunctor Mathlib.CategoryTheory.Preadditive.FunctorCategory Mathlib.CategoryTheory.Preadditive.SingleObj Mathlib.CategoryTheory.Quotient.Linear Mathlib.CategoryTheory.Quotient.Preadditive Mathlib.CategoryTheory.Shift.InducedShiftSequence Mathlib.CategoryTheory.Shift.Linear Mathlib.CategoryTheory.Shift.ShiftSequence Mathlib.CategoryTheory.Shift.ShiftedHom Mathlib.CategoryTheory.Triangulated.Rotate |
20 |
Mathlib.Algebra.Order.Module.Pointwise |
25 |
Mathlib.Tactic.LinearCombination Mathlib.Tactic.Polyrith |
38 |
Mathlib.Data.DFinsupp.Order |
39 |
5 filesMathlib.Algebra.Group.EvenFunction Mathlib.Algebra.Order.Algebra Mathlib.Algebra.Order.Module.OrderedSMul Mathlib.Algebra.Order.Monovary Mathlib.Tactic.LinearCombination.Lemmas |
40 |
Mathlib.Algebra.Algebra.Rat Mathlib.Algebra.Order.Module.Algebra |
42 |
Mathlib.Algebra.Module.LinearMap.Rat |
43 |
3 filesMathlib.Algebra.Module.Equiv.Basic Mathlib.Algebra.Module.Rat Mathlib.LinearAlgebra.GeneralLinearGroup |
44 |
Mathlib.Algebra.Module.Hom |
48 |
Mathlib.Algebra.Order.Module.Defs |
55 |
Mathlib.Algebra.NoZeroSMulDivisors.Basic |
87 |
Mathlib.Algebra.Module.End |
88 |
Mathlib.Analysis.NormedSpace.MStructure |
895 |
Declarations diff
+ AddMonoid.End.ker_id_sub_eq_range
+ AddMonoidHom.ker_coprod_of_disjoint_range
+ AddMonoidHom.ker_prod_ker_le_ker_coprod
+ AddSubgroup.prodEquivOfIsCompl
+ AddSubgroup.sup_eq_range
+ IsIdempotentElem.ker_id_sub_eq_range_cont
+ IsIdempotentElem.range_id_sub_eq_ker_cont
+ IsLprojection.contractive2
+ IsLprojection.range_sum
+ IsLsummand
+ IsLsummand.Lnorm
+ IsLsummand.compl
+ IsLsummand.sup_top
+ IsMideal
+ IsMideal.inter
+ IsMideal.isSublattice
+ L1_norm_inr
+ Lprojections
+ Lsummand.IsClosed
+ Lsummand.IsCompl
+ Lsummands
+ Mprojections
+ WithLp.prod_norm_eq_of_1
+ _root_.IsIdempotentElem.mem_range_iff_self_smul
+ _root_.Lprojections.Lnorm
+ _root_.Lprojections.range
+ bijection
+ commute
+ compl_mul_self
+ contractive
+ idempotentOfClosedCompl
+ instance : Bot (Lsummands G)
+ instance : FunLike Pₗ[𝕜](A) A A
+ instance : FunLike { P : M // IsLprojection X P } X X
+ instance : FunLike ℙᴸ[M](X) X X
+ instance : PartialOrder (Lsummands G) := Subtype.partialOrder fun f ↦ IsLsummand G f
+ instance : Top (Lsummands G)
+ instance [FaithfulSMul M X] : Lattice ℙᴸ[M](X)
+ instance _root_.Lsummands.Subtype.sup [FaithfulSMul M X] : Max (Lsummands X)
+ is_idempotent_ofClosedCompl
+ ker_id_sub_idempotentOfClosedCompl
+ ker_idempotentOfClosedCompl
+ l1map
+ l1map_isometry
+ mem_iff_invariant_ofClosedCompl
+ mem_iff_zero_ofClosedCompl
+ prodEquivₗᵢ
+ prod_nnnorm_equiv
+ range_id_sub_eq_ker
+ range_id_sub_idempotentOfClosedCompl
+ range_idempotentOfClosedCompl
+ range_inter
+ range_sum
+ surjective
+ toAddMonoidEnd
+ unique_Lcomplement
+ unit_ball_conv
++ ker_id_sub_eq_range
+-+ Subtype.hasCompl
- instance [FaithfulSMul M X] : Lattice { P : M // IsLprojection X P }
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
Increase in tech debt: (relative, absolute) = (1.00, 0.12)
| Current number | Change | Type |
|---|---|---|
| 8 | 1 | maxHeartBeats modifications |
Current commit 17abf007b9
Reference commit 8b2141b23d
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
2 tasks
PR summary d03aa1faf7Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Analysis.NormedSpace.MStructure | 1103 | 2031 | +928 (+84.13%) |
| Mathlib.Algebra.Module.End | 416 | 505 | +89 (+21.39%) |
| Mathlib.Algebra.Module.Hom | 473 | 520 | +47 (+9.94%) |
| Mathlib.Algebra.Module.LinearMap.End | 483 | 484 | +1 (+0.21%) |
Import changes for all files
| Files | Import difference |
|---|---|
7 filesMathlib.Algebra.Group.ForwardDiff Mathlib.Algebra.Module.LinearMap.End Mathlib.Algebra.Module.Submodule.EqLocus Mathlib.Algebra.Module.Submodule.IterateMapComap Mathlib.Algebra.Module.Submodule.Ker Mathlib.Algebra.Module.Submodule.LinearMap Mathlib.Algebra.Module.Submodule.Map |
1 |
682 filesMathlib.Algebra.Algebra.Basic Mathlib.Algebra.Algebra.Bilinear Mathlib.Algebra.Algebra.Equiv Mathlib.Algebra.Algebra.Hom.Rat Mathlib.Algebra.Algebra.Hom Mathlib.Algebra.Algebra.NonUnitalHom Mathlib.Algebra.Algebra.NonUnitalSubalgebra Mathlib.Algebra.Algebra.Operations Mathlib.Algebra.Algebra.Opposite Mathlib.Algebra.Algebra.Pi Mathlib.Algebra.Algebra.Prod Mathlib.Algebra.Algebra.RestrictScalars Mathlib.Algebra.Algebra.Shrink Mathlib.Algebra.Algebra.Subalgebra.Basic Mathlib.Algebra.Algebra.Subalgebra.Centralizer Mathlib.Algebra.Algebra.Subalgebra.Directed Mathlib.Algebra.Algebra.Subalgebra.Lattice Mathlib.Algebra.Algebra.Subalgebra.Matrix Mathlib.Algebra.Algebra.Subalgebra.MulOpposite Mathlib.Algebra.Algebra.Subalgebra.Order Mathlib.Algebra.Algebra.Subalgebra.Pi Mathlib.Algebra.Algebra.Subalgebra.Pointwise Mathlib.Algebra.Algebra.Subalgebra.Prod Mathlib.Algebra.Algebra.Subalgebra.Tower Mathlib.Algebra.Algebra.Subalgebra.Unitization Mathlib.Algebra.Algebra.Tower Mathlib.Algebra.Algebra.TransferInstance Mathlib.Algebra.Algebra.Unitization Mathlib.Algebra.Algebra.ZMod Mathlib.Algebra.Category.AlgCat.Basic Mathlib.Algebra.Category.AlgCat.Limits Mathlib.Algebra.Category.AlgCat.Monoidal Mathlib.Algebra.Category.AlgCat.Symmetric Mathlib.Algebra.Category.AlgebraCat.Symmetric Mathlib.Algebra.Category.Grp.AB Mathlib.Algebra.Category.Grp.Abelian Mathlib.Algebra.Category.Grp.Images Mathlib.Algebra.Category.Grp.IsFinite Mathlib.Algebra.Category.Grp.Subobject Mathlib.Algebra.Category.ModuleCat.AB Mathlib.Algebra.Category.ModuleCat.Abelian Mathlib.Algebra.Category.ModuleCat.Adjunctions Mathlib.Algebra.Category.ModuleCat.Algebra Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.Algebra.Category.ModuleCat.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.Algebra.Category.ModuleCat.Images Mathlib.Algebra.Category.ModuleCat.Injective Mathlib.Algebra.Category.ModuleCat.Kernels Mathlib.Algebra.Category.ModuleCat.Limits Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono Mathlib.Algebra.Category.ModuleCat.Presheaf.Free Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.Algebra.Category.ModuleCat.Presheaf Mathlib.Algebra.Category.ModuleCat.Products Mathlib.Algebra.Category.ModuleCat.Projective Mathlib.Algebra.Category.ModuleCat.Pseudofunctor Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.Algebra.Category.ModuleCat.Tannaka Mathlib.Algebra.Category.Ring.Adjunctions Mathlib.Algebra.Central.Basic Mathlib.Algebra.Central.Defs Mathlib.Algebra.Central.Matrix Mathlib.Algebra.CharP.Algebra Mathlib.Algebra.CharP.CharAndCard Mathlib.Algebra.CharP.Subring Mathlib.Algebra.CharP.Two Mathlib.Algebra.Colimit.Module Mathlib.Algebra.DirectSum.AddChar Mathlib.Algebra.DirectSum.Algebra Mathlib.Algebra.DirectSum.Decomposition Mathlib.Algebra.DirectSum.Finsupp Mathlib.Algebra.DirectSum.Internal Mathlib.Algebra.DirectSum.Module Mathlib.Algebra.DualNumber Mathlib.Algebra.Exact Mathlib.Algebra.Field.NegOnePow Mathlib.Algebra.Field.Periodic Mathlib.Algebra.Field.ZMod Mathlib.Algebra.FiveLemma Mathlib.Algebra.FreeAlgebra.Cardinality Mathlib.Algebra.FreeAlgebra Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra Mathlib.Algebra.Homology.BifunctorAssociator Mathlib.Algebra.Homology.BifunctorFlip Mathlib.Algebra.Homology.BifunctorHomotopy Mathlib.Algebra.Homology.BifunctorShift Mathlib.Algebra.Homology.Bifunctor Mathlib.Algebra.Homology.ComplexShapeSigns Mathlib.Algebra.Homology.ConcreteCategory Mathlib.Algebra.Homology.DerivedCategory.Basic Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass Mathlib.Algebra.Homology.DerivedCategory.Fractions Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful Mathlib.Algebra.Homology.DerivedCategory.HomologySequence Mathlib.Algebra.Homology.DerivedCategory.ShortExact Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle Mathlib.Algebra.Homology.Embedding.CochainComplex Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift Mathlib.Algebra.Homology.HomotopyCategory.HomComplex Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor Mathlib.Algebra.Homology.HomotopyCategory.MappingCone Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence Mathlib.Algebra.Homology.HomotopyCategory.Shift Mathlib.Algebra.Homology.HomotopyCategory.ShortExact Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors Mathlib.Algebra.Homology.HomotopyCategory.Triangulated Mathlib.Algebra.Homology.Monoidal Mathlib.Algebra.Homology.ShortComplex.Ab Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.Algebra.Homology.TotalComplexShift Mathlib.Algebra.Homology.TotalComplexSymmetry Mathlib.Algebra.Homology.TotalComplex Mathlib.Algebra.Lie.Basic Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra Mathlib.Algebra.Module.Bimodule Mathlib.Algebra.Module.GradedModule Mathlib.Algebra.Module.Injective Mathlib.Algebra.Module.LocalizedModule.AtPrime Mathlib.Algebra.Module.LocalizedModule.Away Mathlib.Algebra.Module.LocalizedModule.Basic Mathlib.Algebra.Module.LocalizedModule.Exact Mathlib.Algebra.Module.LocalizedModule.Int Mathlib.Algebra.Module.LocalizedModule.IsLocalization Mathlib.Algebra.Module.LocalizedModule.Submodule Mathlib.Algebra.Module.Presentation.Basic Mathlib.Algebra.Module.Presentation.Cokernel Mathlib.Algebra.Module.Presentation.DirectSum Mathlib.Algebra.Module.Presentation.Free Mathlib.Algebra.Module.Presentation.RestrictScalars Mathlib.Algebra.Module.Presentation.Tautological Mathlib.Algebra.Module.Presentation.Tensor Mathlib.Algebra.Module.Projective Mathlib.Algebra.Module.SnakeLemma Mathlib.Algebra.Module.Submodule.Bilinear Mathlib.Algebra.Module.Submodule.Equiv Mathlib.Algebra.Module.Submodule.Pointwise Mathlib.Algebra.Module.Submodule.Range Mathlib.Algebra.Module.Submodule.Union Mathlib.Algebra.Module.ZMod Mathlib.Algebra.MonoidAlgebra.Basic Mathlib.Algebra.MonoidAlgebra.Degree Mathlib.Algebra.MonoidAlgebra.Grading Mathlib.Algebra.MonoidAlgebra.Support Mathlib.Algebra.MonoidAlgebra.ToDirectSum Mathlib.Algebra.MvPolynomial.Basic Mathlib.Algebra.MvPolynomial.Cardinal Mathlib.Algebra.MvPolynomial.Comap Mathlib.Algebra.MvPolynomial.CommRing Mathlib.Algebra.MvPolynomial.Counit Mathlib.Algebra.MvPolynomial.Degrees Mathlib.Algebra.MvPolynomial.Derivation Mathlib.Algebra.MvPolynomial.Division Mathlib.Algebra.MvPolynomial.Equiv Mathlib.Algebra.MvPolynomial.Eval Mathlib.Algebra.MvPolynomial.Expand Mathlib.Algebra.MvPolynomial.Funext Mathlib.Algebra.MvPolynomial.Invertible Mathlib.Algebra.MvPolynomial.Monad Mathlib.Algebra.MvPolynomial.PDeriv Mathlib.Algebra.MvPolynomial.Polynomial Mathlib.Algebra.MvPolynomial.Rename Mathlib.Algebra.MvPolynomial.SchwartzZippel Mathlib.Algebra.MvPolynomial.Supported Mathlib.Algebra.MvPolynomial.Variables Mathlib.Algebra.Order.Chebyshev Mathlib.Algebra.Order.Group.Cyclic Mathlib.Algebra.Order.ToIntervalMod Mathlib.Algebra.Polynomial.AlgebraMap Mathlib.Algebra.Polynomial.Basis Mathlib.Algebra.Polynomial.BigOperators Mathlib.Algebra.Polynomial.CancelLeads Mathlib.Algebra.Polynomial.CoeffList Mathlib.Algebra.Polynomial.Coeff Mathlib.Algebra.Polynomial.Degree.Definitions Mathlib.Algebra.Polynomial.Degree.Domain Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree Mathlib.Algebra.Polynomial.Degree.Lemmas Mathlib.Algebra.Polynomial.Degree.Monomial Mathlib.Algebra.Polynomial.Degree.Operations Mathlib.Algebra.Polynomial.Degree.SmallDegree Mathlib.Algebra.Polynomial.Degree.Support Mathlib.Algebra.Polynomial.Degree.TrailingDegree Mathlib.Algebra.Polynomial.Degree.Units Mathlib.Algebra.Polynomial.DenomsClearable Mathlib.Algebra.Polynomial.Derivative Mathlib.Algebra.Polynomial.Div Mathlib.Algebra.Polynomial.EraseLead Mathlib.Algebra.Polynomial.Eval.Coeff Mathlib.Algebra.Polynomial.Eval.Degree Mathlib.Algebra.Polynomial.Eval.Irreducible Mathlib.Algebra.Polynomial.Eval.SMul Mathlib.Algebra.Polynomial.Eval.Subring Mathlib.Algebra.Polynomial.GroupRingAction Mathlib.Algebra.Polynomial.HasseDeriv Mathlib.Algebra.Polynomial.Identities Mathlib.Algebra.Polynomial.Inductions Mathlib.Algebra.Polynomial.Lifts Mathlib.Algebra.Polynomial.Mirror Mathlib.Algebra.Polynomial.Monic Mathlib.Algebra.Polynomial.OfFn Mathlib.Algebra.Polynomial.PartialFractions Mathlib.Algebra.Polynomial.Reverse Mathlib.Algebra.Polynomial.RingDivision Mathlib.Algebra.Polynomial.Roots Mathlib.Algebra.Polynomial.Sequence Mathlib.Algebra.Polynomial.Smeval Mathlib.Algebra.Polynomial.SumIteratedDerivative Mathlib.Algebra.Polynomial.Taylor Mathlib.Algebra.Polynomial.UnitTrinomial Mathlib.Algebra.Ring.NegOnePow Mathlib.Algebra.Ring.Periodic Mathlib.Algebra.Ring.Subring.IntPolynomial Mathlib.Algebra.SkewMonoidAlgebra.Basic Mathlib.Algebra.Star.Free Mathlib.Algebra.Star.Module Mathlib.Algebra.Star.NonUnitalSubalgebra Mathlib.Algebra.Star.StarAlgHom Mathlib.Algebra.Star.Subalgebra Mathlib.Algebra.TrivSqZeroExt Mathlib.Algebra.Vertex.HVertexOperator Mathlib.Algebra.Vertex.VertexOperator Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit Mathlib.AlgebraicTopology.FundamentalGroupoid.Product Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected Mathlib.AlgebraicTopology.SingularHomology.Basic Mathlib.AlgebraicTopology.SingularSet Mathlib.AlgebraicTopology.TopologicalSimplex Mathlib.Analysis.Asymptotics.Defs Mathlib.Analysis.Convex.Basic Mathlib.Analysis.Convex.Cone.Extension Mathlib.Analysis.Convex.Contractible Mathlib.Analysis.Convex.Extrema Mathlib.Analysis.Convex.Extreme Mathlib.Analysis.Convex.Function Mathlib.Analysis.Convex.Hull Mathlib.Analysis.Convex.Join Mathlib.Analysis.Convex.Mul Mathlib.Analysis.Convex.Piecewise Mathlib.Analysis.Convex.Quasiconvex Mathlib.Analysis.Convex.Segment Mathlib.Analysis.Convex.Slope Mathlib.Analysis.Convex.Star Mathlib.Analysis.Convex.Strict Mathlib.Analysis.Normed.Field.Basic Mathlib.Analysis.Normed.Group.AddTorsor Mathlib.Analysis.Normed.Group.Bounded Mathlib.Analysis.Normed.Group.Continuity Mathlib.Analysis.Normed.Group.Rat Mathlib.Analysis.Normed.Ring.Basic Mathlib.Analysis.Normed.Ring.Finite Mathlib.Analysis.Normed.Ring.WithAbs Mathlib.Analysis.Polynomial.CauchyBound Mathlib.Analysis.Subadditive Mathlib.Analysis.SumOverResidueClass Mathlib.CategoryTheory.Abelian.Ext Mathlib.CategoryTheory.Abelian.FreydMitchell Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite Mathlib.CategoryTheory.Abelian.Injective.Basic Mathlib.CategoryTheory.Abelian.Projective.Basic Mathlib.CategoryTheory.Abelian.Projective.Dimension Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.CategoryTheory.Abelian.Yoneda Mathlib.CategoryTheory.Galois.Equivalence Mathlib.CategoryTheory.Galois.EssSurj Mathlib.CategoryTheory.Galois.IsFundamentalgroup Mathlib.CategoryTheory.Galois.Topology Mathlib.CategoryTheory.Localization.Triangulated Mathlib.CategoryTheory.Monoidal.Internal.Module Mathlib.CategoryTheory.Preadditive.Yoneda.Injective Mathlib.CategoryTheory.Preadditive.Yoneda.Limits Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.CategoryTheory.Sites.MayerVietorisSquare Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.CategoryTheory.Triangulated.Adjunction Mathlib.CategoryTheory.Triangulated.Functor Mathlib.CategoryTheory.Triangulated.HomologicalFunctor Mathlib.CategoryTheory.Triangulated.Opposite.Functor Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated Mathlib.CategoryTheory.Triangulated.Pretriangulated Mathlib.CategoryTheory.Triangulated.Subcategory Mathlib.CategoryTheory.Triangulated.TStructure.Basic Mathlib.CategoryTheory.Triangulated.TriangleShift Mathlib.CategoryTheory.Triangulated.Triangulated Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.Combinatorics.Additive.CauchyDavenport Mathlib.Combinatorics.Optimization.ValuedCSP Mathlib.Combinatorics.SimpleGraph.AdjMatrix Mathlib.Combinatorics.SimpleGraph.Bipartite Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite Mathlib.Combinatorics.SimpleGraph.ConcreteColorings Mathlib.Combinatorics.SimpleGraph.DegreeSum Mathlib.Combinatorics.SimpleGraph.FiveWheelLike Mathlib.Combinatorics.SimpleGraph.Matching Mathlib.Combinatorics.SimpleGraph.StronglyRegular Mathlib.Combinatorics.SimpleGraph.Tutte Mathlib.Combinatorics.SimpleGraph.UniversalVerts Mathlib.Data.Complex.Norm Mathlib.Data.Complex.Order Mathlib.Data.Finsupp.MonomialOrder.DegLex Mathlib.Data.Finsupp.Weight Mathlib.Data.Matrix.Auto Mathlib.Data.Matrix.Basic Mathlib.Data.Matrix.Basis Mathlib.Data.Matrix.Bilinear Mathlib.Data.Matrix.Block Mathlib.Data.Matrix.ColumnRowPartitioned Mathlib.Data.Matrix.Composition Mathlib.Data.Matrix.ConjTranspose Mathlib.Data.Matrix.DualNumber Mathlib.Data.Matrix.Hadamard Mathlib.Data.Matrix.Invertible Mathlib.Data.Matrix.Kronecker Mathlib.Data.Matrix.Notation Mathlib.Data.Matrix.Reflection Mathlib.Data.Matrix.RowCol Mathlib.Data.Matrix.Vec Mathlib.Data.Nat.Choose.Cast Mathlib.Data.Nat.Choose.Vandermonde Mathlib.Data.Nat.Factorial.Cast Mathlib.Data.Nat.Periodic Mathlib.Data.Nat.Totient Mathlib.Data.Real.CompleteField Mathlib.Data.Real.Sqrt Mathlib.Data.ZMod.Aut Mathlib.Data.ZMod.Basic Mathlib.Data.ZMod.Factorial Mathlib.Data.ZMod.IntUnitsPower Mathlib.Data.ZMod.QuotientGroup Mathlib.Data.ZMod.Units Mathlib.Data.ZMod.ValMinAbs Mathlib.FieldTheory.RatFunc.Defs Mathlib.Geometry.Convex.Cone.Basic Mathlib.Geometry.Manifold.ChartedSpace Mathlib.Geometry.Manifold.LocalInvariantProperties Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.GroupTheory.CommutingProbability Mathlib.GroupTheory.Coxeter.Basic Mathlib.GroupTheory.Coxeter.Inversion Mathlib.GroupTheory.Coxeter.Length Mathlib.GroupTheory.Coxeter.Matrix Mathlib.GroupTheory.Exponent Mathlib.GroupTheory.FixedPointFree Mathlib.GroupTheory.Frattini Mathlib.GroupTheory.GroupAction.Iwasawa Mathlib.GroupTheory.GroupAction.MultiplePrimitivity Mathlib.GroupTheory.GroupAction.MultipleTransitivity Mathlib.GroupTheory.GroupAction.Period Mathlib.GroupTheory.GroupAction.Primitive Mathlib.GroupTheory.Nilpotent Mathlib.GroupTheory.Order.Min Mathlib.GroupTheory.PGroup Mathlib.GroupTheory.Perm.Centralizer Mathlib.GroupTheory.Perm.Closure Mathlib.GroupTheory.Perm.ConjAct Mathlib.GroupTheory.Perm.Cycle.Basic Mathlib.GroupTheory.Perm.Cycle.Concrete Mathlib.GroupTheory.Perm.Cycle.Factors Mathlib.GroupTheory.Perm.Cycle.PossibleTypes Mathlib.GroupTheory.Perm.Cycle.Type Mathlib.GroupTheory.Perm.Fin Mathlib.GroupTheory.RegularWreathProduct Mathlib.GroupTheory.Schreier Mathlib.GroupTheory.SchurZassenhaus Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour Mathlib.GroupTheory.SpecificGroups.Alternating Mathlib.GroupTheory.SpecificGroups.Cyclic Mathlib.GroupTheory.SpecificGroups.Dihedral Mathlib.GroupTheory.SpecificGroups.KleinFour Mathlib.GroupTheory.SpecificGroups.Quaternion Mathlib.GroupTheory.Sylow Mathlib.GroupTheory.Torsion Mathlib.GroupTheory.Transfer Mathlib.LinearAlgebra.AffineSpace.AffineEquiv Mathlib.LinearAlgebra.AffineSpace.AffineMap Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic Mathlib.LinearAlgebra.AffineSpace.Centroid Mathlib.LinearAlgebra.AffineSpace.Combination Mathlib.LinearAlgebra.AffineSpace.MidpointZero Mathlib.LinearAlgebra.AffineSpace.Midpoint Mathlib.LinearAlgebra.AffineSpace.Ordered Mathlib.LinearAlgebra.AffineSpace.Pointwise Mathlib.LinearAlgebra.AffineSpace.Restrict Mathlib.LinearAlgebra.AffineSpace.Slope Mathlib.LinearAlgebra.Alternating.Basic Mathlib.LinearAlgebra.Alternating.Curry Mathlib.LinearAlgebra.Alternating.DomCoprod Mathlib.LinearAlgebra.Alternating.Uncurry.Fin Mathlib.LinearAlgebra.Basis.Basic Mathlib.LinearAlgebra.Basis.Bilinear Mathlib.LinearAlgebra.Basis.Cardinality Mathlib.LinearAlgebra.Basis.Defs Mathlib.LinearAlgebra.Basis.Exact Mathlib.LinearAlgebra.Basis.Fin Mathlib.LinearAlgebra.Basis.Flag Mathlib.LinearAlgebra.Basis.Prod Mathlib.LinearAlgebra.Basis.SMul Mathlib.LinearAlgebra.Basis.Submodule Mathlib.LinearAlgebra.BilinearForm.Basic Mathlib.LinearAlgebra.BilinearForm.Hom Mathlib.LinearAlgebra.BilinearMap Mathlib.LinearAlgebra.Countable Mathlib.LinearAlgebra.CrossProduct Mathlib.LinearAlgebra.DFinsupp Mathlib.LinearAlgebra.Dimension.Basic Mathlib.LinearAlgebra.Dimension.Finrank Mathlib.LinearAlgebra.Dimension.Subsingleton Mathlib.LinearAlgebra.DirectSum.Basis Mathlib.LinearAlgebra.DirectSum.Finsupp Mathlib.LinearAlgebra.DirectSum.TensorProduct Mathlib.LinearAlgebra.Dual.Basis Mathlib.LinearAlgebra.Dual.Defs Mathlib.LinearAlgebra.FiniteSpan Mathlib.LinearAlgebra.Finsupp.LinearCombination Mathlib.LinearAlgebra.Finsupp.Pi Mathlib.LinearAlgebra.Finsupp.Span Mathlib.LinearAlgebra.Finsupp.Supported Mathlib.LinearAlgebra.Finsupp.VectorSpace Mathlib.LinearAlgebra.FreeModule.Basic Mathlib.LinearAlgebra.Goursat Mathlib.LinearAlgebra.Isomorphisms Mathlib.LinearAlgebra.LinearIndependent.Basic Mathlib.LinearAlgebra.LinearIndependent.Defs Mathlib.LinearAlgebra.LinearIndependent.Lemmas Mathlib.LinearAlgebra.LinearPMap Mathlib.LinearAlgebra.Matrix.AbsoluteValue Mathlib.LinearAlgebra.Matrix.Adjugate Mathlib.LinearAlgebra.Matrix.Circulant Mathlib.LinearAlgebra.Matrix.Determinant.Basic Mathlib.LinearAlgebra.Matrix.Determinant.Misc Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular Mathlib.LinearAlgebra.Matrix.IsDiag Mathlib.LinearAlgebra.Matrix.MvPolynomial Mathlib.LinearAlgebra.Matrix.Nondegenerate Mathlib.LinearAlgebra.Matrix.Permanent Mathlib.LinearAlgebra.Matrix.Polynomial Mathlib.LinearAlgebra.Matrix.Reindex Mathlib.LinearAlgebra.Matrix.StdBasis Mathlib.LinearAlgebra.Matrix.Symmetric Mathlib.LinearAlgebra.Matrix.Trace Mathlib.LinearAlgebra.Matrix.Transvection Mathlib.LinearAlgebra.Matrix.Unique Mathlib.LinearAlgebra.Multilinear.Basic Mathlib.LinearAlgebra.Multilinear.Basis Mathlib.LinearAlgebra.Multilinear.Curry Mathlib.LinearAlgebra.Multilinear.DFinsupp Mathlib.LinearAlgebra.Multilinear.Pi Mathlib.LinearAlgebra.Multilinear.TensorProduct Mathlib.LinearAlgebra.PiTensorProduct Mathlib.LinearAlgebra.Pi Mathlib.LinearAlgebra.Prod Mathlib.LinearAlgebra.Quotient.Basic Mathlib.LinearAlgebra.Quotient.Pi Mathlib.LinearAlgebra.Ray Mathlib.LinearAlgebra.SModEq Mathlib.LinearAlgebra.SesquilinearForm Mathlib.LinearAlgebra.Span.Basic Mathlib.LinearAlgebra.StdBasis Mathlib.LinearAlgebra.TensorPower.Basic Mathlib.LinearAlgebra.TensorPower.Pairing Mathlib.LinearAlgebra.TensorProduct.Associator Mathlib.LinearAlgebra.TensorProduct.Basic Mathlib.LinearAlgebra.TensorProduct.Basis Mathlib.LinearAlgebra.TensorProduct.DirectLimit Mathlib.LinearAlgebra.TensorProduct.Graded.External Mathlib.LinearAlgebra.TensorProduct.Graded.Internal Mathlib.LinearAlgebra.TensorProduct.Opposite Mathlib.LinearAlgebra.TensorProduct.Pi Mathlib.LinearAlgebra.TensorProduct.Prod Mathlib.LinearAlgebra.TensorProduct.Subalgebra Mathlib.LinearAlgebra.TensorProduct.Submodule Mathlib.LinearAlgebra.TensorProduct.Tower Mathlib.MeasureTheory.OuterMeasure.AE Mathlib.MeasureTheory.OuterMeasure.Basic Mathlib.MeasureTheory.OuterMeasure.BorelCantelli Mathlib.MeasureTheory.OuterMeasure.Operations Mathlib.ModelTheory.Algebra.Field.CharP Mathlib.ModelTheory.Algebra.Ring.FreeCommRing Mathlib.NumberTheory.ClassNumber.AdmissibleAbs Mathlib.NumberTheory.DirichletCharacter.Basic Mathlib.NumberTheory.LegendreSymbol.ZModChar Mathlib.NumberTheory.LucasPrimality Mathlib.NumberTheory.MulChar.Basic Mathlib.NumberTheory.PrimeCounting Mathlib.RingTheory.Adjoin.Basic Mathlib.RingTheory.Adjoin.Polynomial Mathlib.RingTheory.AlgebraTower Mathlib.RingTheory.Algebraic.Cardinality Mathlib.RingTheory.Algebraic.Defs Mathlib.RingTheory.Algebraic.LinearIndependent Mathlib.RingTheory.Algebraic.Pi Mathlib.RingTheory.AlgebraicIndependent.Defs Mathlib.RingTheory.Binomial Mathlib.RingTheory.Derivation.Basic Mathlib.RingTheory.Derivation.DifferentialRing Mathlib.RingTheory.Fintype Mathlib.RingTheory.FreeCommRing Mathlib.RingTheory.GradedAlgebra.Basic Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule Mathlib.RingTheory.HahnSeries.Multiplication Mathlib.RingTheory.HahnSeries.Summable Mathlib.RingTheory.IntegralClosure.Algebra.Defs Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs Mathlib.RingTheory.IntegralDomain Mathlib.RingTheory.IsTensorProduct Mathlib.RingTheory.Localization.Basic Mathlib.RingTheory.Localization.Cardinality Mathlib.RingTheory.Localization.FractionRing Mathlib.RingTheory.Localization.Module Mathlib.RingTheory.Localization.NumDen Mathlib.RingTheory.MatrixAlgebra Mathlib.RingTheory.MatrixPolynomialAlgebra Mathlib.RingTheory.Morita.Basic Mathlib.RingTheory.MvPolynomial.EulerIdentity Mathlib.RingTheory.MvPolynomial.FreeCommRing Mathlib.RingTheory.MvPolynomial.Groebner Mathlib.RingTheory.MvPolynomial.Homogeneous Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex Mathlib.RingTheory.MvPolynomial.MonomialOrder Mathlib.RingTheory.MvPolynomial.Symmetric.Defs Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities Mathlib.RingTheory.MvPolynomial.Tower Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous Mathlib.RingTheory.MvPowerSeries.Basic Mathlib.RingTheory.MvPowerSeries.LexOrder Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors Mathlib.RingTheory.MvPowerSeries.Order Mathlib.RingTheory.MvPowerSeries.Trunc Mathlib.RingTheory.Nilpotent.Exp Mathlib.RingTheory.PiTensorProduct Mathlib.RingTheory.Polynomial.Bernstein Mathlib.RingTheory.Polynomial.Chebyshev Mathlib.RingTheory.Polynomial.Dickson Mathlib.RingTheory.Polynomial.Hermite.Basic Mathlib.RingTheory.Polynomial.IntegralNormalization Mathlib.RingTheory.Polynomial.Opposites Mathlib.RingTheory.Polynomial.Pochhammer Mathlib.RingTheory.Polynomial.Resultant.Basic Mathlib.RingTheory.Polynomial.ScaleRoots Mathlib.RingTheory.Polynomial.ShiftedLegendre Mathlib.RingTheory.Polynomial.Tower Mathlib.RingTheory.Polynomial.Wronskian Mathlib.RingTheory.PolynomialAlgebra Mathlib.RingTheory.PolynomialLaw.Basic Mathlib.RingTheory.RootsOfUnity.Basic Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots Mathlib.RingTheory.TensorProduct.Basic Mathlib.RingTheory.TensorProduct.MvPolynomial Mathlib.RingTheory.TensorProduct.Pi Mathlib.RingTheory.WittVector.WittPolynomial Mathlib.SetTheory.Cardinal.Free Mathlib.SetTheory.Nimber.Field Mathlib.Tactic.Algebraize Mathlib.Tactic.ComputeDegree Mathlib.Tactic.Module Mathlib.Tactic.NormNum.RealSqrt Mathlib.Tactic.Ring.NamePolyVars Mathlib.Topology.Algebra.Affine Mathlib.Topology.Algebra.ClopenNhdofOne Mathlib.Topology.Algebra.ClosedSubgroup Mathlib.Topology.Algebra.Equicontinuity Mathlib.Topology.Algebra.Field Mathlib.Topology.Algebra.FilterBasis Mathlib.Topology.Algebra.Group.Basic Mathlib.Topology.Algebra.Group.ClosedSubgroup Mathlib.Topology.Algebra.Group.Compact Mathlib.Topology.Algebra.Group.GroupTopology Mathlib.Topology.Algebra.Group.OpenMapping Mathlib.Topology.Algebra.Group.Pointwise Mathlib.Topology.Algebra.Group.Quotient Mathlib.Topology.Algebra.Group.SubmonoidClosure Mathlib.Topology.Algebra.Group.TopologicalAbelianization Mathlib.Topology.Algebra.GroupCompletion Mathlib.Topology.Algebra.InfiniteSum.Constructions Mathlib.Topology.Algebra.InfiniteSum.ENNReal Mathlib.Topology.Algebra.InfiniteSum.Field Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion Mathlib.Topology.Algebra.InfiniteSum.Group Mathlib.Topology.Algebra.InfiniteSum.NatInt Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean Mathlib.Topology.Algebra.InfiniteSum.Order Mathlib.Topology.Algebra.InfiniteSum.Real Mathlib.Topology.Algebra.InfiniteSum.Ring Mathlib.Topology.Algebra.InfiniteSum.UniformOn Mathlib.Topology.Algebra.IsUniformGroup.Basic Mathlib.Topology.Algebra.IsUniformGroup.Defs Mathlib.Topology.Algebra.IsUniformGroup.Order Mathlib.Topology.Algebra.LinearTopology Mathlib.Topology.Algebra.Localization Mathlib.Topology.Algebra.MetricSpace.Lipschitz Mathlib.Topology.Algebra.Module.Basic Mathlib.Topology.Algebra.Module.LinearPMap Mathlib.Topology.Algebra.MvPolynomial Mathlib.Topology.Algebra.NonUnitalAlgebra Mathlib.Topology.Algebra.NonUnitalStarAlgebra Mathlib.Topology.Algebra.Nonarchimedean.Bases Mathlib.Topology.Algebra.Nonarchimedean.Basic Mathlib.Topology.Algebra.Nonarchimedean.Completion Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected Mathlib.Topology.Algebra.OpenSubgroup Mathlib.Topology.Algebra.Order.Field Mathlib.Topology.Algebra.Order.LiminfLimsup Mathlib.Topology.Algebra.Order.UpperLower Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace Mathlib.Topology.Algebra.RestrictedProduct Mathlib.Topology.Algebra.Ring.Basic Mathlib.Topology.Algebra.Ring.Ideal Mathlib.Topology.Algebra.Ring.Real Mathlib.Topology.Algebra.UniformConvergence Mathlib.Topology.Algebra.UniformField Mathlib.Topology.Algebra.UniformFilterBasis Mathlib.Topology.Algebra.UniformMulAction Mathlib.Topology.Algebra.UniformRing Mathlib.Topology.Category.TopCommRingCat Mathlib.Topology.Compactness.HilbertCubeEmbedding Mathlib.Topology.Connected.LocPathConnected Mathlib.Topology.Connected.PathComponentOne Mathlib.Topology.Connected.PathConnected Mathlib.Topology.EMetricSpace.BoundedVariation Mathlib.Topology.Homotopy.Basic Mathlib.Topology.Homotopy.Contractible Mathlib.Topology.Homotopy.Equiv Mathlib.Topology.Homotopy.HSpaces Mathlib.Topology.Homotopy.HomotopyGroup Mathlib.Topology.Homotopy.Lifting Mathlib.Topology.Homotopy.Path Mathlib.Topology.Homotopy.Product Mathlib.Topology.Instances.AddCircle.Defs Mathlib.Topology.Instances.AddCircle.Real Mathlib.Topology.Instances.CantorSet Mathlib.Topology.Instances.ENNReal.Lemmas Mathlib.Topology.Instances.EReal.Lemmas Mathlib.Topology.Instances.NNReal.Lemmas Mathlib.Topology.Instances.Rat Mathlib.Topology.Instances.Real.Lemmas Mathlib.Topology.Instances.ZMultiples Mathlib.Topology.LocallyConstant.Algebra Mathlib.Topology.MetricSpace.CauSeqFilter Mathlib.Topology.Path Mathlib.Topology.Semicontinuous Mathlib.Topology.Sheaves.MayerVietoris Mathlib.Topology.UniformSpace.CompareReals Mathlib.Topology.UniformSpace.Matrix Mathlib.Topology.UnitInterval |
2 |
27 filesMathlib.Algebra.Category.Grp.Adjunctions Mathlib.Algebra.Category.Grp.Biproducts Mathlib.Algebra.Category.Grp.CartesianMonoidal Mathlib.Algebra.Category.Grp.ChosenFiniteProducts Mathlib.Algebra.Category.Grp.Colimits Mathlib.Algebra.Category.Grp.Kernels Mathlib.Algebra.Category.Grp.LeftExactFunctor Mathlib.Algebra.Category.Grp.Limits Mathlib.Algebra.Category.ModuleCat.Colimits Mathlib.Algebra.Category.ModuleCat.FilteredColimits Mathlib.Algebra.Category.Ring.Limits Mathlib.Algebra.FreeAbelianGroup.Finsupp Mathlib.Algebra.FreeAbelianGroup.UniqueSums Mathlib.Algebra.ModEq Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization Mathlib.CategoryTheory.Abelian.Indization Mathlib.CategoryTheory.Action.Monoidal Mathlib.CategoryTheory.Galois.Action Mathlib.CategoryTheory.Galois.Examples Mathlib.CategoryTheory.Galois.Full Mathlib.CategoryTheory.Galois.Prorepresentability Mathlib.CategoryTheory.Generator.Indization Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_ Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_ Mathlib.CategoryTheory.Preadditive.Indization Mathlib.Geometry.RingedSpace.Basic Mathlib.GroupTheory.ClassEquation |
3 |
Mathlib.Algebra.Module.Submodule.Invariant |
4 |
3 filesMathlib.Algebra.Module.Submodule.RestrictScalars Mathlib.LinearAlgebra.Matrix.SemiringInverse Mathlib.RingTheory.Localization.Integer |
5 |
19 filesMathlib.Algebra.Order.Antidiag.Nat Mathlib.Algebra.Polynomial.Basic Mathlib.Algebra.Polynomial.Cardinal Mathlib.Algebra.Polynomial.Eval.Algebra Mathlib.Algebra.Polynomial.Eval.Defs Mathlib.Algebra.Polynomial.Monomial Mathlib.Algebra.Ring.CentroidHom Mathlib.Algebra.Squarefree.Basic Mathlib.Algebra.Star.CentroidHom Mathlib.Computability.TMComputable Mathlib.Data.Nat.Squarefree Mathlib.NumberTheory.ArithmeticFunction Mathlib.NumberTheory.MaricaSchoenheim Mathlib.NumberTheory.SelbergSieve Mathlib.NumberTheory.SmoothNumbers Mathlib.RingTheory.Localization.Defs Mathlib.RingTheory.OreLocalization.Cardinality Mathlib.RingTheory.Radical Mathlib.SetTheory.Surreal.Dyadic |
6 |
14 filesMathlib.Algebra.DirectSum.Basic Mathlib.Algebra.DirectSum.Ring Mathlib.Algebra.MonoidAlgebra.Module Mathlib.Analysis.Normed.Group.Submodule Mathlib.Data.DFinsupp.Submonoid Mathlib.Dynamics.Flow Mathlib.Dynamics.OmegaLimit Mathlib.LinearAlgebra.Finsupp.LSum Mathlib.RingTheory.Nilpotent.Basic Mathlib.RingTheory.OreLocalization.Ring Mathlib.Topology.Algebra.GroupWithZero Mathlib.Topology.Algebra.Monoid Mathlib.Topology.Algebra.WithZeroTopology Mathlib.Topology.ApproximateUnit |
7 |
22 filesMathlib.Algebra.CharP.Frobenius Mathlib.Algebra.CharP.Lemmas Mathlib.Algebra.CharP.Reduced Mathlib.Data.DFinsupp.Interval Mathlib.Data.Finsupp.Interval Mathlib.Data.Finsupp.MonomialOrder Mathlib.Data.Finsupp.WellFounded Mathlib.Data.Multiset.Interval Mathlib.Data.Nat.Choose.Factorization Mathlib.Data.Nat.Factorization.Basic Mathlib.Data.Nat.Factorization.Defs Mathlib.Data.Nat.Factorization.Induction Mathlib.Data.Nat.Factorization.LCM Mathlib.Data.Nat.Factorization.PrimePow Mathlib.Data.Nat.Factorization.Root Mathlib.Data.Nat.Multiplicity Mathlib.Logic.Hydra Mathlib.NumberTheory.Padics.PadicNorm Mathlib.NumberTheory.Padics.PadicVal.Basic Mathlib.SetTheory.Surreal.Multiplication Mathlib.Topology.Algebra.Algebra.Rat Mathlib.Topology.MetricSpace.IsometricSMul |
9 |
5 filesMathlib.Analysis.Normed.Group.Subgroup Mathlib.Data.DFinsupp.BigOperators Mathlib.Data.DFinsupp.Multiset Mathlib.Data.Finsupp.Lex Mathlib.Data.Finsupp.Order |
10 |
195 filesMathlib.Algebra.BigOperators.Balance Mathlib.Algebra.BigOperators.Expect Mathlib.Algebra.Homology.AlternatingConst Mathlib.Algebra.Homology.Embedding.AreComplementary Mathlib.Algebra.Homology.Embedding.Connect Mathlib.Algebra.Homology.Embedding.ExtendHomology Mathlib.Algebra.Homology.Embedding.Extend Mathlib.Algebra.Homology.Embedding.HomEquiv Mathlib.Algebra.Homology.Embedding.IsSupported Mathlib.Algebra.Homology.Embedding.RestrictionHomology Mathlib.Algebra.Homology.Embedding.StupidTrunc Mathlib.Algebra.Homology.Embedding.TruncGEHomology Mathlib.Algebra.Homology.Embedding.TruncGE Mathlib.Algebra.Homology.Embedding.TruncLEHomology Mathlib.Algebra.Homology.Embedding.TruncLE Mathlib.Algebra.Homology.HomologySequenceLemmas Mathlib.Algebra.Homology.HomologySequence Mathlib.Algebra.Homology.HomotopyCategory Mathlib.Algebra.Homology.HomotopyCofiber Mathlib.Algebra.Homology.Homotopy Mathlib.Algebra.Homology.Localization Mathlib.Algebra.Homology.Opposite Mathlib.Algebra.Homology.QuasiIso Mathlib.Algebra.Homology.Refinements Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex Mathlib.Algebra.Homology.SingleHomology Mathlib.Algebra.Module.Card Mathlib.Algebra.Order.BigOperators.Expect Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.AlgebraicTopology.DoldKan.Decomposition Mathlib.AlgebraicTopology.DoldKan.Degeneracies Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian Mathlib.AlgebraicTopology.DoldKan.Equivalence Mathlib.AlgebraicTopology.DoldKan.Faces Mathlib.AlgebraicTopology.DoldKan.FunctorGamma Mathlib.AlgebraicTopology.DoldKan.FunctorN Mathlib.AlgebraicTopology.DoldKan.GammaCompN Mathlib.AlgebraicTopology.DoldKan.Homotopies Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence Mathlib.AlgebraicTopology.DoldKan.NCompGamma Mathlib.AlgebraicTopology.DoldKan.NReflectsIso Mathlib.AlgebraicTopology.DoldKan.Normalized Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.AlgebraicTopology.DoldKan.PInfty Mathlib.AlgebraicTopology.DoldKan.Projections Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject Mathlib.AlgebraicTopology.ExtraDegeneracy Mathlib.AlgebraicTopology.MooreComplex Mathlib.Analysis.BoxIntegral.Box.Basic Mathlib.Analysis.BoxIntegral.Partition.Basic Mathlib.Analysis.BoxIntegral.Partition.Split Mathlib.Analysis.BoxIntegral.Partition.Tagged Mathlib.Analysis.Normed.Group.Basic Mathlib.Analysis.Normed.Group.CocompactMap Mathlib.Analysis.Normed.Group.Constructions Mathlib.Analysis.Normed.Group.Int Mathlib.Analysis.Normed.Order.Basic Mathlib.Analysis.Normed.Order.Hom.Basic Mathlib.Analysis.Normed.Order.Hom.Ultra Mathlib.Analysis.NormedSpace.IndicatorFunction Mathlib.Analysis.Oscillation Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ColimCoyoneda Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject Mathlib.CategoryTheory.Abelian.Injective.Resolution Mathlib.CategoryTheory.Abelian.LeftDerived Mathlib.CategoryTheory.Abelian.Projective.Resolution Mathlib.CategoryTheory.Abelian.RightDerived Mathlib.CategoryTheory.Idempotents.SimplicialObject Mathlib.CategoryTheory.Monoidal.Tor Mathlib.CategoryTheory.Noetherian Mathlib.CategoryTheory.Preadditive.Injective.Resolution Mathlib.CategoryTheory.Preadditive.Projective.Resolution Mathlib.CategoryTheory.Simple Mathlib.CategoryTheory.Sites.Coherent.Basic Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology Mathlib.CategoryTheory.Sites.Coherent.Comparison Mathlib.CategoryTheory.Sites.Coherent.Equivalence Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves Mathlib.CategoryTheory.Sites.Coherent.RegularTopology Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit Mathlib.CategoryTheory.Sites.Coherent.SheafComparison Mathlib.CategoryTheory.Sites.ConstantSheaf Mathlib.CategoryTheory.Sites.DenseSubsite.Basic Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology Mathlib.CategoryTheory.Sites.DenseSubsite.SheafEquiv Mathlib.CategoryTheory.Sites.EpiMono Mathlib.CategoryTheory.Sites.Equivalence Mathlib.CategoryTheory.Sites.GlobalSections Mathlib.CategoryTheory.Sites.LeftExact Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.CategoryTheory.Sites.Pullback Mathlib.CategoryTheory.Subobject.ArtinianObject Mathlib.CategoryTheory.Subobject.NoetherianObject Mathlib.Combinatorics.Enumerative.IncidenceAlgebra Mathlib.Combinatorics.Pigeonhole Mathlib.Combinatorics.SimpleGraph.IncMatrix Mathlib.Data.Complex.BigOperators Mathlib.Data.DFinsupp.WellFounded Mathlib.Data.ENNReal.BigOperators Mathlib.Data.EReal.Inv Mathlib.Data.NNReal.Basic Mathlib.Data.Set.Card.Arithmetic Mathlib.Data.Setoid.Partition.Card Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.Geometry.RingedSpace.Stalks Mathlib.InformationTheory.Hamming Mathlib.MeasureTheory.OuterMeasure.Defs Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue Mathlib.Order.Filter.ENNReal Mathlib.Topology.Algebra.InfiniteSum.Basic Mathlib.Topology.Algebra.InfiniteSum.Defs Mathlib.Topology.Algebra.Star.Real Mathlib.Topology.Bornology.Real Mathlib.Topology.Category.CompHausLike.EffectiveEpi Mathlib.Topology.Compactness.PseudometrizableLindelof Mathlib.Topology.EMetricSpace.Basic Mathlib.Topology.EMetricSpace.Defs Mathlib.Topology.EMetricSpace.Diam Mathlib.Topology.EMetricSpace.Lipschitz Mathlib.Topology.EMetricSpace.Paracompact Mathlib.Topology.EMetricSpace.Pi Mathlib.Topology.Instances.Int Mathlib.Topology.Instances.Nat Mathlib.Topology.Instances.PNat Mathlib.Topology.MetricSpace.Antilipschitz Mathlib.Topology.MetricSpace.Basic Mathlib.Topology.MetricSpace.Bilipschitz Mathlib.Topology.MetricSpace.Bounded Mathlib.Topology.MetricSpace.Cauchy Mathlib.Topology.MetricSpace.Congruence Mathlib.Topology.MetricSpace.Defs Mathlib.Topology.MetricSpace.DilationEquiv Mathlib.Topology.MetricSpace.Dilation Mathlib.Topology.MetricSpace.Equicontinuity Mathlib.Topology.MetricSpace.Gluing Mathlib.Topology.MetricSpace.Infsep Mathlib.Topology.MetricSpace.Isometry Mathlib.Topology.MetricSpace.Lipschitz Mathlib.Topology.MetricSpace.MetricSeparated Mathlib.Topology.MetricSpace.ProperSpace.Lemmas Mathlib.Topology.MetricSpace.ProperSpace.Real Mathlib.Topology.MetricSpace.ProperSpace Mathlib.Topology.MetricSpace.Pseudo.Basic Mathlib.Topology.MetricSpace.Pseudo.Constructions Mathlib.Topology.MetricSpace.Pseudo.Defs Mathlib.Topology.MetricSpace.Pseudo.Lemmas Mathlib.Topology.MetricSpace.Pseudo.Pi Mathlib.Topology.MetricSpace.Pseudo.Real Mathlib.Topology.MetricSpace.Sequences Mathlib.Topology.MetricSpace.ShrinkingLemma Mathlib.Topology.MetricSpace.Similarity Mathlib.Topology.MetricSpace.Ultra.Basic Mathlib.Topology.MetricSpace.Ultra.Pi Mathlib.Topology.MetricSpace.Ultra.TotallySeparated Mathlib.Topology.Metrizable.Basic Mathlib.Topology.Metrizable.CompletelyMetrizable Mathlib.Topology.Metrizable.ContinuousMap Mathlib.Topology.Metrizable.Real Mathlib.Topology.Metrizable.Uniformity Mathlib.Topology.Order.Real Mathlib.Topology.Sheaves.Alexandrov Mathlib.Topology.Sheaves.Forget Mathlib.Topology.Sheaves.Functors Mathlib.Topology.Sheaves.Limits Mathlib.Topology.Sheaves.LocalPredicate Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Topology.Sheaves.PUnit Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.Topology.Sheaves.SheafCondition.Sites Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.Topology.Sheaves.Sheaf Mathlib.Topology.Sheaves.Sheafify Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.Sheaves.Stalks Mathlib.Topology.UniformSpace.Real |
13 |
20 filesMathlib.Analysis.Normed.Group.Seminorm Mathlib.Data.DFinsupp.Lex Mathlib.Data.ENNReal.Action Mathlib.Data.ENNReal.Basic Mathlib.Data.ENNReal.Holder Mathlib.Data.ENNReal.Inv Mathlib.Data.ENNReal.Lemmas Mathlib.Data.ENNReal.Operations Mathlib.Data.ENNReal.Order Mathlib.Data.ENNReal.Real Mathlib.Data.EReal.Basic Mathlib.Data.EReal.Operations Mathlib.Data.Int.WithZero Mathlib.Data.NNReal.Defs Mathlib.Data.NNReal.Star Mathlib.Data.Real.ConjExponents Mathlib.Data.Real.ENatENNReal Mathlib.Data.Real.EReal Mathlib.Data.Real.Embedding Mathlib.Data.Real.Pointwise |
14 |
28 filesMathlib.Algebra.Homology.Factorizations.Basic Mathlib.Algebra.Homology.GrothendieckAbelian Mathlib.Algebra.Homology.HomologicalComplexAbelian Mathlib.Algebra.Homology.ShortComplex.ExactFunctor Mathlib.Algebra.Module.BigOperators Mathlib.CategoryTheory.Abelian.Exact Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Connected Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Types Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic Mathlib.CategoryTheory.Abelian.Monomorphisms Mathlib.CategoryTheory.Abelian.Subobject Mathlib.CategoryTheory.Action.Limits Mathlib.CategoryTheory.Generator.Abelian Mathlib.CategoryTheory.Idempotents.HomologicalComplex Mathlib.CategoryTheory.Preadditive.CommGrp_ Mathlib.CategoryTheory.Preadditive.Mat Mathlib.CategoryTheory.Sites.Abelian Mathlib.CategoryTheory.Sites.Subsheaf Mathlib.Combinatorics.Enumerative.InclusionExclusion Mathlib.Data.Matrix.Action Mathlib.Data.Matrix.Mul Mathlib.Data.Matrix.PEquiv Mathlib.LinearAlgebra.Matrix.Integer Mathlib.LinearAlgebra.Matrix.Orthogonal Mathlib.NumberTheory.EllipticDivisibilitySequence |
15 |
61 filesMathlib.Algebra.BigOperators.Finprod Mathlib.Algebra.BigOperators.GroupWithZero.Action Mathlib.Algebra.Homology.ExactSequence Mathlib.Algebra.Homology.ShortComplex.Abelian Mathlib.Algebra.Homology.ShortComplex.Exact Mathlib.Algebra.Homology.ShortComplex.ShortExact Mathlib.Algebra.Homology.ShortComplex.SnakeLemma Mathlib.Algebra.Order.Module.Rat Mathlib.Algebra.QuadraticDiscriminant Mathlib.CategoryTheory.Abelian.Basic Mathlib.CategoryTheory.Abelian.CommSq Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel Mathlib.CategoryTheory.Abelian.FunctorCategory Mathlib.CategoryTheory.Abelian.Opposite Mathlib.CategoryTheory.Abelian.Refinements Mathlib.CategoryTheory.Abelian.SerreClass.Basic Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty Mathlib.CategoryTheory.Abelian.Transfer Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems Mathlib.CategoryTheory.Generator.Sheaf Mathlib.CategoryTheory.Idempotents.Basic Mathlib.CategoryTheory.Idempotents.Biproducts Mathlib.CategoryTheory.Idempotents.FunctorCategories Mathlib.CategoryTheory.Idempotents.FunctorExtension Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi Mathlib.CategoryTheory.Idempotents.Karoubi Mathlib.CategoryTheory.ObjectProperty.EpiMono Mathlib.CategoryTheory.ObjectProperty.Extensions Mathlib.CategoryTheory.Preadditive.LeftExact Mathlib.CategoryTheory.Preadditive.LiftToFinset Mathlib.CategoryTheory.Sites.Adjunction Mathlib.CategoryTheory.Sites.Canonical Mathlib.CategoryTheory.Sites.CartesianClosed Mathlib.CategoryTheory.Sites.CartesianMonoidal Mathlib.CategoryTheory.Sites.ChosenFiniteProducts Mathlib.CategoryTheory.Sites.CompatiblePlus Mathlib.CategoryTheory.Sites.CompatibleSheafification Mathlib.CategoryTheory.Sites.ConcreteSheafification Mathlib.CategoryTheory.Sites.Continuous Mathlib.CategoryTheory.Sites.CoverLifting Mathlib.CategoryTheory.Sites.CoverPreserving Mathlib.CategoryTheory.Sites.Coverage Mathlib.CategoryTheory.Sites.CoversTop Mathlib.CategoryTheory.Sites.IsSheafOneHypercover Mathlib.CategoryTheory.Sites.Limits Mathlib.CategoryTheory.Sites.Localization Mathlib.CategoryTheory.Sites.Monoidal Mathlib.CategoryTheory.Sites.OneHypercover Mathlib.CategoryTheory.Sites.Over Mathlib.CategoryTheory.Sites.Plus Mathlib.CategoryTheory.Sites.PreservesSheafification Mathlib.CategoryTheory.Sites.SheafHom Mathlib.CategoryTheory.Sites.Sheaf Mathlib.CategoryTheory.Sites.Sheafification Mathlib.CategoryTheory.Sites.Subcanonical Mathlib.CategoryTheory.Sites.Types Mathlib.CategoryTheory.Sites.Whiskering Mathlib.CategoryTheory.Sites.ZeroHypercover |
16 |
21 filesMathlib.Algebra.Homology.Additive Mathlib.Algebra.Homology.Augment Mathlib.Algebra.Homology.DifferentialObject Mathlib.Algebra.Homology.Double Mathlib.Algebra.Homology.Embedding.Boundary Mathlib.Algebra.Homology.Embedding.Restriction Mathlib.Algebra.Homology.Functor Mathlib.Algebra.Homology.HomologicalBicomplex Mathlib.Algebra.Homology.HomologicalComplexBiprod Mathlib.Algebra.Homology.HomologicalComplexLimits Mathlib.Algebra.Homology.HomologicalComplex Mathlib.Algebra.Homology.ImageToKernel Mathlib.Algebra.Homology.Linear Mathlib.Algebra.Homology.Single Mathlib.CategoryTheory.Dialectica.Monoidal Mathlib.CategoryTheory.Generator.Basic Mathlib.CategoryTheory.Generator.HomologicalComplex Mathlib.CategoryTheory.Generator.Preadditive Mathlib.CategoryTheory.Generator.Presheaf Mathlib.CategoryTheory.Subobject.Lattice Mathlib.CategoryTheory.Subobject.Limits |
17 |
11 filesMathlib.Algebra.Homology.Square Mathlib.Algebra.Order.Rearrangement Mathlib.CategoryTheory.Distributive.Cartesian Mathlib.CategoryTheory.Distributive.Monoidal Mathlib.CategoryTheory.Monoidal.Subcategory Mathlib.CategoryTheory.Shift.Opposite Mathlib.CategoryTheory.Shift.Pullback Mathlib.CategoryTheory.Shift.ShiftedHomOpposite Mathlib.CategoryTheory.Subobject.FactorThru Mathlib.CategoryTheory.Triangulated.Opposite.Basic Mathlib.CategoryTheory.Triangulated.Opposite.Triangle |
18 |
39 filesMathlib.Algebra.Category.Grp.Preadditive Mathlib.Algebra.Category.Grp.ZModuleEquivalence Mathlib.Algebra.Category.ModuleCat.Basic Mathlib.Algebra.Homology.CommSq Mathlib.Algebra.Homology.ShortComplex.Linear Mathlib.Algebra.Homology.ShortComplex.Preadditive Mathlib.Algebra.Order.Floor.Div Mathlib.CategoryTheory.Abelian.NonPreadditive Mathlib.CategoryTheory.Adjunction.Additive Mathlib.CategoryTheory.Center.Linear Mathlib.CategoryTheory.Center.Localization Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures Mathlib.CategoryTheory.Linear.Basic Mathlib.CategoryTheory.Linear.FunctorCategory Mathlib.CategoryTheory.Linear.LinearFunctor Mathlib.CategoryTheory.Linear.Yoneda Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive Mathlib.CategoryTheory.Localization.Linear Mathlib.CategoryTheory.Localization.Preadditive Mathlib.CategoryTheory.Localization.SmallShiftedHom Mathlib.CategoryTheory.Monoidal.Linear Mathlib.CategoryTheory.Monoidal.Preadditive Mathlib.CategoryTheory.Preadditive.AdditiveFunctor Mathlib.CategoryTheory.Preadditive.Basic Mathlib.CategoryTheory.Preadditive.Biproducts Mathlib.CategoryTheory.Preadditive.EilenbergMoore Mathlib.CategoryTheory.Preadditive.EndoFunctor Mathlib.CategoryTheory.Preadditive.FunctorCategory Mathlib.CategoryTheory.Preadditive.Opposite Mathlib.CategoryTheory.Preadditive.SingleObj Mathlib.CategoryTheory.Preadditive.Transfer Mathlib.CategoryTheory.Preadditive.Yoneda.Basic Mathlib.CategoryTheory.Quotient.Linear Mathlib.CategoryTheory.Quotient.Preadditive Mathlib.CategoryTheory.Shift.InducedShiftSequence Mathlib.CategoryTheory.Shift.Linear Mathlib.CategoryTheory.Shift.ShiftSequence Mathlib.CategoryTheory.Shift.ShiftedHom Mathlib.CategoryTheory.Triangulated.Rotate |
19 |
Mathlib.Algebra.Order.Module.Pointwise |
24 |
Mathlib.Algebra.Group.EvenFunction |
39 |
3 filesMathlib.Algebra.Order.Module.Algebra Mathlib.Tactic.LinearCombination Mathlib.Tactic.Polyrith |
40 |
Mathlib.Algebra.Algebra.Rat Mathlib.Data.DFinsupp.Order |
41 |
5 filesMathlib.Algebra.Module.Equiv.Basic Mathlib.Algebra.Module.LinearMap.Rat Mathlib.Algebra.Order.Algebra Mathlib.Algebra.Order.Module.Equiv Mathlib.LinearAlgebra.GeneralLinearGroup |
43 |
4 filesMathlib.Algebra.Module.Rat Mathlib.Algebra.Order.Module.OrderedSMul Mathlib.Algebra.Order.Monovary Mathlib.Tactic.LinearCombination.Lemmas |
44 |
Mathlib.Algebra.Module.Hom |
47 |
Mathlib.Algebra.Order.Module.Field |
51 |
Mathlib.Algebra.Order.Module.Basic Mathlib.Algebra.Order.Module.Defs |
67 |
Mathlib.Algebra.NoZeroSMulDivisors.Basic |
88 |
Mathlib.Algebra.Module.End |
89 |
Mathlib.Analysis.NormedSpace.MStructure |
928 |
Declarations diff
+ AddMonoid.End.ker_id_sub_eq_range
+ AddMonoidHom.ker_coprod_of_disjoint_range
+ AddMonoidHom.ker_prod_ker_le_ker_coprod
+ AddSubgroup.prodEquivOfIsCompl
+ AddSubgroup.sup_eq_range
+ IsIdempotentElem.ker_id_sub_eq_range_cont
+ IsIdempotentElem.range_id_sub_eq_ker_cont
+ IsLprojection.contractive2
+ IsLprojection.range_sum
+ IsLsummand
+ IsLsummand.Lnorm
+ IsLsummand.compl
+ IsLsummand.sup_top
+ IsMideal
+ IsMideal.inter
+ IsMideal.isSublattice
+ L1_norm_inr
+ Lprojections
+ Lsummand.IsClosed
+ Lsummand.IsCompl
+ Lsummands
+ Mprojections
+ WithLp.prod_norm_eq_of_1
+ _root_.IsIdempotentElem.mem_range_iff_self_smul
+ _root_.Lprojections.Lnorm
+ _root_.Lprojections.range
+ bijection
+ commute
+ compl_mul_self
+ contractive
+ idempotentOfClosedCompl
+ instance : Bot (Lsummands G)
+ instance : FunLike Pₗ[𝕜](A) A A
+ instance : FunLike { P : M // IsLprojection X P } X X
+ instance : FunLike ℙᴸ[M](X) X X
+ instance : PartialOrder (Lsummands G) := Subtype.partialOrder fun f ↦ IsLsummand G f
+ instance : Top (Lsummands G)
+ instance [FaithfulSMul M X] : Lattice ℙᴸ[M](X)
+ instance _root_.Lsummands.Subtype.sup [FaithfulSMul M X] : Max (Lsummands X)
+ is_idempotent_ofClosedCompl
+ ker_id_sub_idempotentOfClosedCompl
+ ker_idempotentOfClosedCompl
+ l1map
+ l1map_isometry
+ mem_iff_invariant_ofClosedCompl
+ mem_iff_zero_ofClosedCompl
+ prodEquivₗᵢ
+ prod_nnnorm_equiv
+ range_id_sub_eq_ker
+ range_id_sub_idempotentOfClosedCompl
+ range_idempotentOfClosedCompl
+ range_inter
+ range_sum
+ surjective
+ toAddMonoidEnd
+ unique_Lcomplement
+ unit_ball_conv
++ ker_id_sub_eq_range
+-+ Subtype.hasCompl
- instance [FaithfulSMul M X] : Lattice { P : M // IsLprojection X P }
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
Increase in tech debt: (relative, absolute) = (1.00, 0.33)
| Current number | Change | Type |
|---|---|---|
| 3 | 1 | maxHeartBeats modifications |
Current commit fd913a8c1e
Reference commit d03aa1faf7
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
Collaborator
|
This pull request has conflicts, please merge |
Collaborator
|
This pull request has conflicts, please merge |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR continues the work from #14369.
Original PR: #14369