[Merged by Bors] - chore: complete deprecation of `PartENat.card` by kim-em · Pull Request #19648 · leanprover-community/mathlib4

kim-em · 2024-12-01T02:41:08Z

depends on: [Merged by Bors] - chore: remove PartENat from PowerSeries #19622 (perhaps unnecessarily)

github-actions · 2024-12-01T02:41:59Z

PR summary 5b4febff9e

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.SetTheory.Cardinal.Aleph	756	680	-76 (-10.05%)
Mathlib.SetTheory.Cardinal.Finite	757	686	-71 (-9.38%)
Mathlib.Data.Finite.Card	758	687	-71 (-9.37%)
Mathlib.Data.Matroid.Basic	761	691	-70 (-9.20%)
Mathlib.Algebra.Group.Subgroup.Finite	777	707	-70 (-9.01%)
Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting	776	709	-67 (-8.63%)
Mathlib.Data.Matroid.IndepAxioms	762	699	-63 (-8.27%)
Mathlib.Data.Matroid.Closure	766	705	-61 (-7.96%)
Mathlib.SetTheory.Cardinal.Continuum	782	769	-13 (-1.66%)
Mathlib.SetTheory.Cardinal.Cofinality	782	773	-9 (-1.15%)
Mathlib.GroupTheory.OrderOfElement	865	862	-3 (-0.35%)
Mathlib.RingTheory.PowerSeries.Order	1045	1043	-2 (-0.19%)
Mathlib.RingTheory.PowerSeries.Inverse	1244	1242	-2 (-0.16%)
Mathlib.NumberTheory.FLT.Three	2542	2540	-2 (-0.08%)

Import changes for all files

Files	Import difference
`Mathlib.SetTheory.Cardinal.PartENat`	-750
`Mathlib.SetTheory.Cardinal.Aleph`	-76
5 files `Mathlib.Data.Fintype.Units` `Mathlib.Data.Finite.Card` `Mathlib.SetTheory.Cardinal.Finite` `Mathlib.Data.Set.Card` `Mathlib.Algebra.Group.ConjFinite`	-71
3 files `Mathlib.Data.Matroid.Basic` `Mathlib.Algebra.Group.Pointwise.Set.Card` `Mathlib.Algebra.Group.Subgroup.Finite`	-70
`Mathlib.Algebra.GroupWithZero.Pointwise.Set.Card`	-69
`Mathlib.GroupTheory.Coset.Card`	-68
`Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting`	-67
`Mathlib.MeasureTheory.MeasurableSpace.NCard`	-64
6 files `Mathlib.Data.Matroid.Map` `Mathlib.Data.Matroid.Dual` `Mathlib.Data.Matroid.Constructions` `Mathlib.Data.Matroid.IndepAxioms` `Mathlib.Data.Matroid.Restrict` `Mathlib.Data.Matroid.Sum`	-63
`Mathlib.GroupTheory.ClassEquation` `Mathlib.Data.Matroid.Closure`	-61
4 files `Mathlib.CategoryTheory.Galois.GaloisObjects` `Mathlib.CategoryTheory.Galois.Decomposition` `Mathlib.CategoryTheory.Galois.Basic` `Mathlib.GroupTheory.Finiteness`	-58
`Mathlib.GroupTheory.QuotientGroup.Finite`	-56
`Mathlib.CategoryTheory.Galois.Prorepresentability`	-55
3 files `Mathlib.LinearAlgebra.Quotient.Pi` `Mathlib.LinearAlgebra.Quotient.Basic` `Mathlib.LinearAlgebra.Isomorphisms`	-53
3 files `Mathlib.LinearAlgebra.Projection` `Mathlib.Algebra.Exact` `Mathlib.Algebra.Module.SnakeLemma`	-51
4 files `Mathlib.Algebra.Category.Grp.Subobject` `Mathlib.Algebra.Category.ModuleCat.Kernels` `Mathlib.Algebra.Category.ModuleCat.Subobject` `Mathlib.Algebra.Category.ModuleCat.EpiMono`	-46
3 files `Mathlib.CategoryTheory.Abelian.Pseudoelements` `Mathlib.Algebra.Category.ModuleCat.Injective` `Mathlib.CategoryTheory.Preadditive.Yoneda.Injective`	-44
`Mathlib.GroupTheory.Perm.DomMulAct`	-41
`Mathlib.GroupTheory.Commutator.Finite` `Mathlib.GroupTheory.Perm.Subgroup`	-40
`Mathlib.GroupTheory.GroupAction.CardCommute`	-39
3 files `Mathlib.Algebra.Module.Presentation.Tautological` `Mathlib.Algebra.Module.Presentation.Cokernel` `Mathlib.Algebra.Module.Presentation.Basic`	-37
7 files `Mathlib.GroupTheory.Abelianization` `Mathlib.GroupTheory.Solvable` `Mathlib.Algebra.Category.Grp.Adjunctions` `Mathlib.GroupTheory.Commensurable` `Mathlib.GroupTheory.Index` `Mathlib.RingTheory.FreeRing` `Mathlib.GroupTheory.FreeAbelianGroup`	-31
5 files `Mathlib.RingTheory.Finiteness.Bilinear` `Mathlib.RingTheory.Finiteness.Prod` `Mathlib.Analysis.CStarAlgebra.Module.Synonym` `Mathlib.RingTheory.Finiteness.Defs` `Mathlib.RingTheory.Finiteness.Nilpotent`	-29
8 files `Mathlib.Combinatorics.SimpleGraph.StronglyRegular` `Mathlib.RingTheory.Noetherian.Filter` `Mathlib.RingTheory.Finiteness.Lattice` `Mathlib.RingTheory.Finiteness.Basic` `Mathlib.RingTheory.Noetherian.Defs` `Mathlib.RingTheory.Finiteness.Finsupp` `Mathlib.Algebra.Module.LocalizedModule.Exact` `Mathlib.Combinatorics.SimpleGraph.AdjMatrix`	-28
`Mathlib.CategoryTheory.Galois.Examples`	-23
`Mathlib.Combinatorics.Additive.RuzsaCovering`	-22
`Mathlib.CategoryTheory.Galois.Full` `Mathlib.CategoryTheory.Galois.Action`	-21
9 files `Mathlib.RingTheory.Coalgebra.Basic` `Mathlib.Algebra.Module.Presentation.Free` `Mathlib.RingTheory.Coalgebra.Hom` `Mathlib.Algebra.Category.CoalgebraCat.Basic` `Mathlib.LinearAlgebra.TensorProduct.Finiteness` `Mathlib.Algebra.Module.Presentation.DirectSum` `Mathlib.RingTheory.Coalgebra.Equiv` `Mathlib.Algebra.Category.ModuleCat.Projective` `Mathlib.LinearAlgebra.Basis.VectorSpace`	-20
3 files `Mathlib.LinearAlgebra.Alternating.DomCoprod` `Mathlib.LinearAlgebra.AffineSpace.Basis` `Mathlib.LinearAlgebra.AffineSpace.Independent`	-19
5 files `Mathlib.Analysis.Convex.SimplicialComplex.Basic` `Mathlib.Analysis.Convex.Independent` `Mathlib.Analysis.Convex.Combination` `Mathlib.Analysis.Convex.Caratheodory` `Mathlib.Analysis.Convex.StoneSeparation`	-16
7 files `Mathlib.Data.W.Cardinal` `Mathlib.SetTheory.Cardinal.Arithmetic` `Mathlib.RingTheory.OreLocalization.Cardinality` `Mathlib.ModelTheory.Encoding` `Mathlib.SetTheory.Cardinal.Continuum` `Mathlib.GroupTheory.MonoidLocalization.Cardinality` `Mathlib.GroupTheory.OreLocalization.Cardinality`	-13
14 files `Mathlib.Algebra.Category.CoalgebraCat.ComonEquivalence` `Mathlib.ModelTheory.PartialEquiv` `Mathlib.ModelTheory.Substructures` `Mathlib.ModelTheory.FinitelyGenerated` `Mathlib.RingTheory.Coalgebra.TensorProduct` `Mathlib.ModelTheory.Skolem` `Mathlib.SetTheory.Cardinal.Subfield` `Mathlib.ModelTheory.ElementarySubstructures` `Mathlib.Algebra.Category.CoalgebraCat.Monoidal` `Mathlib.ModelTheory.Bundled` `Mathlib.ModelTheory.Fraisse` `Mathlib.ModelTheory.DirectLimit` `Mathlib.ModelTheory.ElementaryMaps` `Mathlib.Algebra.Module.LocalizedModule.Submodule`	-12
`Mathlib.RingTheory.Finiteness.Subalgebra`	-10
15 files `Mathlib.SetTheory.Game.Short` `Mathlib.SetTheory.Cardinal.Finsupp` `Mathlib.ModelTheory.Complexity` `Mathlib.ModelTheory.Graph` `Mathlib.SetTheory.Cardinal.Cofinality` `Mathlib.SetTheory.Game.State` `Mathlib.SetTheory.Game.Domineering` `Mathlib.MeasureTheory.MeasurableSpace.Card` `Mathlib.SetTheory.Cardinal.CountableCover` `Mathlib.ModelTheory.Order` `Mathlib.ModelTheory.Equivalence` `Mathlib.ModelTheory.Types` `Mathlib.Order.Filter.Cocardinal` `Mathlib.ModelTheory.Satisfiability` `Mathlib.Order.Filter.CardinalInter`	-9
9 files `Mathlib.RingTheory.Bialgebra.Hom` `Mathlib.RingTheory.Bialgebra.TensorProduct` `Mathlib.RingTheory.Bialgebra.Basic` `Mathlib.Algebra.Order.Chebyshev` `Mathlib.Algebra.Category.BialgebraCat.Basic` `Mathlib.RingTheory.HopfAlgebra` `Mathlib.RingTheory.Bialgebra.Equiv` `Mathlib.Algebra.Group.UniqueProds.VectorSpace` `Mathlib.Algebra.Category.HopfAlgebraCat.Basic`	-8
`Mathlib.GroupTheory.Perm.ConjAct`	-6
`Mathlib.SetTheory.Cardinal.Divisibility` `Mathlib.Algebra.Polynomial.Cardinal`	-5
3 files `Mathlib.GroupTheory.Perm.Cycle.Basic` `Mathlib.GroupTheory.Perm.Closure` `Mathlib.GroupTheory.Perm.Cycle.Factors`	-4
186 files `Mathlib.Algebra.Homology.ShortComplex.Ab` `Mathlib.CategoryTheory.Galois.IsFundamentalgroup` `Mathlib.Analysis.Normed.Group.Uniform` `Mathlib.RingTheory.Localization.Away.Lemmas` `Mathlib.Topology.Algebra.InfiniteSum.Group` `Mathlib.Topology.Algebra.NonUnitalStarAlgebra` `Mathlib.Algebra.Category.ModuleCat.Limits` `Mathlib.RingTheory.Noetherian.Orzech` `Mathlib.RingTheory.IsPrimary` `Mathlib.RingTheory.Lasker` `Mathlib.Topology.Algebra.SeparationQuotient.Section` `Mathlib.Topology.ContinuousMap.Star` `Mathlib.Analysis.Normed.Lp.WithLp` `Mathlib.Algebra.Category.ModuleCat.Abelian` `Mathlib.RingTheory.Ideal.IsPrincipal` `Mathlib.CategoryTheory.Abelian.Ext` `Mathlib.RingTheory.GradedAlgebra.Noetherian` `Mathlib.RingTheory.QuotSMulTop` `Mathlib.RingTheory.TensorProduct.Finite` `Mathlib.Algebra.Category.Grp.AB5` `Mathlib.Topology.Algebra.Module.ModuleTopology` `Mathlib.RingTheory.FractionalIdeal.Extended` `Mathlib.RingTheory.Finiteness.Nakayama` `Mathlib.Algebra.Category.ModuleCat.ChangeOfRings` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits` `Mathlib.GroupTheory.OrderOfElement` `Mathlib.RingTheory.Ideal.Quotient.Noetherian` `Mathlib.GroupTheory.FreeAbelianGroupFinsupp` `Mathlib.Topology.Sheaves.MayerVietoris` `Mathlib.Algebra.Category.Grp.Abelian` `Mathlib.RingTheory.Localization.Ideal` `Mathlib.Algebra.Category.AlgebraCat.Limits` `Mathlib.Algebra.Quaternion` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits` `Mathlib.Topology.ContinuousMap.Lattice` `Mathlib.Algebra.DualQuaternion` `Mathlib.Algebra.Category.ModuleCat.Sheaf` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Free` `Mathlib.RingTheory.PrincipalIdealDomain` `Mathlib.Topology.Algebra.InfiniteSum.Module` `Mathlib.GroupTheory.NoncommPiCoprod` `Mathlib.Algebra.Homology.ShortComplex.ModuleCat` `Mathlib.Analysis.Normed.Group.SemiNormedGrp` `Mathlib.LinearAlgebra.FreeModule.PID` `Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv` `Mathlib.Topology.Algebra.InfiniteSum.NatInt` `Mathlib.Topology.ContinuousMap.LocallyConstant` `Mathlib.RingTheory.Noetherian.Basic` `Mathlib.Data.Real.IsNonarchimedean` `Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion` `Mathlib.RingTheory.Noetherian.Nilpotent` `Mathlib.NumberTheory.PellMatiyasevic` `Mathlib.Algebra.Category.Ring.Epi` `Mathlib.RingTheory.FractionalIdeal.Basic` `Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings` `Mathlib.Algebra.Category.ModuleCat.Biproducts` `Mathlib.RingTheory.Derivation.ToSquareZero` `Mathlib.RingTheory.Valuation.ValuationRing` `Mathlib.LinearAlgebra.FreeModule.Finite.Basic` `Mathlib.RingTheory.Ideal.Quotient.Nilpotent` `Mathlib.RingTheory.MvPolynomial.Localization` `Mathlib.LinearAlgebra.TensorProduct.Quotient` `Mathlib.RingTheory.Localization.Submodule` `Mathlib.NumberTheory.Zsqrtd.GaussianInt` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits` `Mathlib.RingTheory.MvPolynomial.FreeCommRing` `Mathlib.RingTheory.Nilpotent.Lemmas` `Mathlib.Analysis.Normed.Group.Ultra` `Mathlib.Algebra.LinearRecurrence` `Mathlib.Topology.Algebra.StarSubalgebra` `Mathlib.CategoryTheory.Abelian.Injective` `Mathlib.Analysis.Normed.Group.BallSphere` `Mathlib.CategoryTheory.Abelian.Projective` `Mathlib.Topology.Algebra.Module.Multilinear.Basic` `Mathlib.Algebra.Polynomial.Derivation` `Mathlib.Topology.Algebra.InfiniteSum.Ring` `Mathlib.Topology.MetricSpace.Algebra` `Mathlib.RingTheory.Finiteness.TensorProduct` `Mathlib.Algebra.Polynomial.Module.Basic` `Mathlib.Analysis.Normed.MulAction` `Mathlib.CategoryTheory.Galois.Topology` `Mathlib.LinearAlgebra.InvariantBasisNumber` `Mathlib.RingTheory.OrzechProperty` `Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian` `Mathlib.Algebra.DirectLimit` `Mathlib.RingTheory.Ideal.AssociatedPrime` `Mathlib.NumberTheory.Harmonic.Int` `Mathlib.Topology.Algebra.UniformFilterBasis` `Mathlib.Topology.Algebra.Nonarchimedean.Bases` `Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber` `Mathlib.Topology.Algebra.Module.LinearPMap` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator` `Mathlib.Topology.Algebra.Group.TopologicalAbelianization` `Mathlib.Topology.Algebra.Algebra` `Mathlib.NumberTheory.Dioph` `Mathlib.RingTheory.EuclideanDomain` `Mathlib.Algebra.Category.Grp.Images` `Mathlib.Algebra.Module.FinitePresentation` `Mathlib.RingTheory.Int.Basic` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits` `Mathlib.Topology.Algebra.FilterBasis` `Mathlib.LinearAlgebra.TensorProduct.DirectLimit` `Mathlib.RingTheory.Finiteness.Cardinality` `Mathlib.GroupTheory.GroupAction.Blocks` `Mathlib.RingTheory.Ideal.IsPrimary` `Mathlib.RingTheory.Bezout` `Mathlib.Analysis.Normed.Operator.LinearIsometry` `Mathlib.RingTheory.Adjoin.Dimension` `Mathlib.Algebra.Module.Presentation.Finite` `Mathlib.Algebra.Homology.LocalCohomology` `Mathlib.Analysis.Normed.Field.Ultra` `Mathlib.Algebra.Category.ModuleCat.Presheaf` `Mathlib.RingTheory.Idempotents` `Mathlib.Algebra.MvPolynomial.Cardinal` `Mathlib.Analysis.Convex.Jensen` `Mathlib.Topology.Algebra.ClopenNhdofOne` `Mathlib.Topology.Algebra.Module.Basic` `Mathlib.ModelTheory.Algebra.Ring.FreeCommRing` `Mathlib.SetTheory.Cardinal.Free` `Mathlib.CategoryTheory.Sites.MayerVietorisSquare` `Mathlib.Algebra.FreeAlgebra.Cardinality` `Mathlib.RingTheory.Valuation.Quotient` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification` `Mathlib.LinearAlgebra.Dimension.Free` `Mathlib.LinearAlgebra.TensorProduct.RightExactness` `Mathlib.Topology.Algebra.InfiniteSum.Order` `Mathlib.ModelTheory.Algebra.Field.CharP` `Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono` `Mathlib.RingTheory.MvPolynomial.Basic` `Mathlib.Topology.Algebra.Module.WeakDual` `Mathlib.RingTheory.FreeCommRing` `Mathlib.CategoryTheory.Preadditive.HomOrthogonal` `Mathlib.LinearAlgebra.Dimension.Constructions` `Mathlib.RingTheory.Ideal.Quotient.Operations` `Mathlib.Algebra.QuaternionBasis` `Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory` `Mathlib.LinearAlgebra.Dimension.StrongRankCondition` `Mathlib.Algebra.Category.ModuleCat.Free` `Mathlib.Topology.ContinuousMap.Algebra` `Mathlib.NumberTheory.Zsqrtd.Basic` `Mathlib.RingTheory.Ideal.IdempotentFG` `Mathlib.RingTheory.Finiteness.Ideal` `Mathlib.Topology.Algebra.Module.Alternating.Basic` `Mathlib.Algebra.Category.ModuleCat.Images` `Mathlib.RingTheory.Finiteness.Projective` `Mathlib.Topology.Algebra.Module.CharacterSpace` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal` `Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient` `Mathlib.CategoryTheory.Galois.EssSurj` `Mathlib.RingTheory.PrincipalIdealDomainOfPrime` `Mathlib.RingTheory.Localization.Cardinality` `Mathlib.FieldTheory.Tower` `Mathlib.NumberTheory.FLT.Basic` `Mathlib.RingTheory.PrimeSpectrum` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Abelian` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward` `Mathlib.Topology.Algebra.SeparationQuotient.Basic` `Mathlib.LinearAlgebra.FiniteSpan` `Mathlib.Topology.Algebra.ContinuousAffineMap` `Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous` `Mathlib.Topology.Algebra.NonUnitalAlgebra` `Mathlib.Topology.Instances.TrivSqZeroExt` `Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify` `Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent` `Mathlib.Analysis.Normed.Operator.ContinuousLinearMap` `Mathlib.LinearAlgebra.Basis.Cardinality` `Mathlib.Topology.Algebra.Module.Star` `Mathlib.Analysis.Normed.Ring.Ultra` `Mathlib.Algebra.Polynomial.Module.AEval` `Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings` `Mathlib.Analysis.Normed.Group.Hom` `Mathlib.Analysis.Normed.Group.NullSubmodule` `Mathlib.Algebra.Homology.ConcreteCategory` `Mathlib.RingTheory.Noetherian.UniqueFactorizationDomain` `Mathlib.Topology.Algebra.InfiniteSum.Constructions` `Mathlib.LinearAlgebra.TensorProduct.Vanishing` `Mathlib.Topology.Algebra.ClosedSubgroup` `Mathlib.Analysis.Convex.Exposed` `Mathlib.RingTheory.Localization.Algebra` `Mathlib.CategoryTheory.Preadditive.Yoneda.Limits` `Mathlib.Algebra.Category.ModuleCat.Presheaf.Free` `Mathlib.RingTheory.Ideal.Quotient.Basic` `Mathlib.Topology.Algebra.ContinuousMonoidHom`	-3
395 files `Mathlib.Algebra.Polynomial.FieldDivision` `Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing` `Mathlib.Combinatorics.SimpleGraph.Triangle.Removal` `Mathlib.Analysis.CStarAlgebra.GelfandDuality` `Mathlib.Analysis.InnerProductSpace.Spectrum` `Mathlib.RingTheory.Henselian` `Mathlib.Analysis.Calculus.Deriv.Inv` `Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv` `Mathlib.Geometry.Manifold.ContMDiff.Atlas` `Mathlib.RingTheory.Polynomial.Content` `Mathlib.RingTheory.Localization.AtPrime` `Mathlib.NumberTheory.LSeries.HurwitzZetaValues` `Mathlib.Analysis.SpecialFunctions.Gamma.Basic` `Mathlib.Geometry.Manifold.VectorBundle.Pullback` `Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith` `Mathlib.Analysis.Complex.Angle` `Mathlib.LinearAlgebra.Matrix.PosDef` `Mathlib.Analysis.SpecialFunctions.Integrals` `Mathlib.NumberTheory.Harmonic.ZetaAsymp` `Mathlib.Analysis.Calculus.BumpFunction.Convolution` `Mathlib.Analysis.Fourier.PoissonSummation` `Mathlib.Analysis.InnerProductSpace.Rayleigh` `Mathlib.NumberTheory.NumberField.Discriminant.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms` `Mathlib.Geometry.Manifold.VectorBundle.Basic` `Mathlib.Analysis.Calculus.Deriv.Abs` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds` `Mathlib.Tactic.FunProp.ContDiff` `Mathlib.Analysis.Distribution.FourierSchwartz` `Mathlib.Analysis.Calculus.ParametricIntervalIntegral` `Mathlib.Geometry.Manifold.VectorBundle.Tangent` `Mathlib.FieldTheory.Laurent` `Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno` `Mathlib.NumberTheory.GaussSum` `Mathlib.Algebra.Category.Ring.Instances` `Mathlib.Geometry.Manifold.Diffeomorph` `Mathlib.Combinatorics.Derangements.Exponential` `Mathlib.LinearAlgebra.FreeModule.StrongRankCondition` `Mathlib.Combinatorics.Additive.Corner.Roth` `Mathlib.NumberTheory.EulerProduct.DirichletLSeries` `Mathlib.Analysis.Complex.AbsMax` `Mathlib.Geometry.Manifold.MFDeriv.Basic` `Mathlib.Analysis.CStarAlgebra.Spectrum` `Mathlib.RingTheory.Valuation.ExtendToLocalization` `Mathlib.Geometry.Manifold.Instances.Real` `Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv` `Mathlib.RingTheory.AdicCompletion.Basic` `Mathlib.Geometry.Manifold.Complex` `Mathlib.NumberTheory.LSeries.DirichletContinuation` `Mathlib.MeasureTheory.Integral.CircleIntegral` `Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral` `Mathlib.RingTheory.Algebraic.MvPolynomial` `Mathlib.Analysis.SpecialFunctions.Gamma.Beta` `Mathlib.MeasureTheory.Integral.TorusIntegral` `Mathlib.Geometry.Manifold.MFDeriv.FDeriv` `Mathlib.RingTheory.Polynomial.Quotient` `Mathlib.Algebra.CharP.LocalRing` `Mathlib.Analysis.Complex.Periodic` `Mathlib.Geometry.Manifold.ContMDiffMap` `Mathlib.Algebra.MvPolynomial.Funext` `Mathlib.Analysis.Complex.TaylorSeries` `Mathlib.Analysis.Normed.Algebra.Spectrum` `Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions` `Mathlib.Analysis.FunctionalSpaces.SobolevInequality` `Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas` `Mathlib.NumberTheory.LSeries.ZMod` `Mathlib.Analysis.CStarAlgebra.Module.Constructions` `Mathlib.Probability.Distributions.Exponential` `Mathlib.RingTheory.RingHom.FiniteType` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric` `Mathlib.Analysis.SpecialFunctions.Complex.Arctan` `Mathlib.RingTheory.Algebraic.Cardinality` `Mathlib.Topology.Sheaves.CommRingCat` `Mathlib.Analysis.Calculus.AddTorsor.AffineMap` `Mathlib.RingTheory.DiscreteValuationRing.Basic` `Mathlib.RingTheory.KrullDimension.Field` `Mathlib.Algebra.Polynomial.Splits` `Mathlib.RingTheory.Localization.AsSubring` `Mathlib.RingTheory.Localization.Finiteness` `Mathlib.Analysis.Calculus.FDeriv.Analytic` `Mathlib.FieldTheory.Minpoly.Basic` `Mathlib.Analysis.SpecialFunctions.Log.NegMulLog` `Mathlib.Analysis.Calculus.BumpFunction.Basic` `Mathlib.NumberTheory.NumberField.EquivReindex` `Mathlib.Analysis.SpecialFunctions.ImproperIntegrals` `Mathlib.RingTheory.Polynomial.Hermite.Gaussian` `Mathlib.Analysis.Calculus.AddTorsor.Coord` `Mathlib.Analysis.Fourier.ZMod` `Mathlib.Analysis.SpecialFunctions.Complex.LogBounds` `Mathlib.Analysis.SpecialFunctions.Gamma.Deligne` `Mathlib.Analysis.Complex.PhragmenLindelof` `Mathlib.Algebra.CubicDiscriminant` `Mathlib.Analysis.Calculus.SmoothSeries` `Mathlib.RingTheory.Ideal.MinimalPrime` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff` `Mathlib.Analysis.InnerProductSpace.NormPow` `Mathlib.Analysis.Calculus.Deriv.Polynomial` `Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls` `Mathlib.RingTheory.Polynomial.IrreducibleRing` `Mathlib.MeasureTheory.Integral.FundThmCalculus` `Mathlib.NumberTheory.Cyclotomic.Three` `Mathlib.RingTheory.RingHom.Finite` `Mathlib.NumberTheory.LSeries.HurwitzZetaEven` `Mathlib.RingTheory.Unramified.Field` `Mathlib.RingTheory.EssentialFiniteness` `Mathlib.Geometry.Manifold.PoincareConjecture` `Mathlib.RingTheory.PowerSeries.Derivative` `Mathlib.NumberTheory.LSeries.Deriv` `Mathlib.Analysis.Fourier.AddCircle` `Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation` `Mathlib.Analysis.Calculus.MeanValue` `Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap` `Mathlib.Analysis.Fourier.Inversion` `Mathlib.Analysis.Normed.Algebra.QuaternionExponential` `Mathlib.Computability.AkraBazzi.AkraBazzi` `Mathlib.RingTheory.Polynomial.Radical` `Mathlib.NumberTheory.NumberField.Completion` `Mathlib.Analysis.SpecialFunctions.NonIntegrable` `Mathlib.Analysis.Calculus.Deriv.Pow` `Mathlib.Analysis.Calculus.Taylor` `Mathlib.RingTheory.DualNumber` `Mathlib.Analysis.SpecialFunctions.Complex.Analytic` `Mathlib.Combinatorics.SimpleGraph.Regularity.Increment` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic` `Mathlib.Analysis.Calculus.LHopital` `Mathlib.LinearAlgebra.Matrix.Ideal` `Mathlib.Geometry.Manifold.SmoothManifoldWithCorners` `Mathlib.Probability.Distributions.Gaussian` `Mathlib.RingTheory.Algebraic.Basic` `Mathlib.Analysis.Calculus.UniformLimitsDeriv` `Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart` `Mathlib.Geometry.Manifold.BumpFunction` `Mathlib.Analysis.Calculus.FDeriv.Extend` `Mathlib.Algebra.Polynomial.Expand` `Mathlib.Geometry.Manifold.IntegralCurve.Basic` `Mathlib.RingTheory.Polynomial.Vieta` `Mathlib.NumberTheory.Harmonic.GammaDeriv` `Mathlib.Geometry.Manifold.InteriorBoundary` `Mathlib.Geometry.Manifold.ContMDiffMFDeriv` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone` `Mathlib.Geometry.Manifold.ContMDiff.Basic` `Mathlib.RingTheory.Etale.Field` `Mathlib.Data.Real.Pi.Irrational` `Mathlib.RingTheory.FinitePresentation` `Mathlib.Analysis.Complex.CauchyIntegral` `Mathlib.Analysis.InnerProductSpace.JointEigenspace` `Mathlib.Analysis.Calculus.ContDiff.Defs` `Mathlib.Analysis.SpecialFunctions.Pow.Deriv` `Mathlib.Analysis.SpecialFunctions.PolarCoord` `Mathlib.RingTheory.RingHom.Injective` `Mathlib.RingTheory.Localization.LocalizationLocalization` `Mathlib.Analysis.Calculus.ParametricIntegral` `Mathlib.Analysis.Complex.UpperHalfPlane.Metric` `Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential` `Mathlib.LinearAlgebra.TensorAlgebra.Basis` `Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable` `Mathlib.RingTheory.Adjoin.Tower` `Mathlib.Geometry.RingedSpace.OpenImmersion` `Mathlib.Analysis.Calculus.Deriv.ZPow` `Mathlib.NumberTheory.Cyclotomic.Embeddings` `Mathlib.Analysis.CStarAlgebra.Module.Defs` `Mathlib.Analysis.Complex.Schwarz` `Mathlib.RingTheory.Adjoin.FG` `Mathlib.Analysis.Fourier.FourierTransformDeriv` `Mathlib.Dynamics.Newton` `Mathlib.RingTheory.FiniteStability` `Mathlib.RingTheory.Localization.InvSubmonoid` `Mathlib.Analysis.Calculus.DiffContOnCl` `Mathlib.Analysis.Complex.UpperHalfPlane.Manifold` `Mathlib.NumberTheory.LSeries.RiemannZeta` `Mathlib.Data.Real.Pi.Leibniz` `Mathlib.NumberTheory.FLT.Three` `Mathlib.RingTheory.Filtration` `Mathlib.Geometry.Manifold.Algebra.SmoothFunctions` `Mathlib.Geometry.Euclidean.Inversion.Calculus` `Mathlib.Analysis.Calculus.FirstDerivativeTest` `Mathlib.RingTheory.Nakayama` `Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody` `Mathlib.NumberTheory.NumberField.Units.Basic` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique` `Mathlib.NumberTheory.DirichletCharacter.GaussSum` `Mathlib.Geometry.Manifold.Sheaf.Smooth` `Mathlib.Geometry.Manifold.VectorBundle.Hom` `Mathlib.Algebra.AlgebraicCard` `Mathlib.Analysis.Calculus.ContDiff.Bounds` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds` `Mathlib.Probability.Distributions.Poisson` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable` `Mathlib.NumberTheory.LSeries.Dirichlet` `Mathlib.NumberTheory.Fermat` `Mathlib.NumberTheory.Transcendental.Liouville.Residual` `Mathlib.Algebra.Polynomial.Degree.CardPowDegree` `Mathlib.Analysis.CStarAlgebra.ApproximateUnit` `Mathlib.RingTheory.SurjectiveOnStalks` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog` `Mathlib.Tactic.NormNum.LegendreSymbol` `Mathlib.Analysis.Calculus.ContDiff.Basic` `Mathlib.Analysis.Calculus.DSlope` `Mathlib.Analysis.SpecialFunctions.BinaryEntropy` `Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable` `Mathlib.Analysis.Fourier.RiemannLebesgueLemma` `Mathlib.RingTheory.LocalProperties.Exactness` `Mathlib.Analysis.Calculus.Deriv.Mul` `Mathlib.Analysis.SpecialFunctions.SmoothTransition` `Mathlib.RingTheory.Polynomial.Basic` `Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass` `Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf` `Mathlib.RingTheory.LocalRing.ResidueField.Defs` `Mathlib.Analysis.InnerProductSpace.Calculus` `Mathlib.Analysis.SpecialFunctions.Exponential` `Mathlib.RingTheory.ReesAlgebra` `Mathlib.Analysis.Analytic.Meromorphic` `Mathlib.NumberTheory.LSeries.Nonvanishing` `Mathlib.Analysis.Calculus.FDeriv.Norm` `Mathlib.Combinatorics.Additive.AP.Three.Behrend` `Mathlib.Analysis.Complex.Polynomial.Basic` `Mathlib.MeasureTheory.Integral.IntegralEqImproper` `Mathlib.Analysis.Calculus.LocalExtr.Polynomial` `Mathlib.Analysis.Calculus.IteratedDeriv.Defs` `Mathlib.LinearAlgebra.FreeAlgebra` `Mathlib.Analysis.Complex.RemovableSingularity` `Mathlib.RingTheory.JacobsonIdeal` `Mathlib.Analysis.Complex.Liouville` `Mathlib.NumberTheory.Transcendental.Liouville.Measure` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum` `Mathlib.NumberTheory.LSeries.MellinEqDirichlet` `Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol` `Mathlib.RingTheory.LocalRing.Subring` `Mathlib.Analysis.Calculus.Darboux` `Mathlib.Analysis.Complex.LocallyUniformLimit` `Mathlib.NumberTheory.LSeries.Positivity` `Mathlib.Analysis.InnerProductSpace.EuclideanDist` `Mathlib.NumberTheory.Harmonic.EulerMascheroni` `Mathlib.RingTheory.Localization.Free` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace` `Mathlib.Analysis.SpecialFunctions.Log.Deriv` `Mathlib.NumberTheory.LegendreSymbol.AddCharacter` `Mathlib.NumberTheory.Cyclotomic.PID` `Mathlib.NumberTheory.JacobiSum.Basic` `Mathlib.Topology.MetricSpace.HausdorffDimension` `Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff` `Mathlib.Analysis.Calculus.LineDeriv.Basic` `Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity` `Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup` `Mathlib.Data.Real.Pi.Bounds` `Mathlib.Geometry.Manifold.MFDeriv.NormedSpace` `Mathlib.RingTheory.KrullDimension.Basic` `Mathlib.RingTheory.EisensteinCriterion` `Mathlib.Geometry.Manifold.MFDeriv.Defs` `Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization` `Mathlib.NumberTheory.ModularForms.Basic` `Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra` `Mathlib.Analysis.InnerProductSpace.StarOrder` `Mathlib.Analysis.Calculus.LineDeriv.Measurable` `Mathlib.MeasureTheory.Integral.PeakFunction` `Mathlib.RingTheory.SimpleRing.Matrix` `Mathlib.NumberTheory.NumberField.Units.DirichletTheorem` `Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk` `Mathlib.Geometry.Manifold.ContMDiff.Defs` `Mathlib.RingTheory.RingHom.Locally` `Mathlib.Analysis.Normed.Algebra.Basic` `Mathlib.MeasureTheory.Integral.ExpDecay` `Mathlib.Geometry.Manifold.IntegralCurve.UniformTime` `Mathlib.NumberTheory.NumberField.Units.Regulator` `Mathlib.Analysis.Calculus.ContDiff.RCLike` `Mathlib.Analysis.SpecialFunctions.Stirling` `Mathlib.Analysis.ODE.Gronwall` `Mathlib.Analysis.Calculus.FDeriv.Mul` `Mathlib.RingTheory.Polynomial.Nilpotent` `Mathlib.RingTheory.Polynomial.Selmer` `Mathlib.RingTheory.Polynomial.UniqueFactorization` `Mathlib.MeasureTheory.Constructions.HaarToSphere` `Mathlib.Analysis.SpecialFunctions.JapaneseBracket` `Mathlib.RingTheory.LocalProperties.Submodule` `Mathlib.MeasureTheory.Integral.CircleTransform` `Mathlib.NumberTheory.ZetaValues` `Mathlib.Analysis.Convex.Deriv` `Mathlib.Analysis.SpecialFunctions.Arsinh` `Mathlib.Analysis.Complex.Positivity` `Mathlib.Analysis.Calculus.ContDiff.FiniteDimension` `Mathlib.RingTheory.LocalProperties.Reduced` `Mathlib.LinearAlgebra.Matrix.LDL` `Mathlib.Tactic.FunProp.Differentiable` `Mathlib.Geometry.Manifold.MFDeriv.Tangent` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances` `Mathlib.Analysis.Convolution` `Mathlib.LinearAlgebra.Matrix.SchurComplement` `Mathlib.Analysis.Calculus.VectorField` `Mathlib.Algebra.Category.Ring.Under.Basic` `Mathlib.Geometry.Manifold.Algebra.Monoid` `Mathlib.Analysis.MellinInversion` `Mathlib.NumberTheory.BernoulliPolynomials` `Mathlib.RingTheory.RingHomProperties` `Mathlib.Geometry.Manifold.Algebra.Structures` `Mathlib.Algebra.Category.Ring.Constructions` `Mathlib.RingTheory.Polynomial.Eisenstein.Basic` `Mathlib.Analysis.CStarAlgebra.Hom` `Mathlib.Analysis.Complex.Polynomial.UnitTrinomial` `Mathlib.Geometry.Manifold.PartitionOfUnity` `Mathlib.Geometry.Manifold.MFDeriv.Atlas` `Mathlib.NumberTheory.LSeries.HurwitzZetaOdd` `Mathlib.RingTheory.FractionalIdeal.Operations` `Mathlib.Analysis.Complex.Hadamard` `Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts` `Mathlib.Geometry.Manifold.Algebra.LieGroup` `Mathlib.Combinatorics.SimpleGraph.LapMatrix` `Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange` `Mathlib.Combinatorics.SimpleGraph.Regularity.Bound` `Mathlib.Analysis.Calculus.ContDiff.CPolynomial` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order` `Mathlib.NumberTheory.Transcendental.Liouville.Basic` `Mathlib.Probability.Distributions.Pareto` `Mathlib.RingTheory.PowerSeries.Order` `Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv` `Mathlib.Analysis.Calculus.Rademacher` `Mathlib.Analysis.Calculus.BumpFunction.InnerProduct` `Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace` `Mathlib.LinearAlgebra.Matrix.Spectrum` `Mathlib.RingTheory.LocalProperties.Basic` `Mathlib.NumberTheory.NumberField.House` `Mathlib.NumberTheory.NumberField.Embeddings` `Mathlib.NumberTheory.Harmonic.Bounds` `Mathlib.NumberTheory.Bernoulli` `Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ` `Mathlib.Geometry.Manifold.AnalyticManifold` `Mathlib.Analysis.MellinTransform` `Mathlib.RingTheory.LocalRing.RingHom.Basic` `Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar` `Mathlib.Analysis.Analytic.IsolatedZeros` `Mathlib.MeasureTheory.Integral.Gamma` `Mathlib.Geometry.Manifold.ContMDiff.NormedSpace` `Mathlib.Analysis.Convex.SpecificFunctions.Deriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd` `Mathlib.Analysis.Calculus.FDeriv.Symmetric` `Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv` `Mathlib.NumberTheory.LSeries.PrimesInAP` `Mathlib.Analysis.Analytic.Inverse` `Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma` `Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation` `Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension` `Mathlib.RingTheory.MaximalSpectrum` `Mathlib.Probability.Distributions.Gamma` `Mathlib.Analysis.SpecialFunctions.ExpDeriv` `Mathlib.RingTheory.FiniteType` `Mathlib.Geometry.Manifold.DerivationBundle` `Mathlib.Analysis.Complex.RealDeriv` `Mathlib.Analysis.Complex.OpenMapping` `Mathlib.Analysis.Calculus.BumpFunction.Normed` `Mathlib.Geometry.Manifold.IntegralCurve.Transform` `Mathlib.Analysis.ODE.PicardLindelof` `Mathlib.NumberTheory.NumberField.ClassNumber` `Mathlib.Analysis.Calculus.LogDeriv` `Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv` `Mathlib.Algebra.CharP.MixedCharZero` `Mathlib.Geometry.Manifold.LocalDiffeomorph` `Mathlib.RingTheory.RingHom.Surjective` `Mathlib.NumberTheory.LSeries.HurwitzZeta` `Mathlib.Tactic` `Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform` `Mathlib.FieldTheory.RatFunc.Basic` `Mathlib.RingTheory.Support` `Mathlib.Analysis.Distribution.SchwartzSpace` `Mathlib.NumberTheory.Bertrand` `Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber` `Mathlib.Analysis.SpecialFunctions.Gamma.Deriv` `Mathlib.Geometry.Manifold.Metrizable` `Mathlib.Analysis.Calculus.LocalExtr.LineDeriv` `Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic` `Mathlib.Analysis.SpecialFunctions.Pow.Integral` `Mathlib.Geometry.Manifold.WhitneyEmbedding` `Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Series` `Mathlib.NumberTheory.FLT.MasonStothers` `Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus` `Mathlib.Analysis.Complex.AbelLimit` `Mathlib.Analysis.SpecialFunctions.Sqrt` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic` `Mathlib.Data.Real.Pi.Wallis` `Mathlib.NumberTheory.LSeries.AbstractFuncEq` `Mathlib.NumberTheory.EulerProduct.ExpLog` `Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique` `Mathlib.RingTheory.LocalProperties.Projective` `Mathlib.Data.Complex.ExponentialBounds` `Mathlib.NumberTheory.NumberField.AdeleRing` `Mathlib.RingTheory.PowerSeries.Inverse` `Mathlib.Analysis.Calculus.ContDiff.WithLp` `Mathlib.NumberTheory.ModularForms.QExpansion` `Mathlib.Geometry.Manifold.Instances.Sphere` `Mathlib.Geometry.Manifold.VectorBundle.SmoothSection` `Mathlib.Geometry.Manifold.ContMDiff.Product`	-2
425 files `Mathlib.Topology.Category.Stonean.Adjunctions` `Mathlib.Data.Real.Hyperreal` `Mathlib.Topology.Algebra.Module.Simple` `Mathlib.Analysis.Asymptotics.SpecificAsymptotics` `Mathlib.Topology.Category.LightProfinite.EffectiveEpi` `Mathlib.MeasureTheory.Constructions.BorelSpace.Metric` `Mathlib.Probability.Kernel.Defs` `Mathlib.Topology.Category.Stonean.EffectiveEpi` `Mathlib.Analysis.NormedSpace.OperatorNorm.Basic` `Mathlib.RingTheory.SimpleModule` `Mathlib.Topology.MetricSpace.Thickening` `Mathlib.Probability.Distributions.Geometric` `Mathlib.Analysis.Subadditive` `Mathlib.MeasureTheory.Integral.Marginal` `Mathlib.Topology.Category.CompHaus.EffectiveEpi` `Mathlib.Topology.ContinuousMap.Bounded.Basic` `Mathlib.Topology.Homotopy.Contractible` `Mathlib.LinearAlgebra.Matrix.MvPolynomial` `Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit` `Mathlib.Topology.Algebra.Module.UniformConvergence` `Mathlib.LinearAlgebra.Dimension.DivisionRing` `Mathlib.Topology.Category.Profinite.CofilteredLimit` `Mathlib.Condensed.Limits` `Mathlib.MeasureTheory.OuterMeasure.Caratheodory` `Mathlib.MeasureTheory.Constructions.BorelSpace.Basic` `Mathlib.Probability.ProbabilityMassFunction.Monad` `Mathlib.MeasureTheory.OuterMeasure.Induced` `Mathlib.MeasureTheory.Measure.Regular` `Mathlib.Analysis.Asymptotics.AsymptoticEquivalent` `Mathlib.MeasureTheory.Group.MeasurableEquiv` `Mathlib.RingTheory.Flat.Basic` `Mathlib.MeasureTheory.Order.Lattice` `Mathlib.Condensed.TopComparison` `Mathlib.Analysis.Hofer` `Mathlib.LinearAlgebra.Dimension.Localization` `Mathlib.Analysis.CStarAlgebra.ContinuousMap` `Mathlib.Analysis.Normed.Algebra.Ultra` `Mathlib.Analysis.Convex.Topology` `Mathlib.Condensed.Discrete.Basic` `Mathlib.LinearAlgebra.Matrix.Diagonal` `Mathlib.Analysis.Complex.HalfPlane` `Mathlib.Analysis.LocallyConvex.Bounded` `Mathlib.LinearAlgebra.Eigenspace.Matrix` `Mathlib.Analysis.Seminorm` `Mathlib.MeasureTheory.Measure.AEDisjoint` `Mathlib.CategoryTheory.Sites.SheafCohomology.Basic` `Mathlib.Topology.Instances.CantorSet` `Mathlib.Topology.Bornology.BoundedOperation` `Mathlib.Analysis.Convex.Body` `Mathlib.Topology.Category.Profinite.Nobeling` `Mathlib.Analysis.NormedSpace.RCLike` `Mathlib.Condensed.Light.Explicit` `Mathlib.Topology.Compactification.OnePointEquiv` `Mathlib.Data.Real.Sqrt` `Mathlib.Topology.Category.LightProfinite.Extend` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev` `Mathlib.NumberTheory.FLT.Four` `Mathlib.Topology.Instances.ZMultiples` `Mathlib.Analysis.Calculus.FormalMultilinearSeries` `Mathlib.MeasureTheory.Order.Group.Lattice` `Mathlib.Topology.Germ` `Mathlib.Topology.Algebra.InfiniteSum.ENNReal` `Mathlib.MeasureTheory.Group.Measure` `Mathlib.NumberTheory.Zsqrtd.ToReal` `Mathlib.Condensed.Explicit` `Mathlib.Topology.ContinuousMap.Periodic` `Mathlib.Condensed.Module` `Mathlib.Condensed.Discrete.Characterization` `Mathlib.Condensed.Light.CartesianClosed` `Mathlib.Analysis.NormedSpace.RieszLemma` `Mathlib.Data.ZMod.Quotient` `Mathlib.MeasureTheory.OuterMeasure.OfFunction` `Mathlib.Topology.MetricSpace.PartitionOfUnity` `Mathlib.MeasureTheory.Covering.VitaliFamily` `Mathlib.Analysis.LocallyConvex.Barrelled` `Mathlib.NumberTheory.Padics.PadicNumbers` `Mathlib.MeasureTheory.Measure.ContinuousPreimage` `Mathlib.MeasureTheory.Group.Arithmetic` `Mathlib.Dynamics.Ergodic.MeasurePreserving` `Mathlib.GroupTheory.Nilpotent` `Mathlib.RingTheory.WittVector.WittPolynomial` `Mathlib.Analysis.Complex.Basic` `Mathlib.MeasureTheory.Function.AEMeasurableOrder` `Mathlib.MeasureTheory.Category.MeasCat` `Mathlib.Analysis.Calculus.TangentCone` `Mathlib.Topology.Category.Profinite.EffectiveEpi` `Mathlib.RingTheory.Regular.IsSMulRegular` `Mathlib.MeasureTheory.Constructions.Pi` `Mathlib.Analysis.Normed.Order.UpperLower` `Mathlib.Topology.MetricSpace.GromovHausdorffRealized` `Mathlib.Topology.ContinuousMap.Bounded.Star` `Mathlib.MeasureTheory.Decomposition.UnsignedHahn` `Mathlib.RingTheory.Flat.Localization` `Mathlib.Topology.ContinuousMap.Compact` `Mathlib.Analysis.Normed.Algebra.Unitization` `Mathlib.GroupTheory.SchurZassenhaus` `Mathlib.Analysis.Calculus.FDeriv.Basic` `Mathlib.Dynamics.Ergodic.Conservative` `Mathlib.Topology.UniformSpace.CompareReals` `Mathlib.Analysis.BoxIntegral.Box.SubboxInduction` `Mathlib.Topology.Instances.AddCircle` `Mathlib.Analysis.Normed.Affine.Isometry` `Mathlib.Topology.Category.Profinite.AsLimit` `Mathlib.Topology.Order.Bounded` `Mathlib.Topology.Homotopy.Path` `Mathlib.Algebra.Category.ModuleCat.Simple` `Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable` `Mathlib.Algebra.Category.Grp.EnoughInjectives` `Mathlib.Data.ZMod.Coprime` `Mathlib.Topology.CompletelyRegular` `Mathlib.Data.Complex.Exponential` `Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected` `Mathlib.Condensed.Basic` `Mathlib.MeasureTheory.Measure.NullMeasurable` `Mathlib.Topology.ContinuousMap.BoundedCompactlySupported` `Mathlib.Analysis.Normed.Operator.BanachSteinhaus` `Mathlib.AlgebraicTopology.FundamentalGroupoid.Product` `Mathlib.Condensed.Light.TopComparison` `Mathlib.Condensed.Light.TopCatAdjunction` `Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear` `Mathlib.Condensed.Discrete.LocallyConstant` `Mathlib.Analysis.LocallyConvex.Basic` `Mathlib.Analysis.Normed.Ring.WithAbs` `Mathlib.Analysis.LocallyConvex.WeakDual` `Mathlib.Analysis.Normed.Module.Span` `Mathlib.Analysis.Normed.Affine.MazurUlam` `Mathlib.MeasureTheory.Measure.Content` `Mathlib.LinearAlgebra.FiniteDimensional` `Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup` `Mathlib.Topology.Homotopy.Basic` `Mathlib.LinearAlgebra.FreeModule.Int` `Mathlib.Analysis.LocallyConvex.AbsConvex` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels` `Mathlib.Topology.UrysohnsBounded` `Mathlib.MeasureTheory.Decomposition.Exhaustion` `Mathlib.MeasureTheory.Measure.Sub` `Mathlib.Topology.Homotopy.Product` `Mathlib.Topology.Instances.Real` `Mathlib.Topology.Metrizable.Urysohn` `Mathlib.MeasureTheory.Measure.HasOuterApproxClosed` `Mathlib.Analysis.Normed.Group.Tannery` `Mathlib.MeasureTheory.Measure.GiryMonad` `Mathlib.RingTheory.Flat.Algebra` `Mathlib.Probability.ProbabilityMassFunction.Constructions` `Mathlib.RingTheory.Flat.CategoryTheory` `Mathlib.Condensed.Solid` `Mathlib.Algebra.Category.ModuleCat.EnoughInjectives` `Mathlib.Topology.Category.LightProfinite.AsLimit` `Mathlib.Condensed.Discrete.Module` `Mathlib.Topology.Category.LightProfinite.Limits` `Mathlib.Analysis.NormedSpace.OperatorNorm.Mul` `Mathlib.Analysis.Normed.Group.Quotient` `Mathlib.Topology.Category.CompHaus.Basic` `Mathlib.Order.Filter.ZeroAndBoundedAtFilter` `Mathlib.AlgebraicTopology.SingularSet` `Mathlib.Analysis.Asymptotics.TVS` `Mathlib.LinearAlgebra.FiniteDimensional.Defs` `Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic` `Mathlib.Topology.Algebra.Module.Alternating.Topology` `Mathlib.Topology.Category.CompHaus.Projective` `Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace` `Mathlib.MeasureTheory.Measure.Trim` `Mathlib.Analysis.Normed.Group.Completeness` `Mathlib.Analysis.CStarAlgebra.Classes` `Mathlib.Analysis.Normed.Group.ZeroAtInfty` `Mathlib.Analysis.LocallyConvex.StrongTopology` `Mathlib.NumberTheory.PythagoreanTriples` `Mathlib.LinearAlgebra.Projectivization.Constructions` `Mathlib.Analysis.NormedSpace.ConformalLinearMap` `Mathlib.MeasureTheory.Decomposition.Jordan` `Mathlib.Condensed.Light.Epi` `Mathlib.Analysis.BoxIntegral.Partition.Additive` `Mathlib.Analysis.Complex.ReImTopology` `Mathlib.RingTheory.ZMod` `Mathlib.Analysis.Calculus.Deriv.Basic` `Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics` `Mathlib.Topology.Category.Profinite.Projective` `Mathlib.Topology.PartitionOfUnity` `Mathlib.Analysis.NormedSpace.Multilinear.Curry` `Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences` `Mathlib.Analysis.SumOverResidueClass` `Mathlib.Topology.TietzeExtension` `Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal` `Mathlib.Topology.MetricSpace.Polish` `Mathlib.GroupTheory.CosetCover` `Mathlib.LinearAlgebra.LinearDisjoint` `Mathlib.Analysis.CStarAlgebra.Unitization` `Mathlib.Topology.Category.Profinite.Basic` `Mathlib.LinearAlgebra.Dimension.Torsion` `Mathlib.MeasureTheory.Group.LIntegral` `Mathlib.Topology.Instances.Rat` `Mathlib.AlgebraicTopology.TopologicalSimplex` `Mathlib.MeasureTheory.Integral.LebesgueNormedSpace` `Mathlib.Probability.ProbabilityMassFunction.Binomial` `Mathlib.Topology.ContinuousMap.StarOrdered` `Mathlib.GroupTheory.Torsion` `Mathlib.Analysis.Convex.Between` `Mathlib.MeasureTheory.Group.Pointwise` `Mathlib.Analysis.Normed.Group.HomCompletion` `Mathlib.Topology.Category.CompHaus.Limits` `Mathlib.Topology.Algebra.Module.LocallyConvex` `Mathlib.Algebra.Star.CHSH` `Mathlib.Condensed.TopCatAdjunction` `Mathlib.RingTheory.Flat.FaithfullyFlat` `Mathlib.LinearAlgebra.Projectivization.Independence` `Mathlib.Analysis.Complex.Asymptotics` `Mathlib.Probability.ConditionalProbability` `Mathlib.Order.Filter.ENNReal` `Mathlib.Analysis.Normed.Field.UnitBall` `Mathlib.Analysis.Normed.Group.Completion` `Mathlib.Data.Complex.FiniteDimensional` `Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes` `Mathlib.MeasureTheory.Integral.RieszMarkovKakutani` `Mathlib.Analysis.Calculus.FDeriv.RestrictScalars` `Mathlib.GroupTheory.Complement` `Mathlib.Analysis.NormedSpace.Extr` `Mathlib.FieldTheory.Finiteness` `Mathlib.Topology.UnitInterval` `Mathlib.Topology.UrysohnsLemma` `Mathlib.Topology.Category.CompactlyGenerated` `Mathlib.MeasureTheory.Constructions.BorelSpace.Complex` `Mathlib.Topology.Homotopy.HomotopyGroup` `Mathlib.Data.Real.StarOrdered` `Mathlib.Analysis.Normed.Order.Basic` `Mathlib.MeasureTheory.Measure.Count` `Mathlib.Probability.Kernel.Basic` `Mathlib.GroupTheory.Perm.Finite` `Mathlib.MeasureTheory.Group.AEStabilizer` `Mathlib.GroupTheory.SpecificGroups.Quaternion` `Mathlib.Topology.Algebra.Module.StrongTopology` `Mathlib.Analysis.Convex.EGauge` `Mathlib.Topology.MetricSpace.ThickenedIndicator` `Mathlib.MeasureTheory.Measure.Comap` `Mathlib.Probability.ProbabilityMassFunction.Basic` `Mathlib.LinearAlgebra.TensorProduct.Graded.External` `Mathlib.Topology.MetricSpace.Contracting` `Mathlib.Data.Complex.Cardinality` `Mathlib.Topology.Baire.BaireMeasurable` `Mathlib.LinearAlgebra.Eigenspace.Basic` `Mathlib.Analysis.NormedSpace.Int` `Mathlib.Analysis.RCLike.Basic` `Mathlib.Analysis.Normed.Operator.Banach` `Mathlib.Algebra.Module.CharacterModule` `Mathlib.Algebra.Module.Torsion` `Mathlib.Analysis.Normed.Group.AddCircle` `Mathlib.Topology.Instances.Complex` `Mathlib.Analysis.Convex.Contractible` `Mathlib.MeasureTheory.Group.Convolution` `Mathlib.Analysis.BoxIntegral.Partition.Filter` `Mathlib.Topology.MetricSpace.Perfect` `Mathlib.Topology.Connected.PathConnected` `Mathlib.Dynamics.Ergodic.Ergodic` `Mathlib.Analysis.NormedSpace.ENorm` `Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional` `Mathlib.Analysis.Normed.Field.ProperSpace` `Mathlib.Analysis.CStarAlgebra.Basic` `Mathlib.MeasureTheory.Measure.OpenPos` `Mathlib.MeasureTheory.Measure.Dirac` `Mathlib.MeasureTheory.Decomposition.SignedHahn` `Mathlib.Topology.Category.Compactum` `Mathlib.Analysis.Normed.Group.InfiniteSum` `Mathlib.Analysis.Calculus.Deriv.Comp` `Mathlib.Analysis.Normed.Affine.AddTorsor` `Mathlib.Condensed.Light.Limits` `Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps` `Mathlib.GroupTheory.Transfer` `Mathlib.Condensed.Discrete.Colimit` `Mathlib.Topology.MetricSpace.PiNat` `Mathlib.Analysis.NormedSpace.HomeomorphBall` `Mathlib.Topology.Category.Profinite.Extend` `Mathlib.Analysis.Normed.Group.Lemmas` `Mathlib.MeasureTheory.Measure.Stieltjes` `Mathlib.Condensed.CartesianClosed` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn` `Mathlib.Dynamics.Ergodic.Action.Regular` `Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic` `Mathlib.Topology.Compactness.CompactlyGeneratedSpace` `Mathlib.Topology.Category.Stonean.Basic` `Mathlib.Topology.ContinuousMap.ContinuousMapZero` `Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm` `Mathlib.Topology.Instances.EReal` `Mathlib.Topology.Algebra.Module.Multilinear.Bounded` `Mathlib.Topology.MetricSpace.HausdorffDistance` `Mathlib.Analysis.Convex.TotallyBounded` `Mathlib.Data.Complex.Order` `Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous` `Mathlib.GroupTheory.Sylow` `Mathlib.Analysis.NormedSpace.Extend` `Mathlib.Analysis.Asymptotics.Theta` `Mathlib.MeasureTheory.Function.Egorov` `Mathlib.Probability.Independence.Basic` `Mathlib.Topology.Category.LightProfinite.Basic` `Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction` `Mathlib.LinearAlgebra.Dimension.LinearMap` `Mathlib.Topology.MetricSpace.CantorScheme` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion` `Mathlib.Algebra.CharP.Quotient` `Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm` `Mathlib.MeasureTheory.Covering.Vitali` `Mathlib.RingTheory.Flat.EquationalCriterion` `Mathlib.Analysis.Convex.Gauge` `Mathlib.MeasureTheory.VectorMeasure.Basic` `Mathlib.Topology.Category.LightProfinite.Sequence` `Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness` `Mathlib.Condensed.Light.Basic` `Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition` `Mathlib.Analysis.Calculus.Deriv.Support` `Mathlib.MeasureTheory.Constructions.Polish.Basic` `Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber` `Mathlib.Condensed.Light.Module` `Mathlib.Data.Real.Cardinality` `Mathlib.GroupTheory.PushoutI` `Mathlib.Dynamics.Ergodic.Function` `Mathlib.Analysis.Normed.Module.Basic` `Mathlib.Analysis.Complex.Convex` `Mathlib.Topology.Separation.NotNormal` `Mathlib.Topology.Category.Locale` `Mathlib.Analysis.Normed.Group.Pointwise` `Mathlib.MeasureTheory.OuterMeasure.Defs` `Mathlib.LinearAlgebra.Matrix.Basis` `Mathlib.GroupTheory.HNNExtension` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic` `Mathlib.Analysis.Calculus.FDeriv.Comp` `Mathlib.Topology.Instances.RealVectorSpace` `Mathlib.Analysis.LocallyConvex.ContinuousOfBounded` `Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm` `Mathlib.MeasureTheory.Measure.Restrict` `Mathlib.Analysis.LocallyConvex.WithSeminorms` `Mathlib.Analysis.Asymptotics.SuperpolynomialDecay` `Mathlib.Analysis.Normed.Order.Lattice` `Mathlib.Analysis.Normed.Module.Ray` `Mathlib.MeasureTheory.Measure.MutuallySingular` `Mathlib.Analysis.Convex.Visible` `Mathlib.Probability.Independence.Kernel` `Mathlib.MeasureTheory.Group.Prod` `Mathlib.Order.Category.Frm` `Mathlib.Analysis.NormedSpace.OperatorNorm.Prod` `Mathlib.Topology.ContinuousMap.CompactlySupported` `Mathlib.GroupTheory.SpecificGroups.Cyclic` `Mathlib.Condensed.Epi` `Mathlib.Topology.Maps.Proper.CompactlyGenerated` `Mathlib.MeasureTheory.Measure.Typeclasses` `Mathlib.RingTheory.Flat.Equalizer` `Mathlib.Analysis.NormedSpace.Real` `Mathlib.MeasureTheory.OuterMeasure.Operations` `Mathlib.MeasureTheory.Measure.Prod` `Mathlib.Analysis.Normed.Field.Lemmas` `Mathlib.Analysis.Normed.Field.InfiniteSum` `Mathlib.Topology.Algebra.Module.Multilinear.Topology` `Mathlib.Condensed.Light.Functors` `Mathlib.MeasureTheory.Measure.AEMeasurable` `Mathlib.Analysis.Asymptotics.Asymptotics` `Mathlib.MeasureTheory.Measure.WithDensity` `Mathlib.MeasureTheory.Function.AEEqFun` `Mathlib.MeasureTheory.Function.SimpleFuncDense` `Mathlib.Data.Complex.Abs` `Mathlib.Topology.ContinuousMap.ZeroAtInfty` `Mathlib.Analysis.NormedSpace.FunctionSeries` `Mathlib.Analysis.Normed.Operator.Compact` `Mathlib.GroupTheory.SpecificGroups.KleinFour` `Mathlib.Dynamics.Ergodic.Action.Basic` `Mathlib.RingTheory.Flat.Stability` `Mathlib.Condensed.Functors` `Mathlib.MeasureTheory.Constructions.Projective` `Mathlib.Analysis.NormedSpace.BallAction` `Mathlib.MeasureTheory.Measure.MeasureSpace` `Mathlib.MeasureTheory.Measure.MeasureSpaceDef` `Mathlib.MeasureTheory.Group.Action` `Mathlib.Dynamics.BirkhoffSum.NormedSpace` `Mathlib.LinearAlgebra.Projectivization.Subspace` `Mathlib.MeasureTheory.OuterMeasure.Basic` `Mathlib.MeasureTheory.Function.AEMeasurableSequence` `Mathlib.Condensed.Equivalence` `Mathlib.Topology.Homotopy.Equiv` `Mathlib.Topology.Category.Profinite.Product` `Mathlib.Topology.Homotopy.HSpaces` `Mathlib.Topology.Category.Profinite.Limits` `Mathlib.Topology.MetricSpace.Completion` `Mathlib.Topology.Instances.NNReal` `Mathlib.MeasureTheory.Measure.Haar.Basic` `Mathlib.Analysis.Calculus.Deriv.Slope` `Mathlib.Analysis.SpecificLimits.RCLike` `Mathlib.GroupTheory.Frattini` `Mathlib.Analysis.NormedSpace.Multilinear.Basic` `Mathlib.MeasureTheory.Constructions.BorelSpace.Real` `Mathlib.GroupTheory.PGroup` `Mathlib.LinearAlgebra.TensorProduct.Graded.Internal` `Mathlib.LinearAlgebra.Dimension.Finite` `Mathlib.Analysis.LocallyConvex.BalancedCoreHull` `Mathlib.Algebra.Category.Grp.Injective` `Mathlib.MeasureTheory.Constructions.BorelSpace.Order` `Mathlib.MeasureTheory.Integral.Indicator` `Mathlib.Topology.Algebra.InfiniteSum.Real` `Mathlib.Analysis.Normed.Group.Rat` `Mathlib.Topology.MetricSpace.Closeds` `Mathlib.Analysis.Convex.Radon` `Mathlib.Analysis.Normed.Affine.ContinuousAffineMap` `Mathlib.Topology.Semicontinuous` `Mathlib.MeasureTheory.Measure.EverywherePos` `Mathlib.RepresentationTheory.Maschke` `Mathlib.Analysis.SpecificLimits.Basic` `Mathlib.MeasureTheory.Function.EssSup` `Mathlib.MeasureTheory.OuterMeasure.AE` `Mathlib.GroupTheory.Schreier` `Mathlib.MeasureTheory.Measure.Complex` `Mathlib.CategoryTheory.Triangulated.Yoneda` `Mathlib.MeasureTheory.Function.Floor` `Mathlib.LinearAlgebra.Dimension.RankNullity` `Mathlib.Analysis.NormedSpace.SphereNormEquiv` `Mathlib.Topology.Order.Category.FrameAdjunction` `Mathlib.Probability.UniformOn` `Mathlib.Analysis.Convex.PartitionOfUnity` `Mathlib.Analysis.NormedSpace.Pointwise` `Mathlib.MeasureTheory.Integral.Lebesgue` `Mathlib.Analysis.SpecialFunctions.Log.ERealExp` `Mathlib.Topology.Baire.CompleteMetrizable` `Mathlib.MeasureTheory.Function.SimpleFunc` `Mathlib.MeasureTheory.Group.Defs` `Mathlib.Analysis.Normed.Module.Completion` `Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps` `Mathlib.GroupTheory.SpecificGroups.ZGroup` `Mathlib.Topology.Instances.ENNReal` `Mathlib.Topology.Category.Stonean.Limits` `Mathlib.LinearAlgebra.Projectivization.Basic` `Mathlib.MeasureTheory.OuterMeasure.BorelCantelli`	-1
30 files `Mathlib.GroupTheory.Perm.Cycle.PossibleTypes` `Mathlib.Data.Matrix.DoublyStochastic` `Mathlib.Analysis.Convex.Birkhoff` `Mathlib.LinearAlgebra.Matrix.Reindex` `Mathlib.NumberTheory.MulChar.Basic` `Mathlib.GroupTheory.Exponent` `Mathlib.LinearAlgebra.Matrix.Determinant.Misc` `Mathlib.GroupTheory.CommutingProbability` `Mathlib.GroupTheory.Perm.Fin` `Mathlib.NumberTheory.DirichletCharacter.Basic` `Mathlib.GroupTheory.GroupAction.Period` `Mathlib.SetTheory.Nimber.Field` `Mathlib.LinearAlgebra.CrossProduct` `Mathlib.LinearAlgebra.Matrix.Permutation` `Mathlib.GroupTheory.FixedPointFree` `Mathlib.LinearAlgebra.Matrix.AbsoluteValue` `Mathlib.NumberTheory.LegendreSymbol.ZModChar` `Mathlib.GroupTheory.Perm.Cycle.Concrete` `Mathlib.Data.ZMod.Factorial` `Mathlib.GroupTheory.Coxeter.Inversion` `Mathlib.NumberTheory.PrimeCounting` `Mathlib.GroupTheory.SpecificGroups.Alternating` `Mathlib.GroupTheory.Coxeter.Length` `Mathlib.LinearAlgebra.Matrix.Transvection` `Mathlib.Algebra.CharP.Two` `Mathlib.GroupTheory.SpecificGroups.Dihedral` `Mathlib.Algebra.CharP.CharAndCard` `Mathlib.LinearAlgebra.Matrix.Determinant.Basic` `Mathlib.GroupTheory.Perm.Cycle.Type` `Mathlib.Data.Nat.Totient`	1
52 files `Mathlib.Algebra.Periodic` `Mathlib.Algebra.Homology.DerivedCategory.HomologySequence` `Mathlib.Algebra.Homology.TotalComplexSymmetry` `Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated` `Mathlib.CategoryTheory.Triangulated.Pretriangulated` `Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic` `Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift` `Mathlib.Algebra.Homology.HomotopyCategory.MappingCone` `Mathlib.Algebra.Homology.BifunctorFlip` `Mathlib.Algebra.Homology.TotalComplexShift` `Mathlib.Algebra.Order.ToIntervalMod` `Mathlib.Data.Nat.Periodic` `Mathlib.CategoryTheory.Triangulated.Triangulated` `Mathlib.CategoryTheory.Triangulated.HomologicalFunctor` `Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor` `Mathlib.Data.ZMod.IntUnitsPower` `Mathlib.CategoryTheory.Shift.ShiftedHomOpposite` `Mathlib.Algebra.Homology.HomotopyCategory.Triangulated` `Mathlib.Algebra.Homology.BifunctorAssociator` `Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors` `Mathlib.Algebra.Homology.HomotopyCategory.HomComplex` `Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle` `Mathlib.Algebra.Homology.DerivedCategory.ShortExact` `Mathlib.Algebra.Homology.HomotopyCategory.Shift` `Mathlib.Data.ZMod.Basic` `Mathlib.Algebra.Homology.Monoidal` `Mathlib.CategoryTheory.Localization.Triangulated` `Mathlib.CategoryTheory.Triangulated.Opposite` `Mathlib.Algebra.Homology.ComplexShapeSigns` `Mathlib.Data.ZMod.Units` `Mathlib.Algebra.Homology.BifunctorHomotopy` `Mathlib.CategoryTheory.Triangulated.TriangleShift` `Mathlib.Algebra.Homology.TotalComplex` `Mathlib.Combinatorics.SimpleGraph.DegreeSum` `Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence` `Mathlib.NumberTheory.LucasLehmer` `Mathlib.Algebra.Algebra.ZMod` `Mathlib.Algebra.Module.ZMod` `Mathlib.RingTheory.Fintype` `Mathlib.Algebra.Homology.HomotopyCategory.ShortExact` `Mathlib.CategoryTheory.Triangulated.Subcategory` `Mathlib.CategoryTheory.Triangulated.Functor` `Mathlib.CategoryTheory.Triangulated.TStructure.Basic` `Mathlib.Algebra.Homology.Bifunctor` `Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit` `Mathlib.Algebra.Ring.NegOnePow` `Mathlib.Algebra.Homology.BifunctorShift` `Mathlib.Combinatorics.SimpleGraph.Matching` `Mathlib.Algebra.Homology.DerivedCategory.Basic` `Mathlib.Data.ZMod.Aut` `Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor` `Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass`	4
`Mathlib.Deprecated.Cardinal.PartENat`	750
`Mathlib.Deprecated.Cardinal.Finite` (new file)	759
`Mathlib.Deprecated.Cardinal.Continuum` (new file)	783

Declarations diff

+ add_lt_top
+ aleph_toENat
+ coe_inj
+ coe_le_coe
+ coe_lift
+ coe_lt_coe
+ continuum_toENat
+ forall_coeff_eq_zero
+ le_lift_iff
+ lift
+ lift_add
+ lift_coe
+ lift_le_iff
+ lift_lt_iff
+ lift_ofNat
+ lift_one
+ lift_zero
+ lt_lift_iff

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) = (3.08, 0.20)

Current number	Change	Type
55	-1	disabled deprecation lints
21	3	`Deprecated` files
3102	245	total LoC in `Deprecated` files

Current commit 5b4febff9e
Reference commit a1f01bd5d1

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).

mathlib4-dependent-issues-bot · 2024-12-01T11:31:51Z

This PR/issue depends on:

~~[Merged by Bors] - chore: remove PartENat from PowerSeries #19622~~
By Dependent Issues (🤖). Happy coding!

grunweg · 2024-12-01T12:31:58Z

Per zulip: I think it would be good to only land this after the release. (Unless I'm misunderstanding something.)

jcommelin · 2024-12-03T05:50:20Z

Per zulip: I think we're ready to merge this now.

bors merge

- [x] depends on: #19622 (perhaps unnecessarily)

mathlib-bors · 2024-12-03T06:18:08Z

Pull request successfully merged into master.

Build succeeded:

kim-em added 5 commits November 30, 2024 17:33

chore: start removing PartENat from PowerSeries

23fbaf4

finish

bed9cdb

fix

0303f34

.

838fe55

.

74b1255

kim-em added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Dec 1, 2024

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 1, 2024

kim-em added 3 commits December 1, 2024 14:44

lint

8f51556

Merge branch 'powerseries_enat' into rm_PartENat

37b6daa

fix

5b4febf

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Dec 1, 2024

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Dec 1, 2024

ghost added the ready-to-merge This PR has been sent to bors. label Dec 3, 2024

mathlib-bors bot pushed a commit that referenced this pull request Dec 3, 2024

chore: complete deprecation of PartENat.card (#19648)

72b0941

- [x] depends on: #19622 (perhaps unnecessarily)

mathlib-bors bot changed the title ~~chore: complete deprecation of PartENat.card~~ [Merged by Bors] - chore: complete deprecation of PartENat.card Dec 3, 2024

mathlib-bors bot closed this Dec 3, 2024

mathlib-bors bot deleted the rm_PartENat branch December 3, 2024 06:18

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore: complete deprecation of `PartENat.card`#19648

[Merged by Bors] - chore: complete deprecation of `PartENat.card`#19648
kim-em wants to merge 8 commits intomasterfrom
rm_PartENat

kim-em commented Dec 1, 2024 •

edited by riccardobrasca

Loading

Uh oh!

github-actions bot commented Dec 1, 2024 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Dec 1, 2024

Uh oh!

grunweg commented Dec 1, 2024

Uh oh!

jcommelin commented Dec 3, 2024

Uh oh!

mathlib-bors bot commented Dec 3, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

kim-em commented Dec 1, 2024 • edited by riccardobrasca Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Dec 1, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 5b4febff9e

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Dec 1, 2024

Uh oh!

grunweg commented Dec 1, 2024

Uh oh!

jcommelin commented Dec 3, 2024

Uh oh!

mathlib-bors bot commented Dec 3, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

kim-em commented Dec 1, 2024 •

edited by riccardobrasca

Loading

github-actions bot commented Dec 1, 2024 •

edited

Loading