feat: add `CharZero`/`CharP` instances on `OrderDual` and `Lex` by NoahW314 · Pull Request #42541 · leanprover-community/mathlib4

NoahW314 · 2026-08-07T15:51:27Z

github-actions · 2026-08-07T15:52:56Z

PR summary 4606c8371a

Import changes exceeding 2%

%	File
+144.10%	`Mathlib.Algebra.Order.Ring.Synonym`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Order.Ring.Synonym	161	393	+232 (+144.10%)
Mathlib.LinearAlgebra.Eigenspace.Basic	1411	1413	+2 (+0.14%)

Import changes for all files

Files	Import difference
44 files `Mathlib.Algebra.GCDMonoid.FinsetLemmas` `Mathlib.Algebra.Order.Antidiag.Nat` `Mathlib.Combinatorics.Schnirelmann` `Mathlib.Data.Nat.Choose.Factorization` `Mathlib.Data.Nat.Factorization.Basic` `Mathlib.Data.Nat.Factorization.Defs` `Mathlib.Data.Nat.Factorization.Divisors` `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.Data.Nat.Squarefree` `Mathlib.Data.Num.Prime` `Mathlib.Data.PNat.Xgcd` `Mathlib.GroupTheory.GroupAction.Iwasawa` `Mathlib.GroupTheory.GroupAction.Primitive` `Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup` `Mathlib.LinearAlgebra.FixedSubmodule` `Mathlib.NumberTheory.AlmostPrime` `Mathlib.NumberTheory.ArithmeticFunction.Defs` `Mathlib.NumberTheory.ArithmeticFunction.Liouville` `Mathlib.NumberTheory.ArithmeticFunction.Misc` `Mathlib.NumberTheory.ArithmeticFunction.Moebius` `Mathlib.NumberTheory.ArithmeticFunction.Zeta` `Mathlib.NumberTheory.Dioph` `Mathlib.NumberTheory.FactorisationProperties` `Mathlib.NumberTheory.FrobeniusNumber` `Mathlib.NumberTheory.Harmonic.Int` `Mathlib.NumberTheory.MaricaSchoenheim` `Mathlib.NumberTheory.Multiplicity` `Mathlib.NumberTheory.Padics.PadicNorm` `Mathlib.NumberTheory.Padics.PadicNumbers` `Mathlib.NumberTheory.Padics.PadicVal.Basic` `Mathlib.NumberTheory.PellMatiyasevic` `Mathlib.NumberTheory.SelbergSieve` `Mathlib.NumberTheory.Zsqrtd.GaussianInt` `Mathlib.RingTheory.ChainOfDivisors` `Mathlib.RingTheory.Ideal.NatInt` `Mathlib.RingTheory.Int.Basic` `Mathlib.RingTheory.Localization.Rat` `Mathlib.RingTheory.Radical.NatInt` `Mathlib.RingTheory.Radical` `Mathlib.RingTheory.UniqueFactorizationDomain.Moebius`	1
1066 files `Mathlib.Algebra.AffineMonoid.Embedding` `Mathlib.Algebra.AffineMonoid.UniqueSums` `Mathlib.Algebra.Algebra.Bilinear` `Mathlib.Algebra.Algebra.Epi` `Mathlib.Algebra.Algebra.NonUnitalSubalgebra` `Mathlib.Algebra.Algebra.Operations` `Mathlib.Algebra.Algebra.RestrictScalars` `Mathlib.Algebra.Algebra.Spectrum.Basic` `Mathlib.Algebra.Algebra.Spectrum.Pi` `Mathlib.Algebra.Algebra.Spectrum.Quasispectrum` `Mathlib.Algebra.Algebra.StrictPositivity` `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.Operations` `Mathlib.Algebra.Algebra.Subalgebra.Order` `Mathlib.Algebra.Algebra.Subalgebra.Pi` `Mathlib.Algebra.Algebra.Subalgebra.Pointwise` `Mathlib.Algebra.Algebra.Subalgebra.Prod` `Mathlib.Algebra.Algebra.Subalgebra.Tower` `Mathlib.Algebra.Algebra.Subalgebra.Unitization` `Mathlib.Algebra.Algebra.Tower` `Mathlib.Algebra.Algebra.Unitization` `Mathlib.Algebra.Azumaya.Defs` `Mathlib.Algebra.Azumaya.Matrix` `Mathlib.Algebra.Category.AlgCat.Basic` `Mathlib.Algebra.Category.AlgCat.FilteredColimits` `Mathlib.Algebra.Category.AlgCat.Limits` `Mathlib.Algebra.Category.AlgCat.Monoidal` `Mathlib.Algebra.Category.AlgCat.Symmetric` `Mathlib.Algebra.Category.AlgCat.TensorAlgebra` `Mathlib.Algebra.Category.BialgCat.Basic` `Mathlib.Algebra.Category.BialgCat.Monoidal` `Mathlib.Algebra.Category.CoalgCat.Basic` `Mathlib.Algebra.Category.CoalgCat.ComonEquivalence` `Mathlib.Algebra.Category.CoalgCat.Monoidal` `Mathlib.Algebra.Category.Grp.AB` `Mathlib.Algebra.Category.Grp.Abelian` `Mathlib.Algebra.Category.Grp.Images` `Mathlib.Algebra.Category.Grp.Injective` `Mathlib.Algebra.Category.Grp.IsFinite` `Mathlib.Algebra.Category.Grp.Subobject` `Mathlib.Algebra.Category.HopfAlgCat.Basic` `Mathlib.Algebra.Category.HopfAlgCat.Monoidal` `Mathlib.Algebra.Category.ModuleCat.AB` `Mathlib.Algebra.Category.ModuleCat.Abelian` `Mathlib.Algebra.Category.ModuleCat.Adjunctions` `Mathlib.Algebra.Category.ModuleCat.Algebra` `Mathlib.Algebra.Category.ModuleCat.Biproducts` `Mathlib.Algebra.Category.ModuleCat.ChangeOfRingsExact` `Mathlib.Algebra.Category.ModuleCat.ChangeOfRings` `Mathlib.Algebra.Category.ModuleCat.Colimits` `Mathlib.Algebra.Category.ModuleCat.EpiMono` `Mathlib.Algebra.Category.ModuleCat.FilteredColimits` `Mathlib.Algebra.Category.ModuleCat.Free` `Mathlib.Algebra.Category.ModuleCat.Images` `Mathlib.Algebra.Category.ModuleCat.Injective` `Mathlib.Algebra.Category.ModuleCat.Kernels` `Mathlib.Algebra.Category.ModuleCat.LeftResolution` `Mathlib.Algebra.Category.ModuleCat.Limits` `Mathlib.Algebra.Category.ModuleCat.Localization` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Adjunction` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed` `Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian` `Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings` `Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits` `Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Free` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback` `Mathlib.Algebra.Category.ModuleCat.Presheaf.PushforwardZeroMonoidal` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule` `Mathlib.Algebra.Category.ModuleCat.Presheaf` `Mathlib.Algebra.Category.ModuleCat.Products` `Mathlib.Algebra.Category.ModuleCat.Projective` `Mathlib.Algebra.Category.ModuleCat.Pseudofunctor` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian` `Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Free` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization` `Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree` `Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous` `Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree` `Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent` `Mathlib.Algebra.Category.ModuleCat.Sheaf` `Mathlib.Algebra.Category.ModuleCat.Simple` `Mathlib.Algebra.Category.ModuleCat.Stalk` `Mathlib.Algebra.Category.ModuleCat.Subobject` `Mathlib.Algebra.Category.ModuleCat.Tannaka` `Mathlib.Algebra.Category.ModuleCat.Topology.Basic` `Mathlib.Algebra.Category.ModuleCat.Topology.Homology` `Mathlib.Algebra.Category.ModuleCat.Ulift` `Mathlib.Algebra.Category.Ring.Adjunctions` `Mathlib.Algebra.Category.Ring.Epi` `Mathlib.Algebra.Central.Basic` `Mathlib.Algebra.Central.Defs` `Mathlib.Algebra.Central.End` `Mathlib.Algebra.Central.Matrix` `Mathlib.Algebra.Colimit.Finiteness` `Mathlib.Algebra.Colimit.Module` `Mathlib.Algebra.Colimit.TensorProduct` `Mathlib.Algebra.DirectSum.Algebra` `Mathlib.Algebra.DirectSum.Decomposition` `Mathlib.Algebra.DirectSum.Finsupp` `Mathlib.Algebra.DirectSum.Idempotents` `Mathlib.Algebra.DirectSum.Internal` `Mathlib.Algebra.DirectSum.Module` `Mathlib.Algebra.DualNumber` `Mathlib.Algebra.DualQuaternion` `Mathlib.Algebra.Exact.Basic` `Mathlib.Algebra.Exact.Sequence` `Mathlib.Algebra.Exact` `Mathlib.Algebra.FiveLemma` `Mathlib.Algebra.FreeAlgebra` `Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra` `Mathlib.Algebra.Group.UniqueProds.VectorSpace` `Mathlib.Algebra.Homology.ConcreteCategory` `Mathlib.Algebra.Homology.LocalCohomology` `Mathlib.Algebra.Homology.ShortComplex.Ab` `Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory` `Mathlib.Algebra.Homology.ShortComplex.ModuleCat` `Mathlib.Algebra.Jordan.Basic` `Mathlib.Algebra.Lie.Abelian` `Mathlib.Algebra.Lie.AdjointAction.Derivation` `Mathlib.Algebra.Lie.BaseChange` `Mathlib.Algebra.Lie.Cochain` `Mathlib.Algebra.Lie.Derivation.Basic` `Mathlib.Algebra.Lie.DirectSum` `Mathlib.Algebra.Lie.Extension` `Mathlib.Algebra.Lie.Free` `Mathlib.Algebra.Lie.Graded` `Mathlib.Algebra.Lie.IdealOperations` `Mathlib.Algebra.Lie.Ideal` `Mathlib.Algebra.Lie.Normalizer` `Mathlib.Algebra.Lie.OfAssociative` `Mathlib.Algebra.Lie.Prod` `Mathlib.Algebra.Lie.Quotient` `Mathlib.Algebra.Lie.SemiDirect` `Mathlib.Algebra.Lie.Subalgebra` `Mathlib.Algebra.Lie.Submodule` `Mathlib.Algebra.Lie.TensorProduct` `Mathlib.Algebra.Lie.UniversalEnveloping` `Mathlib.Algebra.Module.Bimodule` `Mathlib.Algebra.Module.GradedModule` `Mathlib.Algebra.Module.Injective` `Mathlib.Algebra.Module.Lattice` `Mathlib.Algebra.Module.LinearMap.FiniteRange` `Mathlib.Algebra.Module.LinearMap.Index` `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.SpanRank` `Mathlib.Algebra.Module.Submodule.Bilinear` `Mathlib.Algebra.MonoidAlgebra.Basic` `Mathlib.Algebra.MonoidAlgebra.Degree` `Mathlib.Algebra.MonoidAlgebra.Grading` `Mathlib.Algebra.MonoidAlgebra.Ideal` `Mathlib.Algebra.MonoidAlgebra.Module` `Mathlib.Algebra.MonoidAlgebra.Support` `Mathlib.Algebra.MonoidAlgebra.ToDirectSum` `Mathlib.Algebra.MvPolynomial.Basic` `Mathlib.Algebra.MvPolynomial.Coeff` `Mathlib.Algebra.MvPolynomial.Comap` `Mathlib.Algebra.MvPolynomial.CommRing` `Mathlib.Algebra.MvPolynomial.Counit` `Mathlib.Algebra.MvPolynomial.Degrees` `Mathlib.Algebra.MvPolynomial.Division` `Mathlib.Algebra.MvPolynomial.Eval` `Mathlib.Algebra.MvPolynomial.Invertible` `Mathlib.Algebra.MvPolynomial.Monad` `Mathlib.Algebra.MvPolynomial.Rename` `Mathlib.Algebra.MvPolynomial.Supported` `Mathlib.Algebra.MvPolynomial.Variables` `Mathlib.Algebra.Order.Module.HahnEmbedding` `Mathlib.Algebra.Order.Ring.Archimedean` `Mathlib.Algebra.Order.Ring.Ordering.Basic` `Mathlib.Algebra.Order.Ring.Ordering.Defs` `Mathlib.Algebra.Polynomial.Basic` `Mathlib.Algebra.Polynomial.Basis` `Mathlib.Algebra.Polynomial.Cardinal` `Mathlib.Algebra.Polynomial.Degree.Definitions` `Mathlib.Algebra.Polynomial.Degree.Defs` `Mathlib.Algebra.Polynomial.Degree.Monomial` `Mathlib.Algebra.Polynomial.Eval.Algebra` `Mathlib.Algebra.Polynomial.Eval.Defs` `Mathlib.Algebra.Polynomial.Monomial` `Mathlib.Algebra.QuadraticAlgebra.Basic` `Mathlib.Algebra.QuadraticAlgebra.Defs` `Mathlib.Algebra.QuaternionBasis` `Mathlib.Algebra.Quaternion` `Mathlib.Algebra.Ring.Divisibility.Lemmas` `Mathlib.Algebra.Ring.IsFormallyReal` `Mathlib.Algebra.RingQuot` `Mathlib.Algebra.SkewMonoidAlgebra.Basic` `Mathlib.Algebra.SkewMonoidAlgebra.Lift` `Mathlib.Algebra.SkewMonoidAlgebra.Single` `Mathlib.Algebra.SkewMonoidAlgebra.Support` `Mathlib.Algebra.SkewPolynomial.Basic` `Mathlib.Algebra.Squarefree.Basic` `Mathlib.Algebra.Star.Free` `Mathlib.Algebra.Star.LinearMap` `Mathlib.Algebra.Star.Module` `Mathlib.Algebra.Star.NonUnitalSubalgebra` `Mathlib.Algebra.Star.RingQuot` `Mathlib.Algebra.Star.Subalgebra` `Mathlib.Algebra.Star.TensorProduct` `Mathlib.Algebra.Star.UnitaryStarAlgAut` `Mathlib.Algebra.Star.Unitary` `Mathlib.Algebra.Symmetrized` `Mathlib.Algebra.TrivSqZeroExt.Basic` `Mathlib.Algebra.TrivSqZeroExt.Ideal` `Mathlib.Algebra.TrivSqZeroExt` `Mathlib.Algebra.Vertex.HVertexOperator` `Mathlib.Algebra.Vertex.VertexOperator` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology` `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.SimplicialComplex.Basic` `Mathlib.AlgebraicTopology.SimplicialSet.TopAdj` `Mathlib.AlgebraicTopology.SingularHomology.Basic` `Mathlib.AlgebraicTopology.SingularHomology.HomologyZero` `Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvarianceTopCat` `Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance` `Mathlib.AlgebraicTopology.SingularSet` `Mathlib.AlgebraicTopology.TopologicalSimplex` `Mathlib.Analysis.AperiodicOrder.Delone.Basic` `Mathlib.Analysis.Asymptotics.AsymptoticEquivalent` `Mathlib.Analysis.Asymptotics.Completion` `Mathlib.Analysis.Asymptotics.Defs` `Mathlib.Analysis.Asymptotics.Lemmas` `Mathlib.Analysis.Asymptotics.LinearGrowth` `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.CStarAlgebra.Basic` `Mathlib.Analysis.CStarAlgebra.Module.Synonym` `Mathlib.Analysis.CStarAlgebra.Unitary.Maps` `Mathlib.Analysis.Calculus.Deriv.Basic` `Mathlib.Analysis.Calculus.Deriv.Comp` `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.OfCompLeft` `Mathlib.Analysis.Calculus.FDeriv.RestrictScalars` `Mathlib.Analysis.Calculus.FormalMultilinearSeries` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn` `Mathlib.Analysis.Calculus.TangentCone.Basic` `Mathlib.Analysis.Calculus.TangentCone.DimOne` `Mathlib.Analysis.Calculus.TangentCone.Pi` `Mathlib.Analysis.Calculus.TangentCone.Prod` `Mathlib.Analysis.Calculus.TangentCone.ProperSpace` `Mathlib.Analysis.Calculus.TangentCone.Real` `Mathlib.Analysis.Complex.Cardinality` `Mathlib.Analysis.Convex.Basic` `Mathlib.Analysis.Convex.Body` `Mathlib.Analysis.Convex.Caratheodory` `Mathlib.Analysis.Convex.Combination` `Mathlib.Analysis.Convex.Cone.Basic` `Mathlib.Analysis.Convex.Cone.Closure` `Mathlib.Analysis.Convex.Cone.Extension` `Mathlib.Analysis.Convex.ContinuousLinearEquiv` `Mathlib.Analysis.Convex.Contractible` `Mathlib.Analysis.Convex.EGauge` `Mathlib.Analysis.Convex.Exposed` `Mathlib.Analysis.Convex.Extrema` `Mathlib.Analysis.Convex.Extreme` `Mathlib.Analysis.Convex.FunctionTopology` `Mathlib.Analysis.Convex.Function` `Mathlib.Analysis.Convex.Hull` `Mathlib.Analysis.Convex.Independent` `Mathlib.Analysis.Convex.Jensen` `Mathlib.Analysis.Convex.Join` `Mathlib.Analysis.Convex.LinearIsometry` `Mathlib.Analysis.Convex.MetricSpace` `Mathlib.Analysis.Convex.Mul` `Mathlib.Analysis.Convex.NNReal` `Mathlib.Analysis.Convex.PathConnected` `Mathlib.Analysis.Convex.Piecewise` `Mathlib.Analysis.Convex.Quasiconvex` `Mathlib.Analysis.Convex.Segment` `Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion` `Mathlib.Analysis.Convex.SimplicialComplex.Basic` `Mathlib.Analysis.Convex.Slope` `Mathlib.Analysis.Convex.Star` `Mathlib.Analysis.Convex.StdSimplex` `Mathlib.Analysis.Convex.StoneSeparation` `Mathlib.Analysis.Convex.StrictCombination` `Mathlib.Analysis.Convex.StrictConvexSpace` `Mathlib.Analysis.Convex.Strict` `Mathlib.Analysis.Convex.Topology` `Mathlib.Analysis.Convex.TotallyBounded` `Mathlib.Analysis.Convex.Uniform` `Mathlib.Analysis.Fourier.Notation` `Mathlib.Analysis.Hofer` `Mathlib.Analysis.LocallyConvex.AbsConvex` `Mathlib.Analysis.LocallyConvex.BalancedCoreHull` `Mathlib.Analysis.LocallyConvex.Barrelled` `Mathlib.Analysis.LocallyConvex.Basic` `Mathlib.Analysis.LocallyConvex.Bounded` `Mathlib.Analysis.LocallyConvex.PointwiseConvergence` `Mathlib.Analysis.LocallyConvex.Polar` `Mathlib.Analysis.LocallyConvex.StrongTopology` `Mathlib.Analysis.LocallyConvex.WithSeminorms` `Mathlib.Analysis.Normed.Affine.ContinuousAffineMap` `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.TransferInstance` `Mathlib.Analysis.Normed.Field.Ultra` `Mathlib.Analysis.Normed.Field.UnitBall` `Mathlib.Analysis.Normed.Group.AddCircle` `Mathlib.Analysis.Normed.Group.AddTorsor` `Mathlib.Analysis.Normed.Group.BallSphere` `Mathlib.Analysis.Normed.Group.Completeness` `Mathlib.Analysis.Normed.Group.Completion` `Mathlib.Analysis.Normed.Group.FunctionSeries` `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.Quotient` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels` `Mathlib.Analysis.Normed.Group.SemiNormedGrp` `Mathlib.Analysis.Normed.Group.SeparationQuotient` `Mathlib.Analysis.Normed.Group.Ultra` `Mathlib.Analysis.Normed.Group.Uniform` `Mathlib.Analysis.Normed.Group.ZeroAtInfty` `Mathlib.Analysis.Normed.Lp.WithLp` `Mathlib.Analysis.Normed.Module.Alternating.Basic` `Mathlib.Analysis.Normed.Module.Alternating.Curry` `Mathlib.Analysis.Normed.Module.Ball.Action` `Mathlib.Analysis.Normed.Module.Ball.Homeomorph` `Mathlib.Analysis.Normed.Module.Ball.Pointwise` `Mathlib.Analysis.Normed.Module.Ball.RadialEquiv` `Mathlib.Analysis.Normed.Module.Basic` `Mathlib.Analysis.Normed.Module.Completion` `Mathlib.Analysis.Normed.Module.Convex` `Mathlib.Analysis.Normed.Module.Extr` `Mathlib.Analysis.Normed.Module.Multilinear.Basic` `Mathlib.Analysis.Normed.Module.Multilinear.Curry` `Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm` `Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm` `Mathlib.Analysis.Normed.Module.RCLike.Real` `Mathlib.Analysis.Normed.Module.Ray` `Mathlib.Analysis.Normed.Module.Shrink` `Mathlib.Analysis.Normed.Module.Span` `Mathlib.Analysis.Normed.Module.TransferInstance` `Mathlib.Analysis.Normed.MulAction` `Mathlib.Analysis.Normed.Operator.Asymptotics` `Mathlib.Analysis.Normed.Operator.BanachSteinhaus` `Mathlib.Analysis.Normed.Operator.Banach` `Mathlib.Analysis.Normed.Operator.Basic` `Mathlib.Analysis.Normed.Operator.Bilinear` `Mathlib.Analysis.Normed.Operator.Compact.Basic` `Mathlib.Analysis.Normed.Operator.Compact` `Mathlib.Analysis.Normed.Operator.Completeness` `Mathlib.Analysis.Normed.Operator.Conformal` `Mathlib.Analysis.Normed.Operator.ContinuousLinearMap` `Mathlib.Analysis.Normed.Operator.Extend` `Mathlib.Analysis.Normed.Operator.LinearIsometry` `Mathlib.Analysis.Normed.Operator.Mul` `Mathlib.Analysis.Normed.Operator.NNNorm` `Mathlib.Analysis.Normed.Operator.NormedSpace` `Mathlib.Analysis.Normed.Operator.Prod` `Mathlib.Analysis.Normed.Order.Lattice` `Mathlib.Analysis.Normed.Order.UpperLower` `Mathlib.Analysis.Normed.Ring.Basic` `Mathlib.Analysis.Normed.Ring.InfiniteSum` `Mathlib.Analysis.Normed.Ring.Int` `Mathlib.Analysis.Normed.Ring.Lemmas` `Mathlib.Analysis.Normed.Ring.TransferInstance` `Mathlib.Analysis.Normed.Ring.Ultra` `Mathlib.Analysis.Normed.Ring.WithAbs` `Mathlib.Analysis.NormedSpace.FunctionSeries` `Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness` `Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm` `Mathlib.Analysis.NormedSpace.OperatorNorm.Prod` `Mathlib.Analysis.NormedSpace.Real` `Mathlib.Analysis.ODE.Basic` `Mathlib.Analysis.Real.Cardinality` `Mathlib.Analysis.Real.Spectrum` `Mathlib.Analysis.Seminorm` `Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean` `Mathlib.Analysis.SpecialFunctions.Choose` `Mathlib.Analysis.SpecificLimits.ArithmeticGeometric` `Mathlib.Analysis.SpecificLimits.Basic` `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.Pseudoelements` `Mathlib.CategoryTheory.Abelian.Yoneda` `Mathlib.CategoryTheory.Monoidal.Internal.Module` `Mathlib.CategoryTheory.Preadditive.HomOrthogonal` `Mathlib.CategoryTheory.Preadditive.Yoneda.Injective` `Mathlib.CategoryTheory.Preadditive.Yoneda.Limits` `Mathlib.CategoryTheory.Preadditive.Yoneda.Projective` `Mathlib.CategoryTheory.Sites.MayerVietorisSquare` `Mathlib.Combinatorics.Enumerative.Pentagonal.Ring` `Mathlib.Combinatorics.Optimization.ValuedCSP` `Mathlib.Computability.TMComputable` `Mathlib.Computability.TuringMachine.Computable` `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.DualNumber` `Mathlib.Data.Matrix.Invertible` `Mathlib.Data.Matrix.Reflection` `Mathlib.Dynamics.BirkhoffSum.QuasiMeasurePreserving` `Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber` `Mathlib.Dynamics.Ergodic.Action.Basic` `Mathlib.Dynamics.Ergodic.Conservative` `Mathlib.Dynamics.Ergodic.Ergodic` `Mathlib.Dynamics.Ergodic.MeasurePreserving` `Mathlib.FieldTheory.Finiteness` `Mathlib.FieldTheory.RatFunc.Defs` `Mathlib.FieldTheory.Tower` `Mathlib.Geometry.Convex.Cone.Basic` `Mathlib.Geometry.Convex.Cone.DualFinite` `Mathlib.Geometry.Convex.Cone.Dual` `Mathlib.Geometry.Convex.Cone.Face.Basic` `Mathlib.Geometry.Convex.Cone.Pointed` `Mathlib.Geometry.Convex.Cone.Simplicial` `Mathlib.Geometry.Convex.ConvexSpace.AffineSpace` `Mathlib.Geometry.Convex.ConvexSpace.Module` `Mathlib.GroupTheory.CosetCover` `Mathlib.GroupTheory.Coxeter.Basic` `Mathlib.GroupTheory.Coxeter.Matrix` `Mathlib.GroupTheory.DivisibleHull` `Mathlib.GroupTheory.FreeGroup.GeneratorEquiv` `Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization` `Mathlib.LinearAlgebra.AffineSpace.AffineEquiv` `Mathlib.LinearAlgebra.AffineSpace.AffineMap` `Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic` `Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift` `Mathlib.LinearAlgebra.AffineSpace.Basis` `Mathlib.LinearAlgebra.AffineSpace.Centroid` `Mathlib.LinearAlgebra.AffineSpace.Ceva` `Mathlib.LinearAlgebra.AffineSpace.Combination` `Mathlib.LinearAlgebra.AffineSpace.Independent` `Mathlib.LinearAlgebra.AffineSpace.Midpoint` `Mathlib.LinearAlgebra.AffineSpace.Pointwise` `Mathlib.LinearAlgebra.AffineSpace.Restrict` `Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic` `Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid` `Mathlib.LinearAlgebra.AffineSpace.Slope` `Mathlib.LinearAlgebra.Alternating.Basic` `Mathlib.LinearAlgebra.Alternating.Curry` `Mathlib.LinearAlgebra.Alternating.DomCoprod` `Mathlib.LinearAlgebra.Basis.Basic` `Mathlib.LinearAlgebra.Basis.Cardinality` `Mathlib.LinearAlgebra.Basis.Exact` `Mathlib.LinearAlgebra.Basis.Fin` `Mathlib.LinearAlgebra.Basis.Flag` `Mathlib.LinearAlgebra.Basis.MulOpposite` `Mathlib.LinearAlgebra.Basis.Prod` `Mathlib.LinearAlgebra.Basis.SMul` `Mathlib.LinearAlgebra.Basis.Submodule` `Mathlib.LinearAlgebra.Basis.VectorSpace` `Mathlib.LinearAlgebra.BilinearForm.Basic` `Mathlib.LinearAlgebra.BilinearForm.Hom` `Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv` `Mathlib.LinearAlgebra.ConvexSpace.AffineSpace` `Mathlib.LinearAlgebra.Countable` `Mathlib.LinearAlgebra.DFinsupp` `Mathlib.LinearAlgebra.Dimension.Basic` `Mathlib.LinearAlgebra.Dimension.Constructions` `Mathlib.LinearAlgebra.Dimension.DivisionRing` `Mathlib.LinearAlgebra.Dimension.ErdosKaplansky` `Mathlib.LinearAlgebra.Dimension.Finite` `Mathlib.LinearAlgebra.Dimension.Finrank` `Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition` `Mathlib.LinearAlgebra.Dimension.Free` `Mathlib.LinearAlgebra.Dimension.LinearMap` `Mathlib.LinearAlgebra.Dimension.Localization` `Mathlib.LinearAlgebra.Dimension.OrzechProperty` `Mathlib.LinearAlgebra.Dimension.RankNullity` `Mathlib.LinearAlgebra.Dimension.StrongRankCondition` `Mathlib.LinearAlgebra.Dimension.Subsingleton` `Mathlib.LinearAlgebra.DirectSum.Basis` `Mathlib.LinearAlgebra.DirectSum.Finite` `Mathlib.LinearAlgebra.DirectSum.Finsupp` `Mathlib.LinearAlgebra.DirectSum.TensorProduct` `Mathlib.LinearAlgebra.Eigenspace.Basic` `Mathlib.LinearAlgebra.Eigenspace.ContinuousLinearMap` `Mathlib.LinearAlgebra.Eigenspace.Matrix` `Mathlib.LinearAlgebra.FiniteDimensional.Basic` `Mathlib.LinearAlgebra.FiniteDimensional.Defs` `Mathlib.LinearAlgebra.FiniteDimensional.Lemmas` `Mathlib.LinearAlgebra.Finsupp.Pi` `Mathlib.LinearAlgebra.Finsupp.Span` `Mathlib.LinearAlgebra.Finsupp.VectorSpace` `Mathlib.LinearAlgebra.FreeModule.Basic` `Mathlib.LinearAlgebra.FreeModule.Finite.Basic` `Mathlib.LinearAlgebra.FreeModule.PID` `Mathlib.LinearAlgebra.FreeProduct.Basic` `Mathlib.LinearAlgebra.Goursat` `Mathlib.LinearAlgebra.InvariantBasisNumber` `Mathlib.LinearAlgebra.Isomorphisms` `Mathlib.LinearAlgebra.LeftExact` `Mathlib.LinearAlgebra.LinearIndependent.BaseChange` `Mathlib.LinearAlgebra.LinearIndependent.Lemmas` `Mathlib.LinearAlgebra.LinearPMap` `Mathlib.LinearAlgebra.Matrix.Bilinear` `Mathlib.LinearAlgebra.Matrix.Circulant` `Mathlib.LinearAlgebra.Matrix.ConjTranspose` `Mathlib.LinearAlgebra.Matrix.Diagonal` `Mathlib.LinearAlgebra.Matrix.DotProduct` `Mathlib.LinearAlgebra.Matrix.DualNumber` `Mathlib.LinearAlgebra.Matrix.Dual` `Mathlib.LinearAlgebra.Matrix.Hadamard` `Mathlib.LinearAlgebra.Matrix.Ideal` `Mathlib.LinearAlgebra.Matrix.Integer` `Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber` `Mathlib.LinearAlgebra.Matrix.Invertible` `Mathlib.LinearAlgebra.Matrix.Module` `Mathlib.LinearAlgebra.Matrix.Notation` `Mathlib.LinearAlgebra.Matrix.Permanent` `Mathlib.LinearAlgebra.Matrix.RowCol` `Mathlib.LinearAlgebra.Matrix.SemiringInverse` `Mathlib.LinearAlgebra.Matrix.StdBasis` `Mathlib.LinearAlgebra.Matrix.Symmetric` `Mathlib.LinearAlgebra.Matrix.ToLin` `Mathlib.LinearAlgebra.Matrix.Trace` `Mathlib.LinearAlgebra.Matrix.Unique` `Mathlib.LinearAlgebra.Matrix.WithConv` `Mathlib.LinearAlgebra.Multilinear.Basic` `Mathlib.LinearAlgebra.Multilinear.Basis` `Mathlib.LinearAlgebra.Multilinear.Curry` `Mathlib.LinearAlgebra.Multilinear.DFinsupp` `Mathlib.LinearAlgebra.Multilinear.DirectSum` `Mathlib.LinearAlgebra.Multilinear.Finsupp` `Mathlib.LinearAlgebra.Multilinear.Pi` `Mathlib.LinearAlgebra.Multilinear.TensorProduct` `Mathlib.LinearAlgebra.PiTensorProduct.Basic` `Mathlib.LinearAlgebra.PiTensorProduct.Basis` `Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp` `Mathlib.LinearAlgebra.PiTensorProduct.DirectSum` `Mathlib.LinearAlgebra.PiTensorProduct.Dual` `Mathlib.LinearAlgebra.PiTensorProduct.Finite` `Mathlib.LinearAlgebra.PiTensorProduct.Finsupp` `Mathlib.LinearAlgebra.PiTensorProduct.Generators` `Mathlib.LinearAlgebra.PiTensorProduct` `Mathlib.LinearAlgebra.Pi` `Mathlib.LinearAlgebra.Prod` `Mathlib.LinearAlgebra.Projection` `Mathlib.LinearAlgebra.Projectivization.Basic` `Mathlib.LinearAlgebra.Projectivization.Cardinality` `Mathlib.LinearAlgebra.Projectivization.Collinear` `Mathlib.LinearAlgebra.Projectivization.Independence` `Mathlib.LinearAlgebra.Projectivization.Subspace` `Mathlib.LinearAlgebra.Quotient.Basic` `Mathlib.LinearAlgebra.Quotient.Bilinear` `Mathlib.LinearAlgebra.Quotient.Pi` `Mathlib.LinearAlgebra.Ray` `Mathlib.LinearAlgebra.SModEq.Basic` `Mathlib.LinearAlgebra.SModEq.Pointwise` `Mathlib.LinearAlgebra.SesquilinearForm.Basic` `Mathlib.LinearAlgebra.SesquilinearForm.Orthogonal` `Mathlib.LinearAlgebra.Span.Basic` `Mathlib.LinearAlgebra.StdBasis` `Mathlib.LinearAlgebra.SymmetricAlgebra.Basic` `Mathlib.LinearAlgebra.TensorAlgebra.Basic` `Mathlib.LinearAlgebra.TensorAlgebra.Grading` `Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower` `Mathlib.LinearAlgebra.TensorPower.Basic` `Mathlib.LinearAlgebra.TensorPower.Pairing` `Mathlib.LinearAlgebra.TensorPower.Symmetric` `Mathlib.LinearAlgebra.TensorProduct.Associator` `Mathlib.LinearAlgebra.TensorProduct.Basic` `Mathlib.LinearAlgebra.TensorProduct.Basis` `Mathlib.LinearAlgebra.TensorProduct.Decomposition` `Mathlib.LinearAlgebra.TensorProduct.Defs` `Mathlib.LinearAlgebra.TensorProduct.DirectLimit` `Mathlib.LinearAlgebra.TensorProduct.Finiteness` `Mathlib.LinearAlgebra.TensorProduct.Free` `Mathlib.LinearAlgebra.TensorProduct.Map` `Mathlib.LinearAlgebra.TensorProduct.Opposite` `Mathlib.LinearAlgebra.TensorProduct.Pi` `Mathlib.LinearAlgebra.TensorProduct.Prod` `Mathlib.LinearAlgebra.TensorProduct.Quotient` `Mathlib.LinearAlgebra.TensorProduct.RightExactness` `Mathlib.LinearAlgebra.TensorProduct.Subalgebra` `Mathlib.LinearAlgebra.TensorProduct.Submodule` `Mathlib.LinearAlgebra.TensorProduct.Tower` `Mathlib.LinearAlgebra.TensorProduct.Vanishing` `Mathlib.MeasureTheory.Constructions.BorelSpace.Basic` `Mathlib.MeasureTheory.Constructions.BorelSpace.Metric` `Mathlib.MeasureTheory.Constructions.BorelSpace.Order` `Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop` `Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders` `Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent` `Mathlib.MeasureTheory.Constructions.Projective` `Mathlib.MeasureTheory.Covering.VitaliFamily` `Mathlib.MeasureTheory.Covering.Vitali` `Mathlib.MeasureTheory.Function.AEMeasurableOrder` `Mathlib.MeasureTheory.Function.AEMeasurableSequence` `Mathlib.MeasureTheory.Function.Floor` `Mathlib.MeasureTheory.Function.SimpleFunc` `Mathlib.MeasureTheory.Group.AEStabilizer` `Mathlib.MeasureTheory.Group.Action` `Mathlib.MeasureTheory.Group.Arithmetic` `Mathlib.MeasureTheory.Group.Defs` `Mathlib.MeasureTheory.Group.FoelnerFilter` `Mathlib.MeasureTheory.Group.MeasurableEquiv` `Mathlib.MeasureTheory.Group.Pointwise` `Mathlib.MeasureTheory.Integral.Lebesgue.Basic` `Mathlib.MeasureTheory.Integral.Lebesgue.Norm` `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.Dirac` `Mathlib.MeasureTheory.Measure.Doubling` `Mathlib.MeasureTheory.Measure.Map` `Mathlib.MeasureTheory.Measure.MeasureSpaceDef` `Mathlib.MeasureTheory.Measure.MeasureSpace` `Mathlib.MeasureTheory.Measure.MeasuredSets` `Mathlib.MeasureTheory.Measure.MutuallySingular` `Mathlib.MeasureTheory.Measure.NullMeasurable` `Mathlib.MeasureTheory.Measure.OpenPos` `Mathlib.MeasureTheory.Measure.PreVariation` `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.Support` `Mathlib.MeasureTheory.Measure.Trim` `Mathlib.MeasureTheory.Measure.Typeclasses.Finite` `Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass` `Mathlib.MeasureTheory.Measure.Typeclasses.Probability` `Mathlib.MeasureTheory.Measure.Typeclasses.SFinite` `Mathlib.MeasureTheory.Measure.WithDensityFinite` `Mathlib.MeasureTheory.Order.Group.Lattice` `Mathlib.MeasureTheory.Order.Lattice` `Mathlib.MeasureTheory.OuterMeasure.Caratheodory` `Mathlib.MeasureTheory.OuterMeasure.Induced` `Mathlib.MeasureTheory.OuterMeasure.OfAddContent` `Mathlib.MeasureTheory.OuterMeasure.OfFunction` `Mathlib.MeasureTheory.Topology` `Mathlib.MeasureTheory.VectorMeasure.Basic` `Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn` `Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub` `Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan` `Mathlib.MeasureTheory.VectorMeasure.Variation.Basic` `Mathlib.MeasureTheory.VectorMeasure.Variation.Defs` `Mathlib.MeasureTheory.VectorMeasure.Variation.SignedMeasure` `Mathlib.ModelTheory.Arithmetic.Presburger.Definability` `Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic` `Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs` `Mathlib.NumberTheory.Basic` `Mathlib.NumberTheory.FLT.Basic` `Mathlib.NumberTheory.Padics.Measure.Basic` `Mathlib.NumberTheory.Padics.Measure.Topology` `Mathlib.NumberTheory.Zsqrtd.Basic` `Mathlib.NumberTheory.Zsqrtd.ToReal` `Mathlib.Order.Filter.ZeroAndBoundedAtFilter` `Mathlib.Probability.ConditionalProbability` `Mathlib.Probability.ProbabilityMassFunction.Basic` `Mathlib.Probability.ProbabilityMassFunction.Monad` `Mathlib.RingTheory.AdicCompletion.Basic` `Mathlib.RingTheory.AdicCompletion.Topology` `Mathlib.RingTheory.Adjoin.Basic` `Mathlib.RingTheory.Adjoin.Dimension` `Mathlib.RingTheory.AlgebraTower` `Mathlib.RingTheory.AlgebraicIndependent.Defs` `Mathlib.RingTheory.Artinian.Module` `Mathlib.RingTheory.Artinian.Ring` `Mathlib.RingTheory.Bezout` `Mathlib.RingTheory.Bialgebra.Basic` `Mathlib.RingTheory.Bialgebra.Convolution` `Mathlib.RingTheory.Bialgebra.Equiv` `Mathlib.RingTheory.Bialgebra.Hom` `Mathlib.RingTheory.Bialgebra.Quotient` `Mathlib.RingTheory.Bialgebra.SymmetricAlgebra` `Mathlib.RingTheory.Bialgebra.TensorProduct` `Mathlib.RingTheory.Coalgebra.Basic` `Mathlib.RingTheory.Coalgebra.CoassocSimps` `Mathlib.RingTheory.Coalgebra.Convolution` `Mathlib.RingTheory.Coalgebra.Equiv` `Mathlib.RingTheory.Coalgebra.Hom` `Mathlib.RingTheory.Coalgebra.MulOpposite` `Mathlib.RingTheory.Coalgebra.Quotient` `Mathlib.RingTheory.Coalgebra.TensorProduct` `Mathlib.RingTheory.Congruence.Hom` `Mathlib.RingTheory.Coprime.Basic` `Mathlib.RingTheory.Coprime.Ideal` `Mathlib.RingTheory.Coprime.Lemmas` `Mathlib.RingTheory.DualNumber` `Mathlib.RingTheory.EuclideanDomain` `Mathlib.RingTheory.FiniteLength` `Mathlib.RingTheory.Finiteness.Basic` `Mathlib.RingTheory.Finiteness.Bilinear` `Mathlib.RingTheory.Finiteness.Cardinality` `Mathlib.RingTheory.Finiteness.Cofinite` `Mathlib.RingTheory.Finiteness.Defs` `Mathlib.RingTheory.Finiteness.Finsupp` `Mathlib.RingTheory.Finiteness.Ideal` `Mathlib.RingTheory.Finiteness.Lattice` `Mathlib.RingTheory.Finiteness.Nakayama` `Mathlib.RingTheory.Finiteness.NilpotentKer` `Mathlib.RingTheory.Finiteness.Nilpotent` `Mathlib.RingTheory.Finiteness.Prod` `Mathlib.RingTheory.Finiteness.Projective` `Mathlib.RingTheory.Finiteness.Subalgebra` `Mathlib.RingTheory.GradedAlgebra.AlgHom` `Mathlib.RingTheory.GradedAlgebra.Basic` `Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal` `Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps` `Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule` `Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring` `Mathlib.RingTheory.GradedAlgebra.Noetherian` `Mathlib.RingTheory.GradedAlgebra.Radical` `Mathlib.RingTheory.GradedAlgebra.RingHom` `Mathlib.RingTheory.GradedAlgebra.TensorProduct` `Mathlib.RingTheory.HahnSeries.Cardinal` `Mathlib.RingTheory.HahnSeries.Lex` `Mathlib.RingTheory.HahnSeries.Multiplication` `Mathlib.RingTheory.HahnSeries.Summable` `Mathlib.RingTheory.HahnSeries.Valuation` `Mathlib.RingTheory.HopfAlgebra.Basic` `Mathlib.RingTheory.HopfAlgebra.Convolution` `Mathlib.RingTheory.HopfAlgebra.Quotient` `Mathlib.RingTheory.HopfAlgebra.TensorProduct` `Mathlib.RingTheory.Ideal.AssociatedPrime.Basic` `Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness` `Mathlib.RingTheory.Ideal.Basic` `Mathlib.RingTheory.Ideal.Basis` `Mathlib.RingTheory.Ideal.Colon` `Mathlib.RingTheory.Ideal.Finsupp` `Mathlib.RingTheory.Ideal.IdempotentFG` `Mathlib.RingTheory.Ideal.IsAugmentation` `Mathlib.RingTheory.Ideal.IsPrimary` `Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient` `Mathlib.RingTheory.Ideal.IsPrincipal` `Mathlib.RingTheory.Ideal.Maps` `Mathlib.RingTheory.Ideal.Maximal` `Mathlib.RingTheory.Ideal.MinimalPrime.Basic` `Mathlib.RingTheory.Ideal.MinimalPrime.Colon` `Mathlib.RingTheory.Ideal.MinimalPrime.Localization` `Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian` `Mathlib.RingTheory.Ideal.Nonunits` `Mathlib.RingTheory.Ideal.Oka` `Mathlib.RingTheory.Ideal.Operations` `Mathlib.RingTheory.Ideal.Over` `Mathlib.RingTheory.Ideal.Pointwise` `Mathlib.RingTheory.Ideal.Prime` `Mathlib.RingTheory.Ideal.Prod` `Mathlib.RingTheory.Ideal.Quotient.Basic` `Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder` `Mathlib.RingTheory.Ideal.Quotient.Index` `Mathlib.RingTheory.Ideal.Quotient.Nilpotent` `Mathlib.RingTheory.Ideal.Quotient.Noetherian` `Mathlib.RingTheory.Ideal.Quotient.Operations` `Mathlib.RingTheory.Ideal.Quotient.Over` `Mathlib.RingTheory.Ideal.Quotient.PowTransition` `Mathlib.RingTheory.Ideal.Span` `Mathlib.RingTheory.IdealFilter.Basic` `Mathlib.RingTheory.IdealFilter.Topology` `Mathlib.RingTheory.Idempotents` `Mathlib.RingTheory.IntegralClosure.Algebra.Defs` `Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs` `Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs` `Mathlib.RingTheory.IsGaloisGroup.Defs` `Mathlib.RingTheory.IsPrimary` `Mathlib.RingTheory.IsTensorProduct` `Mathlib.RingTheory.Jacobson.Ideal` `Mathlib.RingTheory.Jacobson.Radical` `Mathlib.RingTheory.Jacobson.Semiprimary` `Mathlib.RingTheory.KrullDimension.Basic` `Mathlib.RingTheory.KrullDimension.Field` `Mathlib.RingTheory.Lasker` `Mathlib.RingTheory.Length` `Mathlib.RingTheory.LocalProperties.Submodule` `Mathlib.RingTheory.LocalRing.Basic` `Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic` `Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs` `Mathlib.RingTheory.LocalRing.MaximalIdeal.Square` `Mathlib.RingTheory.LocalRing.NonLocalRing` `Mathlib.RingTheory.LocalRing.ResidueField.Defs` `Mathlib.RingTheory.Localization.AsSubring` `Mathlib.RingTheory.Localization.AtPrime.Basic` `Mathlib.RingTheory.Localization.Away.Basic` `Mathlib.RingTheory.Localization.BaseChange` `Mathlib.RingTheory.Localization.Basic` `Mathlib.RingTheory.Localization.Cardinality` `Mathlib.RingTheory.Localization.Defs` `Mathlib.RingTheory.Localization.FractionRing` `Mathlib.RingTheory.Localization.Ideal` `Mathlib.RingTheory.Localization.Integer` `Mathlib.RingTheory.Localization.LocalizationLocalization` `Mathlib.RingTheory.Localization.Module` `Mathlib.RingTheory.Localization.NumDen` `Mathlib.RingTheory.Morita.Basic` `Mathlib.RingTheory.Morita.Matrix` `Mathlib.RingTheory.MvPolynomial.Symmetric.Defs` `Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem` `Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities` `Mathlib.RingTheory.MvPolynomial.Tower` `Mathlib.RingTheory.MvPowerSeries.Basic` `Mathlib.RingTheory.MvPowerSeries.Evaluation` `Mathlib.RingTheory.MvPowerSeries.GaussNorm` `Mathlib.RingTheory.MvPowerSeries.Inverse` `Mathlib.RingTheory.MvPowerSeries.LexOrder` `Mathlib.RingTheory.MvPowerSeries.LinearTopology` `Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors` `Mathlib.RingTheory.MvPowerSeries.Order` `Mathlib.RingTheory.MvPowerSeries.PiTopology` `Mathlib.RingTheory.MvPowerSeries.Rename` `Mathlib.RingTheory.MvPowerSeries.Restricted` `Mathlib.RingTheory.MvPowerSeries.Substitution` `Mathlib.RingTheory.MvPowerSeries.Trunc` `Mathlib.RingTheory.Nakayama` `Mathlib.RingTheory.Nilpotent.Basic` `Mathlib.RingTheory.Nilpotent.Exp` `Mathlib.RingTheory.Nilpotent.Lemmas` `Mathlib.RingTheory.Noetherian.Basic` `Mathlib.RingTheory.Noetherian.Defs` `Mathlib.RingTheory.Noetherian.Filter` `Mathlib.RingTheory.Noetherian.Nilpotent` `Mathlib.RingTheory.Noetherian.OfPrime` `Mathlib.RingTheory.Noetherian.Orzech` `Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain` `Mathlib.RingTheory.OrzechProperty` `Mathlib.RingTheory.PiTensorProduct` `Mathlib.RingTheory.PrincipalIdealDomainOfPrime` `Mathlib.RingTheory.PrincipalIdealDomain` `Mathlib.RingTheory.QuotSMulTop` `Mathlib.RingTheory.Radical.Basic` `Mathlib.RingTheory.Regular.Category` `Mathlib.RingTheory.SimpleModule.Basic` `Mathlib.RingTheory.SimpleModule.InjectiveProjective` `Mathlib.RingTheory.SimpleModule.Isotypic` `Mathlib.RingTheory.SimpleModule.Rank` `Mathlib.RingTheory.SimpleModule.WedderburnArtin` `Mathlib.RingTheory.SimpleRing.DivisionRing` `Mathlib.RingTheory.SimpleRing.Matrix` `Mathlib.RingTheory.SimpleRing.Principal` `Mathlib.RingTheory.Spectrum.Maximal.Basic` `Mathlib.RingTheory.Spectrum.Maximal.Defs` `Mathlib.RingTheory.Spectrum.Prime.Basic` `Mathlib.RingTheory.Spectrum.Prime.Defs` `Mathlib.RingTheory.SurjectiveOnStalks` `Mathlib.RingTheory.TensorProduct.Basic` `Mathlib.RingTheory.TensorProduct.Finite` `Mathlib.RingTheory.TensorProduct.Free` `Mathlib.RingTheory.TensorProduct.IsBaseChangeFree` `Mathlib.RingTheory.TensorProduct.IsBaseChangePi` `Mathlib.RingTheory.TensorProduct.IsBaseChangeRightExact` `Mathlib.RingTheory.TensorProduct.Maps` `Mathlib.RingTheory.TensorProduct.MonoidAlgebra` `Mathlib.RingTheory.TensorProduct.Pi` `Mathlib.RingTheory.TensorProduct.Quotient` `Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet` `Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp` `Mathlib.RingTheory.UniqueFactorizationDomain.GCDMonoid` `Mathlib.RingTheory.UniqueFactorizationDomain.Ideal` `Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky` `Mathlib.RingTheory.UniqueFactorizationDomain.Localization` `Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity` `Mathlib.RingTheory.Valuation.Basic` `Mathlib.RingTheory.Valuation.ExtendToLocalization` `Mathlib.RingTheory.Valuation.Integers` `Mathlib.RingTheory.Valuation.PrimeMultiplicity` `Mathlib.RingTheory.Valuation.Quotient` `Mathlib.RingTheory.Valuation.ValuationRing` `Mathlib.RingTheory.Valuation.ValuativeRel.Basic` `Mathlib.RingTheory.Valuation.ValuativeRel.Trivial` `Mathlib.Tactic.Algebraize` `Mathlib.Tactic.ComputeAsymptotics.Lemmas` `Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion` `Mathlib.Tactic.Module` `Mathlib.Tactic.NormNum.IsCoprime` `Mathlib.Topology.Algebra.AffineSubspace` `Mathlib.Topology.Algebra.Affine` `Mathlib.Topology.Algebra.Algebra.Equiv` `Mathlib.Topology.Algebra.Algebra` `Mathlib.Topology.Algebra.ContinuousAffineEquiv` `Mathlib.Topology.Algebra.ContinuousAffineMap` `Mathlib.Topology.Algebra.FilterBasis` `Mathlib.Topology.Algebra.Group.CompactOpen` `Mathlib.Topology.Algebra.Group.Extension` `Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution` `Mathlib.Topology.Algebra.InfiniteSum.Field` `Mathlib.Topology.Algebra.InfiniteSum.Module` `Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean` `Mathlib.Topology.Algebra.IsOpenUnits` `Mathlib.Topology.Algebra.LinearMapCompletion` `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.ClosedSubmodule` `Mathlib.Topology.Algebra.Module.Compact` `Mathlib.Topology.Algebra.Module.Complement` `Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic` `Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent` `Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd` `Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient` `Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars` `Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict` `Mathlib.Topology.Algebra.Module.Equiv` `Mathlib.Topology.Algebra.Module.IsWeak` `Mathlib.Topology.Algebra.Module.LinearMapPiProd` `Mathlib.Topology.Algebra.Module.LinearMap` `Mathlib.Topology.Algebra.Module.LinearPMap` `Mathlib.Topology.Algebra.Module.LocallyConvex` `Mathlib.Topology.Algebra.Module.ModuleTopology` `Mathlib.Topology.Algebra.Module.Multilinear.Basic` `Mathlib.Topology.Algebra.Module.Multilinear.Bounded` `Mathlib.Topology.Algebra.Module.Multilinear.Topology` `Mathlib.Topology.Algebra.Module.PerfectPairing` `Mathlib.Topology.Algebra.Module.Simple` `Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace` `Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM` `Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap` `Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM` `Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM` `Mathlib.Topology.Algebra.Module.Spaces.WeakBilin` `Mathlib.Topology.Algebra.Module.Spaces.WeakDual` `Mathlib.Topology.Algebra.Module.Star` `Mathlib.Topology.Algebra.Module.StrongTopology` `Mathlib.Topology.Algebra.Module.TransferInstance` `Mathlib.Topology.Algebra.Module.UniformConvergence` `Mathlib.Topology.Algebra.Module.WeakDual` `Mathlib.Topology.Algebra.Monoid.FunOnFinite` `Mathlib.Topology.Algebra.MvPolynomial` `Mathlib.Topology.Algebra.NonUnitalAlgebra` `Mathlib.Topology.Algebra.NonUnitalStarAlgebra` `Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology` `Mathlib.Topology.Algebra.Nonarchimedean.Bases` `Mathlib.Topology.Algebra.Nonarchimedean.Completion` `Mathlib.Topology.Algebra.SeparationQuotient.Basic` `Mathlib.Topology.Algebra.SeparationQuotient.FiniteDimensional` `Mathlib.Topology.Algebra.SeparationQuotient.Hom` `Mathlib.Topology.Algebra.SeparationQuotient.Section` `Mathlib.Topology.Algebra.Star.LinearMap` `Mathlib.Topology.Algebra.Star.Unitary` `Mathlib.Topology.Algebra.StarSubalgebra` `Mathlib.Topology.Algebra.TopologicallyNilpotent` `Mathlib.Topology.Algebra.UniformField` `Mathlib.Topology.Algebra.UniformFilterBasis` `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.CWComplex.Classical.Graph` `Mathlib.Topology.CWComplex.Classical.Subcomplex` `Mathlib.Topology.Category.DeltaGenerated` `Mathlib.Topology.Compactness.DeltaGeneratedSpace` `Mathlib.Topology.ContinuousMap.Algebra` `Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli` `Mathlib.Topology.ContinuousMap.Bounded.Basic` `Mathlib.Topology.ContinuousMap.Bounded.Normed` `Mathlib.Topology.ContinuousMap.Bounded.Star` `Mathlib.Topology.ContinuousMap.BoundedCompactlySupported` `Mathlib.Topology.ContinuousMap.Compact` `Mathlib.Topology.ContinuousMap.CompactlySupported` `Mathlib.Topology.ContinuousMap.ContinuousMapZero` `Mathlib.Topology.ContinuousMap.Lattice` `Mathlib.Topology.ContinuousMap.LocallyConstant` `Mathlib.Topology.ContinuousMap.LocallyConvex` `Mathlib.Topology.ContinuousMap.StarOrdered` `Mathlib.Topology.ContinuousMap.Star` `Mathlib.Topology.ContinuousMap.ZeroAtInfty` `Mathlib.Topology.Homotopy.Affine` `Mathlib.Topology.Homotopy.Contractible` `Mathlib.Topology.Homotopy.HomotopyGroup` `Mathlib.Topology.Homotopy.Lifting` `Mathlib.Topology.Homotopy.LocallyContractible` `Mathlib.Topology.Homotopy.Path` `Mathlib.Topology.Homotopy.Product` `Mathlib.Topology.Homotopy.TopCat.ToSSet` `Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy` `Mathlib.Topology.Instances.RealVectorSpace` `Mathlib.Topology.Instances.TrivSqZeroExt` `Mathlib.Topology.LocallyConstant.Algebra` `Mathlib.Topology.Maps.Strict.Module` `Mathlib.Topology.MetricSpace.Algebra` `Mathlib.Topology.MetricSpace.CantorScheme` `Mathlib.Topology.MetricSpace.CauSeqFilter` `Mathlib.Topology.MetricSpace.Closeds` `Mathlib.Topology.MetricSpace.Completion` `Mathlib.Topology.MetricSpace.Contracting` `Mathlib.Topology.MetricSpace.Cover` `Mathlib.Topology.MetricSpace.CoveringNumbers` `Mathlib.Topology.MetricSpace.GromovHausdorffRealized` `Mathlib.Topology.MetricSpace.HausdorffDistance` `Mathlib.Topology.MetricSpace.Perfect` `Mathlib.Topology.MetricSpace.PiNat` `Mathlib.Topology.MetricSpace.Polish` `Mathlib.Topology.MetricSpace.ThickenedIndicator` `Mathlib.Topology.MetricSpace.Thickening` `Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps` `Mathlib.Topology.MetricSpace.UniformConvergence` `Mathlib.Topology.Sheaves.Abelian` `Mathlib.Topology.Sheaves.AddCommGrpCat` `Mathlib.Topology.Sheaves.Flasque` `Mathlib.Topology.Sheaves.MayerVietoris` `Mathlib.Topology.Sheaves.Module` `Mathlib.Topology.Sion` `Mathlib.Topology.Subpath` `Mathlib.Topology.UniformSpace.Dini` `Mathlib.Topology.UniformSpace.ProdApproximation`	2
615 files `Mathlib.Algebra.AddConstMap.Basic` `Mathlib.Algebra.AddConstMap.Equiv` `Mathlib.Algebra.Algebra.Hom.Rat` `Mathlib.Algebra.BigOperators.Balance` `Mathlib.Algebra.BigOperators.Expect` `Mathlib.Algebra.BigOperators.Field` `Mathlib.Algebra.BigOperators.Finprod` `Mathlib.Algebra.BigOperators.GroupWithZero.Action` `Mathlib.Algebra.Category.Grp.Colimits` `Mathlib.Algebra.Category.MonCat.Adjunctions` `Mathlib.Algebra.Colimit.DirectLimit` `Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries` `Mathlib.Algebra.ContinuedFractions.Computation.Approximations` `Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating` `Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat` `Mathlib.Algebra.ContinuedFractions.Computation.Translations` `Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv` `Mathlib.Algebra.ContinuedFractions.Determinant` `Mathlib.Algebra.DirectSum.AddChar` `Mathlib.Algebra.DirectSum.Basic` `Mathlib.Algebra.DirectSum.Ring` `Mathlib.Algebra.Field.GeomSum` `Mathlib.Algebra.Group.Pointwise.Finset.Density` `Mathlib.Algebra.Homology.AlternatingConst` `Mathlib.Algebra.Homology.CochainComplexOpposite` `Mathlib.Algebra.Homology.Embedding.AreComplementary` `Mathlib.Algebra.Homology.Embedding.Connect` `Mathlib.Algebra.Homology.Embedding.ExtendHomology` `Mathlib.Algebra.Homology.Embedding.ExtendHomotopy` `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.Functor` `Mathlib.Algebra.Homology.HomologicalComplexLimitsEventuallyConstant` `Mathlib.Algebra.Homology.HomologySequenceLemmas` `Mathlib.Algebra.Homology.HomologySequence` `Mathlib.Algebra.Homology.HomotopyCategory` `Mathlib.Algebra.Homology.HomotopyCofiber` `Mathlib.Algebra.Homology.HomotopyFiber` `Mathlib.Algebra.Homology.Homotopy` `Mathlib.Algebra.Homology.LeftResolution.Basic` `Mathlib.Algebra.Homology.LeftResolution.Reduced` `Mathlib.Algebra.Homology.LeftResolution.Transport` `Mathlib.Algebra.Homology.Localization` `Mathlib.Algebra.Homology.Opposite` `Mathlib.Algebra.Homology.Precylinder` `Mathlib.Algebra.Homology.QuasiIso` `Mathlib.Algebra.Homology.Refinements` `Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex` `Mathlib.Algebra.Homology.SingleHomology` `Mathlib.Algebra.Homology.SpectralObject.FirstPage` `Mathlib.Algebra.Homology.SpectralObject.SpectralSequence` `Mathlib.Algebra.Homology.SpectralSequence.Basic` `Mathlib.Algebra.Module.BigOperators` `Mathlib.Algebra.Module.Submodule.Finsupp` `Mathlib.Algebra.MonoidAlgebra.Cardinal` `Mathlib.Algebra.MonoidAlgebra.Defs` `Mathlib.Algebra.MonoidAlgebra.Division` `Mathlib.Algebra.MonoidAlgebra.Lift` `Mathlib.Algebra.MonoidAlgebra.MapDomain` `Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors` `Mathlib.Algebra.MonoidAlgebra.Opposite` `Mathlib.Algebra.MonoidAlgebra.PointwiseSMul` `Mathlib.Algebra.Order.Antidiag.FinsuppEquiv` `Mathlib.Algebra.Order.Archimedean.Basic` `Mathlib.Algebra.Order.Archimedean.Class` `Mathlib.Algebra.Order.Archimedean.Hom` `Mathlib.Algebra.Order.Archimedean.IndicatorCard` `Mathlib.Algebra.Order.Archimedean.Real.Basic` `Mathlib.Algebra.Order.Archimedean.Real.Hom` `Mathlib.Algebra.Order.Archimedean.Submonoid` `Mathlib.Algebra.Order.BigOperators.Expect` `Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset` `Mathlib.Algebra.Order.BigOperators.Ring.Finset` `Mathlib.Algebra.Order.CauSeq.BigOperators` `Mathlib.Algebra.Order.CompleteField` `Mathlib.Algebra.Order.Field.GeomSum` `Mathlib.Algebra.Order.Floor.Extended` `Mathlib.Algebra.Order.Floor.Ring` `Mathlib.Algebra.Order.Floor.Semifield` `Mathlib.Algebra.Order.Module.Archimedean` `Mathlib.Algebra.Order.Ring.IsNonarchimedean` `Mathlib.Algebra.Order.Round` `Mathlib.Algebra.Order.Star.Conjneg` `Mathlib.Algebra.Order.Star.Real` `Mathlib.Algebra.Quandle` `Mathlib.Algebra.Star.BigOperators` `Mathlib.AlgebraicTopology.AlternatingFaceMapComplex` `Mathlib.AlgebraicTopology.CechNerve` `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.EilenbergSteenrod` `Mathlib.AlgebraicTopology.ExtraDegeneracy` `Mathlib.AlgebraicTopology.MooreComplex` `Mathlib.AlgebraicTopology.Quasicategory.Basic` `Mathlib.AlgebraicTopology.Quasicategory.InnerFibration` `Mathlib.AlgebraicTopology.Quasicategory.Nerve` `Mathlib.AlgebraicTopology.Quasicategory.StrictBicategory` `Mathlib.AlgebraicTopology.Quasicategory.StrictSegal` `Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated` `Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic` `Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal` `Mathlib.AlgebraicTopology.SimplexCategory.Basic` `Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter` `Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic` `Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono` `Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms` `Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty` `Mathlib.AlgebraicTopology.SimplexCategory.Rev` `Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory` `Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne` `Mathlib.AlgebraicTopology.SimplexCategory.Truncated` `Mathlib.AlgebraicTopology.SimplicialCategory.Basic` `Mathlib.AlgebraicTopology.SimplicialCategory.SimplicialObject` `Mathlib.AlgebraicTopology.SimplicialNerve` `Mathlib.AlgebraicTopology.SimplicialObject.Basic` `Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy` `Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal` `Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter` `Mathlib.AlgebraicTopology.SimplicialObject.Homotopy` `Mathlib.AlgebraicTopology.SimplicialObject.II` `Mathlib.AlgebraicTopology.SimplicialObject.Op` `Mathlib.AlgebraicTopology.SimplicialObject.Split` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Op` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex` `Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd` `Mathlib.AlgebraicTopology.SimplicialSet.Basic` `Mathlib.AlgebraicTopology.SimplicialSet.Boundary` `Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations` `Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso` `Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated` `Mathlib.AlgebraicTopology.SimplicialSet.CompStruct` `Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal` `Mathlib.AlgebraicTopology.SimplicialSet.Degenerate` `Mathlib.AlgebraicTopology.SimplicialSet.Dimension` `Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits` `Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd` `Mathlib.AlgebraicTopology.SimplicialSet.Finite` `Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal` `Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic` `Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero` `Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomotopyInvariance` `Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate` `Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat` `Mathlib.AlgebraicTopology.SimplicialSet.Homotopy` `Mathlib.AlgebraicTopology.SimplicialSet.HornColimits` `Mathlib.AlgebraicTopology.SimplicialSet.Horn` `Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct` `Mathlib.AlgebraicTopology.SimplicialSet.KanComplex` `Mathlib.AlgebraicTopology.SimplicialSet.Monoidal` `Mathlib.AlgebraicTopology.SimplicialSet.Monomorphisms` `Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction` `Mathlib.AlgebraicTopology.SimplicialSet.NerveCodiscrete` `Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate` `Mathlib.AlgebraicTopology.SimplicialSet.Nerve` `Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit` `Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex` `Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices` `Mathlib.AlgebraicTopology.SimplicialSet.Nonempty` `Mathlib.AlgebraicTopology.SimplicialSet.NonsingularColimit` `Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular` `Mathlib.AlgebraicTopology.SimplicialSet.Op` `Mathlib.AlgebraicTopology.SimplicialSet.Path` `Mathlib.AlgebraicTopology.SimplicialSet.PiZero` `Mathlib.AlgebraicTopology.SimplicialSet.Presentable` `Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne` `Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex` `Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct` `Mathlib.AlgebraicTopology.SimplicialSet.RegularEpi` `Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism` `Mathlib.AlgebraicTopology.SimplicialSet.Simplices` `Mathlib.AlgebraicTopology.SimplicialSet.Skeleton` `Mathlib.AlgebraicTopology.SimplicialSet.Splitting` `Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne` `Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex` `Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal` `Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits` `Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexEvaluation` `Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexOp` `Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex` `Mathlib.AlgebraicTopology.SimplicialSet.Subdivision` `Mathlib.Analysis.BoxIntegral.Box.Basic` `Mathlib.Analysis.BoxIntegral.Partition.Basic` `Mathlib.Analysis.BoxIntegral.Partition.Split` `Mathlib.Analysis.BoxIntegral.Partition.Tagged` `Mathlib.Analysis.Calculus.TangentCone.Defs` `Mathlib.Analysis.Complex.Norm` `Mathlib.Analysis.Complex.Order` `Mathlib.Analysis.Normed.Group.Basic` `Mathlib.Analysis.Normed.Group.Bounded` `Mathlib.Analysis.Normed.Group.CocompactMap` `Mathlib.Analysis.Normed.Group.Constructions` `Mathlib.Analysis.Normed.Group.Continuity` `Mathlib.Analysis.Normed.Group.Defs` `Mathlib.Analysis.Normed.Group.Indicator` `Mathlib.Analysis.Normed.Group.Int` `Mathlib.Analysis.Normed.Group.Rat` `Mathlib.Analysis.Normed.Group.Real` `Mathlib.Analysis.Normed.Group.Seminorm` `Mathlib.Analysis.Normed.Group.Subgroup` `Mathlib.Analysis.Normed.Group.Submodule` `Mathlib.Analysis.Normed.Module.MStructure` `Mathlib.Analysis.Normed.Order.Basic` `Mathlib.Analysis.Normed.Order.Hom.Basic` `Mathlib.Analysis.Normed.Order.Hom.Ultra` `Mathlib.Analysis.Oscillation` `Mathlib.Analysis.Rat.NatSqrt.Real` `Mathlib.Analysis.Real.Sqrt` `Mathlib.Analysis.Subadditive` `Mathlib.CategoryTheory.Abelian.Injective.Resolution` `Mathlib.CategoryTheory.Abelian.LeftDerived` `Mathlib.CategoryTheory.Abelian.Projective.Resolution` `Mathlib.CategoryTheory.Abelian.RightDerived` `Mathlib.CategoryTheory.Category.Cat.Colimit` `Mathlib.CategoryTheory.Functor.ReflectsIso.Exact` `Mathlib.CategoryTheory.Galois.Equivalence` `Mathlib.CategoryTheory.Galois.EssSurj` `Mathlib.CategoryTheory.Galois.IsFundamentalgroup` `Mathlib.CategoryTheory.Galois.Topology` `Mathlib.CategoryTheory.Idempotents.SimplicialObject` `Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech` `Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy` `Mathlib.CategoryTheory.Monoidal.Tor` `Mathlib.CategoryTheory.Preadditive.Injective.Resolution` `Mathlib.CategoryTheory.Preadditive.Mat` `Mathlib.CategoryTheory.Preadditive.Projective.Resolution` `Mathlib.CategoryTheory.Sites.SheafCohomology.Cech` `Mathlib.Combinatorics.Additive.ApproximateSubgroup` `Mathlib.Combinatorics.Additive.CovBySMul` `Mathlib.Combinatorics.Additive.DoublingConst` `Mathlib.Combinatorics.Additive.Energy` `Mathlib.Combinatorics.Additive.PluenneckeRuzsa` `Mathlib.Combinatorics.Additive.RuzsaCovering` `Mathlib.Combinatorics.Additive.SmallTripling` `Mathlib.Combinatorics.Derangements.Basic` `Mathlib.Combinatorics.Derangements.Finite` `Mathlib.Combinatorics.Enumerative.Bell` `Mathlib.Combinatorics.Enumerative.Catalan.Basic` `Mathlib.Combinatorics.Enumerative.Catalan.Tree` `Mathlib.Combinatorics.Enumerative.Catalan` `Mathlib.Combinatorics.Enumerative.DyckWord` `Mathlib.Combinatorics.Enumerative.IncidenceAlgebra` `Mathlib.Combinatorics.Enumerative.InclusionExclusion` `Mathlib.Combinatorics.Enumerative.Schroder` `Mathlib.Combinatorics.KatonaCircle` `Mathlib.Combinatorics.Pigeonhole` `Mathlib.Combinatorics.SetFamily.AhlswedeZhang` `Mathlib.Combinatorics.SetFamily.FourFunctions` `Mathlib.Combinatorics.SetFamily.LYM` `Mathlib.Combinatorics.SimpleGraph.Density` `Mathlib.Combinatorics.SimpleGraph.IncMatrix` `Mathlib.Combinatorics.SimpleGraph.Regularity.Energy` `Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform` `Mathlib.Combinatorics.SimpleGraph.Triangle.Basic` `Mathlib.Combinatorics.SimpleGraph.Triangle.Counting` `Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite` `Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic` `Mathlib.Computability.DFA` `Mathlib.Computability.EpsilonNFA` `Mathlib.Computability.MyhillNerode` `Mathlib.Computability.NFA` `Mathlib.Data.Complex.Basic` `Mathlib.Data.Complex.BigOperators` `Mathlib.Data.DFinsupp.BigOperators` `Mathlib.Data.DFinsupp.Interval` `Mathlib.Data.DFinsupp.Multiset` `Mathlib.Data.DFinsupp.Small` `Mathlib.Data.DFinsupp.Submonoid` `Mathlib.Data.ENNReal.Action` `Mathlib.Data.ENNReal.Basic` `Mathlib.Data.ENNReal.BigOperators` `Mathlib.Data.ENNReal.Holder` `Mathlib.Data.ENNReal.Inv` `Mathlib.Data.ENNReal.Lemmas` `Mathlib.Data.ENNReal.Operations` `Mathlib.Data.ENNReal.Real` `Mathlib.Data.EReal.Basic` `Mathlib.Data.EReal.Inv` `Mathlib.Data.EReal.Operations` `Mathlib.Data.Finsupp.AList` `Mathlib.Data.Finsupp.Antidiagonal` `Mathlib.Data.Finsupp.Basic` `Mathlib.Data.Finsupp.Encodable` `Mathlib.Data.Finsupp.Interval` `Mathlib.Data.Finsupp.Lex` `Mathlib.Data.Finsupp.MonomialOrder.DegLex` `Mathlib.Data.Finsupp.MonomialOrder` `Mathlib.Data.Finsupp.Multiset` `Mathlib.Data.Finsupp.Option` `Mathlib.Data.Finsupp.Order` `Mathlib.Data.Finsupp.PointwiseSMul` `Mathlib.Data.Finsupp.SMul` `Mathlib.Data.Finsupp.Sigma` `Mathlib.Data.Finsupp.ToDFinsupp` `Mathlib.Data.Finsupp.Weight` `Mathlib.Data.Finsupp.WellFounded` `Mathlib.Data.Int.CardIntervalMod` `Mathlib.Data.Int.Fib.Basic` `Mathlib.Data.Int.Fib.Lemmas` `Mathlib.Data.Int.WithZero` `Mathlib.Data.Matrix.Action` `Mathlib.Data.Matrix.Mul` `Mathlib.Data.Matrix.PEquiv` `Mathlib.Data.Multiset.Interval` `Mathlib.Data.NNRat.BigOperators` `Mathlib.Data.NNRat.Floor` `Mathlib.Data.NNReal.Basic` `Mathlib.Data.NNReal.Defs` `Mathlib.Data.NNReal.Star` `Mathlib.Data.Nat.Choose.Central` `Mathlib.Data.Nat.Choose.Multinomial` `Mathlib.Data.Nat.Choose.Sum` `Mathlib.Data.Nat.Digits.Div` `Mathlib.Data.Nat.Digits.Lemmas` `Mathlib.Data.Nat.Factorial.BigOperators` `Mathlib.Data.Nat.Factorial.DoubleFactorial` `Mathlib.Data.Nat.Factorial.SuperFactorial` `Mathlib.Data.Nat.Fib.Basic` `Mathlib.Data.Nat.Fib.Zeckendorf` `Mathlib.Data.Rat.BigOperators` `Mathlib.Data.Rat.Floor` `Mathlib.Data.Rat.NatSqrt.Real` `Mathlib.Data.Rat.Star` `Mathlib.Data.Real.Archimedean` `Mathlib.Data.Real.Basic` `Mathlib.Data.Real.CompleteField` `Mathlib.Data.Real.ConjExponents` `Mathlib.Data.Real.ENatENNReal` `Mathlib.Data.Real.Embedding` `Mathlib.Data.Real.Hom` `Mathlib.Data.Real.Pointwise` `Mathlib.Data.Real.Sign` `Mathlib.Data.Real.Sqrt` `Mathlib.Data.Real.StarOrdered` `Mathlib.Data.Real.Star` `Mathlib.Data.Set.Card.Arithmetic` `Mathlib.Data.Setoid.Partition.Card` `Mathlib.Dynamics.Flow` `Mathlib.Dynamics.OmegaLimit` `Mathlib.Geometry.Convex.ConvexSpace.AffineMap` `Mathlib.Geometry.Convex.ConvexSpace.Defs` `Mathlib.Geometry.Convex.ConvexSpace.Prod` `Mathlib.Geometry.Convex.Hull` `Mathlib.Geometry.Convex.Set` `Mathlib.Geometry.Convex.Star` `Mathlib.Geometry.Manifold.ChartedSpace` `Mathlib.Geometry.Manifold.HasGroupoid` `Mathlib.Geometry.Manifold.Instances.Quotient` `Mathlib.Geometry.Manifold.LocalInvariantProperties` `Mathlib.Geometry.Manifold.Sheaf.Basic` `Mathlib.Geometry.Manifold.StructureGroupoid` `Mathlib.GroupTheory.Archimedean` `Mathlib.GroupTheory.ClassEquation` `Mathlib.GroupTheory.Congruence.BigOperators` `Mathlib.GroupTheory.Divisible` `Mathlib.GroupTheory.GroupAction.Blocks` `Mathlib.GroupTheory.GroupExtension.Basic` `Mathlib.GroupTheory.Perm.Option` `Mathlib.GroupTheory.Perm.Sign` `Mathlib.InformationTheory.Hamming` `Mathlib.LinearAlgebra.Basis.Bilinear` `Mathlib.LinearAlgebra.Basis.Defs` `Mathlib.LinearAlgebra.ConvexSpace` `Mathlib.LinearAlgebra.Dual.Basis` `Mathlib.LinearAlgebra.Finsupp.Defs` `Mathlib.LinearAlgebra.Finsupp.LSum` `Mathlib.LinearAlgebra.Finsupp.LinearCombination` `Mathlib.LinearAlgebra.Finsupp.SumProd` `Mathlib.LinearAlgebra.Finsupp.Supported` `Mathlib.LinearAlgebra.LinearIndependent.Algebra` `Mathlib.LinearAlgebra.LinearIndependent.Basic` `Mathlib.LinearAlgebra.LinearIndependent.Defs` `Mathlib.LinearAlgebra.Matrix.Action` `Mathlib.LinearAlgebra.Matrix.Irreducible.Defs` `Mathlib.LinearAlgebra.Matrix.Orthogonal` `Mathlib.Logic.Hydra` `Mathlib.MeasureTheory.OuterMeasure.AE` `Mathlib.MeasureTheory.OuterMeasure.Basic` `Mathlib.MeasureTheory.OuterMeasure.BorelCantelli` `Mathlib.MeasureTheory.OuterMeasure.Defs` `Mathlib.MeasureTheory.OuterMeasure.Operations` `Mathlib.ModelTheory.Fraisse` `Mathlib.ModelTheory.Order` `Mathlib.NumberTheory.ADEInequality` `Mathlib.NumberTheory.ClassNumber.AdmissibleAbs` `Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue` `Mathlib.NumberTheory.EllipticDivisibilitySequence` `Mathlib.Order.Filter.AtTopBot.Archimedean` `Mathlib.Order.Filter.AtTopBot.Interval` `Mathlib.Order.Filter.CardinalInter` `Mathlib.Order.Filter.Cocardinal` `Mathlib.Order.Filter.ENNReal` `Mathlib.Order.Filter.TendstoCofinite` `Mathlib.Order.Interval.Finset.Box` `Mathlib.Order.Northcott` `Mathlib.Order.Types.Arithmetic` `Mathlib.RingTheory.Congruence.BigOperators` `Mathlib.RingTheory.HahnSeries.Addition` `Mathlib.RingTheory.Ideal.Lattice` `Mathlib.RingTheory.TwoSidedIdeal.BigOperators` `Mathlib.SetTheory.Cardinal.ENNReal` `Mathlib.SetTheory.Cardinal.Finsupp` `Mathlib.SetTheory.Cardinal.Subfield` `Mathlib.SetTheory.Ordinal.CantorNormalForm` `Mathlib.SetTheory.Ordinal.Notation` `Mathlib.SetTheory.Ordinal.Topology` `Mathlib.Tactic.Algebra.Lemmas` `Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates` `Mathlib.Tactic.NormNum.ModEq` `Mathlib.Tactic.NormNum.NatFib` `Mathlib.Tactic.NormNum.RealSqrt` `Mathlib.Tactic.Rify` `Mathlib.Topology.Algebra.Algebra.Rat` `Mathlib.Topology.Algebra.ClopenNhdofOne` `Mathlib.Topology.Algebra.Equicontinuity` `Mathlib.Topology.Algebra.Field` `Mathlib.Topology.Algebra.Group.AddTorsor` `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.Group.Torsor` `Mathlib.Topology.Algebra.Group.Units` `Mathlib.Topology.Algebra.GroupCompletion` `Mathlib.Topology.Algebra.GroupWithZero` `Mathlib.Topology.Algebra.InfiniteSum.Basic` `Mathlib.Topology.Algebra.InfiniteSum.Constructions` `Mathlib.Topology.Algebra.InfiniteSum.Defs` `Mathlib.Topology.Algebra.InfiniteSum.ENNReal` `Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion` `Mathlib.Topology.Algebra.InfiniteSum.Group` `Mathlib.Topology.Algebra.InfiniteSum.NatInt` `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.Constructions` `Mathlib.Topology.Algebra.IsUniformGroup.Defs` `Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup` `Mathlib.Topology.Algebra.IsUniformGroup.Order` `Mathlib.Topology.Algebra.LinearTopology` `Mathlib.Topology.Algebra.MetricSpace.Lipschitz` `Mathlib.Topology.Algebra.Monoid` `Mathlib.Topology.Algebra.Nonarchimedean.Basic` `Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected` `Mathlib.Topology.Algebra.OpenSubgroup` `Mathlib.Topology.Algebra.Order.Archimedean` `Mathlib.Topology.Algebra.Order.Field` `Mathlib.Topology.Algebra.Order.Floor` `Mathlib.Topology.Algebra.Order.Group` `Mathlib.Topology.Algebra.Order.LiminfLimsup` `Mathlib.Topology.Algebra.Order.UpperLower` `Mathlib.Topology.Algebra.ProperAction.AddTorsor` `Mathlib.Topology.Algebra.ProperAction.Basic` `Mathlib.Topology.Algebra.ProperAction.Torsor` `Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace` `Mathlib.Topology.Algebra.Ring.Basic` `Mathlib.Topology.Algebra.Ring.Ideal` `Mathlib.Topology.Algebra.Ring.Real` `Mathlib.Topology.Algebra.Star.Real` `Mathlib.Topology.Algebra.UniformConvergence` `Mathlib.Topology.Algebra.UniformMulAction` `Mathlib.Topology.Algebra.WithZeroTopology` `Mathlib.Topology.ApproximateUnit` `Mathlib.Topology.Bornology.Real` `Mathlib.Topology.Category.Sequential` `Mathlib.Topology.Category.TopCat.Monoidal` `Mathlib.Topology.Category.TopCommRingCat` `Mathlib.Topology.Category.TopPair` `Mathlib.Topology.Connected.CardComponents` `Mathlib.Topology.Connected.LocPathConnected` `Mathlib.Topology.Connected.LocallyPathConnected` `Mathlib.Topology.Connected.PathComponentOne` `Mathlib.Topology.Connected.PathConnected` `Mathlib.Topology.ContinuousMap.Interval` `Mathlib.Topology.ContinuousMap.Ordered` `Mathlib.Topology.Covering.Basic` `Mathlib.Topology.Covering.Quotient` `Mathlib.Topology.EMetricSpace.Basic` `Mathlib.Topology.EMetricSpace.BoundedVariation` `Mathlib.Topology.EMetricSpace.Defs` `Mathlib.Topology.EMetricSpace.Diam` `Mathlib.Topology.EMetricSpace.Lipschitz` `Mathlib.Topology.EMetricSpace.Paracompact` `Mathlib.Topology.EMetricSpace.Pi` `Mathlib.Topology.EMetricSpace.VariationOnFromTo` `Mathlib.Topology.EMetricSpace.Weak` `Mathlib.Topology.FiberBundle.Basic` `Mathlib.Topology.FiberBundle.Constructions` `Mathlib.Topology.FiberBundle.Trivialization` `Mathlib.Topology.Homotopy.Basic` `Mathlib.Topology.Homotopy.Equiv` `Mathlib.Topology.Homotopy.HSpaces` `Mathlib.Topology.Homotopy.TopCat.Basic` `Mathlib.Topology.Homotopy.TopCat.Path` `Mathlib.Topology.Instances.Discrete` `Mathlib.Topology.Instances.ENNReal.ENatENNReal` `Mathlib.Topology.Instances.ENNReal.Lemmas` `Mathlib.Topology.Instances.ENat` `Mathlib.Topology.Instances.EReal.Lemmas` `Mathlib.Topology.Instances.Int` `Mathlib.Topology.Instances.NNReal.Lemmas` `Mathlib.Topology.Instances.Nat` `Mathlib.Topology.Instances.PNat` `Mathlib.Topology.Instances.Rat` `Mathlib.Topology.Instances.Sign` `Mathlib.Topology.Instances.ZMultiples` `Mathlib.Topology.LocallyFinsupp.Pushforward` `Mathlib.Topology.LocallyFinsupp` `Mathlib.Topology.Maps.Strict.Group` `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.IsometricSMul` `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.TransferInstance` `Mathlib.Topology.MetricSpace.Ultra.Basic` `Mathlib.Topology.MetricSpace.Ultra.Pi` `Mathlib.Topology.MetricSpace.Ultra.TotallySeparated` `Mathlib.Topology.Metrizable.CompletelyMetrizable` `Mathlib.Topology.Metrizable.ContinuousMap` `Mathlib.Topology.Metrizable.Real` `Mathlib.Topology.Metrizable.Uniformity` `Mathlib.Topology.Order.AtTopBotIxx` `Mathlib.Topology.Order.Basic` `Mathlib.Topology.Order.Compact` `Mathlib.Topology.Order.Completion` `Mathlib.Topology.Order.CountableSeparating` `Mathlib.Topology.Order.DenselyOrdered` `Mathlib.Topology.Order.ExtendFrom` `Mathlib.Topology.Order.Filter` `Mathlib.Topology.Order.IntermediateValue` `Mathlib.Topology.Order.IsLUB` `Mathlib.Topology.Order.IsNormal` `Mathlib.Topology.Order.LeftRightLim` `Mathlib.Topology.Order.LeftRightNhds` `Mathlib.Topology.Order.LiminfLimsup` `Mathlib.Topology.Order.MonotoneContinuity` `Mathlib.Topology.Order.MonotoneConvergence` `Mathlib.Topology.Order.Monotone` `Mathlib.Topology.Order.NhdsSet` `Mathlib.Topology.Order.ProjIcc` `Mathlib.Topology.Order.Real` `Mathlib.Topology.Order.Rolle` `Mathlib.Topology.Order.SuccPred` `Mathlib.Topology.Order.T5` `Mathlib.Topology.Order.WithTop` `Mathlib.Topology.Path` `Mathlib.Topology.Semicontinuity.Basic` `Mathlib.Topology.Semicontinuity.Lindelof` `Mathlib.Topology.Sheaves.EtaleSpace` `Mathlib.Topology.UniformSpace.CompareReals` `Mathlib.Topology.UniformSpace.Path` `Mathlib.Topology.UniformSpace.Real` `Mathlib.Topology.UnitInterval`	4
57 files `Mathlib.Algebra.Algebra.Field` `Mathlib.Algebra.Algebra.Rat` `Mathlib.Algebra.Category.BoolRing` `Mathlib.Algebra.Order.Module.Rat` `Mathlib.Algebra.Order.Ring.Star` `Mathlib.Algebra.Order.Star.Basic` `Mathlib.Algebra.Order.Star.Pi` `Mathlib.Algebra.Order.Star.Prod` `Mathlib.Algebra.QuadraticDiscriminant` `Mathlib.Algebra.Ring.BooleanRing` `Mathlib.Algebra.Ring.Identities` `Mathlib.Algebra.Star.Rat` `Mathlib.Algebra.Star.SelfAdjoint` `Mathlib.Algebra.Star.StarProjection` `Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas` `Mathlib.Combinatorics.Enumerative.Stirling` `Mathlib.Computability.Ackermann` `Mathlib.Data.Finset.Density` `Mathlib.Data.Int.Star` `Mathlib.Data.List.Shortlex` `Mathlib.Data.Nat.Digits.Defs` `Mathlib.Data.Nat.Hyperoperation` `Mathlib.Data.Rat.Cast.CharZero` `Mathlib.Data.Rat.Cast.Defs` `Mathlib.Data.Rat.Cast.Lemmas` `Mathlib.Data.Rat.Cast.OfScientific` `Mathlib.Data.Rat.Cast.Order` `Mathlib.GroupTheory.FreeGroup.CyclicallyReduced` `Mathlib.Tactic.AddGroup` `Mathlib.Tactic.Algebra.AlgebraNF` `Mathlib.Tactic.Algebra.Basic` `Mathlib.Tactic.Bound` `Mathlib.Tactic.CancelDenoms` `Mathlib.Tactic.Field` `Mathlib.Tactic.Group` `Mathlib.Tactic.IntervalCases` `Mathlib.Tactic.Linarith.Frontend` `Mathlib.Tactic.Linarith` `Mathlib.Tactic.LinearCombinationPrime` `Mathlib.Tactic.LinearCombination` `Mathlib.Tactic.NormNum.DivMod` `Mathlib.Tactic.NormNum.Eq` `Mathlib.Tactic.NormNum.GCD` `Mathlib.Tactic.NormNum.Ineq` `Mathlib.Tactic.NormNum.Inv` `Mathlib.Tactic.NormNum.IsSquare` `Mathlib.Tactic.NormNum.NatFactorial` `Mathlib.Tactic.NormNum.NatLog` `Mathlib.Tactic.NormNum.NatSqrt` `Mathlib.Tactic.NormNum.OfScientific` `Mathlib.Tactic.NormNum` `Mathlib.Tactic.Ring.Basic` `Mathlib.Tactic.Ring.Common` `Mathlib.Tactic.Ring.Compare` `Mathlib.Tactic.Ring.PNat` `Mathlib.Tactic.Ring.RingNF` `Mathlib.Tactic.Ring`	5
5 files `Mathlib.Algebra.Field.Subfield.Basic` `Mathlib.Algebra.Group.Pointwise.Finset.Interval` `Mathlib.Algebra.Order.Rearrangement` `Mathlib.Data.NNRat.Lemmas` `Mathlib.Topology.UniformSpace.AbsoluteValue`	6
8 files `Mathlib.Algebra.Order.CauSeq.Basic` `Mathlib.Algebra.Order.CauSeq.Completion` `Mathlib.Algebra.Order.Field.Basic` `Mathlib.Algebra.Order.Group.Pointwise.Interval` `Mathlib.Data.Nat.Cast.Order.Field` `Mathlib.Data.Rat.NatSqrt.Defs` `Mathlib.Order.Interval.Set.IsoIoo` `Mathlib.Tactic.Positivity`	7
6 files `Mathlib.Algebra.CharZero.Quotient` `Mathlib.Algebra.Order.Field.Rat` `Mathlib.Algebra.Order.Module.Equiv` `Mathlib.Algebra.Order.Monovary` `Mathlib.Algebra.Order.Nonneg.Field` `Mathlib.Tactic.Linarith.Preprocessing`	8
`Mathlib.Algebra.Field.Subfield.Defs` `Mathlib.Algebra.Order.Field.Subfield`	17
`Mathlib.Algebra.Field.Shrink` `Mathlib.Algebra.Field.TransferInstance`	19
`Mathlib.Algebra.Order.Module.Synonym`	70
`Mathlib.Tactic.CancelDenoms.Core`	133
`Mathlib.Algebra.Field.ModEq`	179
`Mathlib.Algebra.Field.Basic`	181
`Mathlib.Algebra.Order.Ring.Synonym`	232

Declarations diff (regex)

+ instance [AddMonoidWithOne R] [CharZero R] : CharZero (Lex R) := inferInstanceAs <| CharZero R
+ instance [AddMonoidWithOne R] [CharZero R] : CharZero Rᵒᵈ := inferInstanceAs <| CharZero R
+ instance {p : ℕ} [AddMonoidWithOne R] [CharP R p] : CharP (Lex R) p := inferInstanceAs <| CharP R p
+ instance {p : ℕ} [AddMonoidWithOne R] [CharP R p] : CharP Rᵒᵈ p := inferInstanceAs <| CharP R p

You can run this locally as follows

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

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

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

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

Declarations diff (Lean)

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

+4 new declarations
−0 removed declarations

+Lex.instCharP
+Lex.instCharZero
+OrderDual.instCharP
+OrderDual.instCharZero

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 4606c8371a
Reference commit ac10dc7e9a

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

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

add CharZero/CharP instances on OrderDual and Lex

82012b4

github-actions Bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Aug 7, 2026

github-actions Bot added the t-algebra Algebra (groups, rings, fields, etc) label Aug 7, 2026

fix

4606c83

Navigation Menu

Uh oh!

feat: add `CharZero`/`CharP` instances on `OrderDual` and `Lex` - #42541

feat: add `CharZero`/`CharP` instances on `OrderDual` and `Lex`#42541
NoahW314 wants to merge 2 commits into
leanprover-community:masterfrom
NoahW314:Char

NoahW314 commented Aug 7, 2026

Uh oh!

github-actions Bot commented Aug 7, 2026 •

edited

Loading

Import changes for modified files

Declarations diff (regex)

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Uh oh!

Conversation

NoahW314 commented Aug 7, 2026

Uh oh!

github-actions Bot commented Aug 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 4606c8371a

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

github-actions Bot commented Aug 7, 2026 •

edited

Loading