mathlib4 feat(Analysis/NormedSpace/MStructure): M-ideals

feat(Analysis/NormedSpace/MStructure): M-ideals

Open mans0954 opened this issue 1 year ago • 1 comments

WiP: Define M-ideals and establish basic properties.

Jul 02 '24 21:07 mans0954

PR summary 8b2141b23d

Import changes exceeding 2%

%	File
+22.68%	`Mathlib.Algebra.Module.End`
+10.86%	`Mathlib.Algebra.Module.Hom`
+83.33%	`Mathlib.Analysis.NormedSpace.MStructure`

Import changes for modified files

Dependency changes

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 files `Mathlib.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 files `Mathlib.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 files `Mathlib.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 files `Mathlib.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 files `Mathlib.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 files `Mathlib.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 files `Mathlib.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 files `Mathlib.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 files `Mathlib.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 files `Mathlib.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 files `Mathlib.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 files `Mathlib.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 files `Mathlib.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 files `Mathlib.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 files `Mathlib.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 files `Mathlib.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 relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Jul 02 '24 21:07 github-actions[bot]

This PR/issue depends on:

~~leanprover-community/mathlib4#14458~~ By Dependent Issues (🤖). Happy coding!

Jul 16 '24 00:07 leanprover-community-mathlib4-bot

This PR has been migrated to a fork-based workflow: https://github.com/leanprover-community/mathlib4/pull/26337

Jun 24 '25 06:06 mans0954

mathlib4 mathlib4 copied to clipboard

feat(Analysis/NormedSpace/MStructure): M-ideals

PR summary 8b2141b23d

Import changes for modified files

Declarations diff

mathlib4
mathlib4 copied to clipboard