Conversation
PR summary 0181c1ed7b
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Algebra.IsPrimePow | 604 | 440 | -164 (-27.15%) |
| Mathlib.NumberTheory.Divisors | 603 | 604 | +1 (+0.17%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Algebra.IsPrimePow |
-164 |
Mathlib.SetTheory.Cardinal.Divisibility |
-20 |
Mathlib.RingTheory.ChainOfDivisors |
-15 |
12 filesMathlib.NumberTheory.RamificationInertia.Basic Mathlib.FieldTheory.Laurent Mathlib.RingTheory.DedekindDomain.Ideal Mathlib.RingTheory.ClassGroup Mathlib.RingTheory.LaurentSeries Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.FieldTheory.RatFunc.Degree |
-5 |
4 filesMathlib.AlgebraicGeometry.EllipticCurve.Group Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic Mathlib.NumberTheory.KummerDedekind Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree |
-4 |
Mathlib.Algebra.CharP.LocalRing Mathlib.Algebra.CharP.MixedCharZero |
-1 |
650 filesMathlib.NumberTheory.NumberField.Discriminant.Defs Mathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.Analysis.MeanInequalitiesPow Mathlib.Combinatorics.Additive.ErdosGinzburgZiv Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Analysis.BoxIntegral.UnitPartition Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Probability.Process.HittingTime Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.FieldTheory.IsPerfectClosure Mathlib.NumberTheory.Padics.PadicNorm Mathlib.Probability.BorelCantelli Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.NumberTheory.Wilson Mathlib.Dynamics.TopologicalEntropy.NetEntropy Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.FieldTheory.Finite.Trace Mathlib.NumberTheory.Padics.MahlerBasis Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.Probability.Variance Mathlib.Analysis.Complex.Angle Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.Analysis.SpecialFunctions.Integrals Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.Fourier.PoissonSummation Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.LinearAlgebra.ExteriorAlgebra.Grading Mathlib.NumberTheory.MulChar.Lemmas Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.CStarAlgebra.Multiplier Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.Analysis.SpecialFunctions.Pow.Complex Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.MeasureTheory.Function.SpecialFunctions.Basic Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Normed.Lp.PiLp Mathlib.RingTheory.WittVector.Domain Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.MeasureTheory.Function.UnifTight Mathlib.Analysis.SpecialFunctions.CompareExp Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.MeasureTheory.Function.LpSeminorm.Basic Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.Analysis.SpecialFunctions.Complex.Log Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.Analysis.Calculus.FDeriv.WithLp Mathlib.Analysis.Complex.AbsMax Mathlib.RingTheory.Flat.Basic Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.RingTheory.WittVector.InitTail Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Geometry.Manifold.Instances.Real Mathlib.RingTheory.Localization.NormTrace Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.Geometry.Manifold.Complex Mathlib.FieldTheory.AbelRuffini Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.Probability.StrongLaw Mathlib.RingTheory.Regular.RegularSequence Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.RingTheory.TensorProduct.Nontrivial Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Probability.Kernel.Composition.MeasureCompProd Mathlib.RingTheory.Trace.Defs Mathlib.RingTheory.WittVector.Compare Mathlib.Probability.Kernel.Composition.IntegralCompProd Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.Analysis.Complex.Isometry Mathlib.MeasureTheory.Function.L2Space Mathlib.AlgebraicGeometry.PrimeSpectrum.FreeLocus Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.RingTheory.AdicCompletion.Functoriality Mathlib.NumberTheory.ModularForms.Identities Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.Analysis.Complex.Periodic Mathlib.Analysis.Normed.Algebra.Norm Mathlib.Computability.AkraBazzi.GrowsPolynomially Mathlib.NumberTheory.NumberField.Norm Mathlib.FieldTheory.Isaacs Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.NumberTheory.Divisors Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.LinearAlgebra.QuadraticForm.Prod Mathlib.RingTheory.Trace.Basic Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Probability.Distributions.Exponential Mathlib.RingTheory.WittVector.MulCoeff Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.Analysis.Fourier.AddCircleMulti Mathlib.Probability.Martingale.Upcrossing Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.Probability.Martingale.OptionalSampling Mathlib.RingTheory.Kaehler.Polynomial Mathlib.Analysis.RCLike.Inner Mathlib.RingTheory.WittVector.Identities Mathlib.LinearAlgebra.RootSystem.RootPairingCat Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.LinearAlgebra.ExteriorPower.Basic Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.RingTheory.AdicCompletion.Exactness Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.FieldTheory.SeparableClosure Mathlib.RingTheory.WittVector.Truncated Mathlib.NumberTheory.SiegelsLemma Mathlib.LinearAlgebra.JordanChevalley Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.FieldTheory.ChevalleyWarning Mathlib.LinearAlgebra.QuadraticForm.Basic Mathlib.LinearAlgebra.QuadraticForm.Basis Mathlib.NumberTheory.Padics.PadicNumbers Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.RingTheory.RingHom.Flat Mathlib.MeasureTheory.Function.LpSeminorm.Trim Mathlib.Analysis.PSeries Mathlib.Algebra.Module.Presentation.Differentials Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.MeasureTheory.Function.LpSpace Mathlib.NumberTheory.ModularForms.SlashActions Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat Mathlib.GroupTheory.Nilpotent Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Algebra.Module.ZLattice.Basic Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.Probability.Kernel.Disintegration.Integral Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.RingTheory.Unramified.Field Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.FieldTheory.Minpoly.MinpolyDiv Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.NumberTheory.LSeries.Deriv Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.RingTheory.Ideal.Cotangent Mathlib.Analysis.Fourier.AddCircle Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.RingTheory.Flat.Localization Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar Mathlib.Analysis.SpecialFunctions.Pow.Continuity Mathlib.GroupTheory.SchurZassenhaus Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow Mathlib.Topology.Instances.AddCircle Mathlib.NumberTheory.NumberField.Completion Mathlib.Probability.Kernel.WithDensity Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.FieldTheory.Galois.GaloisClosure Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp Mathlib.FieldTheory.Finite.Basic Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.MeasureTheory.Group.AddCircle Mathlib.Probability.Independence.ZeroOne Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.Combinatorics.SimpleGraph.Regularity.Increment Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.MeasureTheory.Function.UniformIntegrable Mathlib.LinearAlgebra.RootSystem.OfBilinear Mathlib.MeasureTheory.Measure.Hausdorff Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.NumberTheory.ModularForms.SlashInvariantForms Mathlib.FieldTheory.IsSepClosed Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.Probability.Distributions.Gaussian Mathlib.NumberTheory.LSeries.Injectivity Mathlib.Probability.Kernel.CondDistrib Mathlib.Analysis.SpecificLimits.FloorPow Mathlib.RingTheory.RootsOfUnity.Lemmas Mathlib.NumberTheory.ModularForms.LevelOne Mathlib.MeasureTheory.Integral.Bochner Mathlib.Algebra.Order.AbsoluteValue.Equivalence Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart Mathlib.RingTheory.Presentation Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.Geometry.Manifold.BumpFunction Mathlib.Probability.Martingale.Basic Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.FieldTheory.Finite.Polynomial Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.Probability.Kernel.RadonNikodym Mathlib.RingTheory.Kaehler.CotangentComplex Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.LSeries.Basic Mathlib.Analysis.Normed.Ring.SeminormFromConst Mathlib.MeasureTheory.Decomposition.SignedLebesgue Mathlib.NumberTheory.SumFourSquares Mathlib.LinearAlgebra.RootSystem.WeylGroup Mathlib.MeasureTheory.Measure.WithDensityFinite Mathlib.RingTheory.Etale.Field Mathlib.Data.Real.Pi.Irrational Mathlib.Analysis.Complex.CauchyIntegral Mathlib.LinearAlgebra.Semisimple Mathlib.FieldTheory.AbsoluteGaloisGroup Mathlib.LinearAlgebra.RootSystem.Basic Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.Analysis.SpecialFunctions.Pow.Deriv Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.Complex.UpperHalfPlane.Topology Mathlib.RingTheory.Smooth.Local Mathlib.RingTheory.Flat.CategoryTheory Mathlib.Analysis.SpecialFunctions.Log.Base Mathlib.MeasureTheory.Order.UpperLower Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.Probability.Martingale.Convergence Mathlib.Analysis.Convex.SpecificFunctions.Pow Mathlib.FieldTheory.KrullTopology Mathlib.Analysis.Complex.UpperHalfPlane.Metric Mathlib.Analysis.Normed.Lp.lpSpace Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.RingTheory.Unramified.Pi Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.Analysis.Normed.Ring.Seminorm Mathlib.RingTheory.Generators Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.Combinatorics.Extremal.RuzsaSzemeredi Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov Mathlib.Analysis.PSeriesComplex Mathlib.Probability.Kernel.Disintegration.Density Mathlib.Analysis.Convex.Integral Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.AlgebraicGeometry.RationalMap Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan Mathlib.FieldTheory.Galois.Profinite Mathlib.FieldTheory.LinearDisjoint Mathlib.LinearAlgebra.CliffordAlgebra.Star Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.MeasureTheory.Integral.Prod Mathlib.MeasureTheory.Integral.Layercake Mathlib.Analysis.CStarAlgebra.Module.Defs Mathlib.Analysis.Complex.Schwarz Mathlib.RingTheory.Etale.Kaehler Mathlib.NumberTheory.LegendreSymbol.Basic Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.Analysis.Complex.UpperHalfPlane.Manifold Mathlib.Analysis.SpecialFunctions.Complex.Arg Mathlib.FieldTheory.Finite.GaloisField Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.MeasureTheory.Covering.OneDim Mathlib.Data.Real.Pi.Leibniz Mathlib.LinearAlgebra.QuadraticForm.Real Mathlib.LinearAlgebra.CliffordAlgebra.Equivs Mathlib.RingTheory.DedekindDomain.IntegralClosure Mathlib.FieldTheory.Galois.Basic Mathlib.RingTheory.WittVector.Verschiebung Mathlib.Algebra.Lie.SkewAdjoint Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.LinearAlgebra.LinearDisjoint Mathlib.Analysis.InnerProductSpace.Positive Mathlib.LinearAlgebra.CliffordAlgebra.Fold Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.Probability.Distributions.Uniform Mathlib.Algebra.Lie.Matrix Mathlib.MeasureTheory.Covering.DensityTheorem Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.GroupTheory.Torsion Mathlib.LinearAlgebra.QuadraticForm.Complex Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Topology.CWComplex Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.NumberTheory.Ostrowski Mathlib.MeasureTheory.Measure.Doubling Mathlib.Analysis.MeanInequalities Mathlib.LinearAlgebra.Matrix.BilinearForm Mathlib.FieldTheory.PrimitiveElement Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.Analysis.Normed.Ring.SeminormFromBounded Mathlib.RingTheory.Smooth.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Even Mathlib.Combinatorics.Additive.Randomisation Mathlib.RingTheory.Flat.FaithfullyFlat Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.Analysis.CStarAlgebra.ApproximateUnit Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog Mathlib.Analysis.SpecialFunctions.BinaryEntropy Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.Analysis.BoxIntegral.Basic Mathlib.Analysis.Quaternion Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex Mathlib.Analysis.BoxIntegral.Integrability Mathlib.RingTheory.Discriminant Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Topology.Category.TopCat.Sphere Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup Mathlib.Analysis.Calculus.FDeriv.Norm Mathlib.LinearAlgebra.CliffordAlgebra.Inversion Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.Topology.MetricSpace.GromovHausdorff Mathlib.NumberTheory.Harmonic.Int Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.RingTheory.WittVector.StructurePolynomial Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving Mathlib.LinearAlgebra.Dimension.Torsion.Finite Mathlib.MeasureTheory.Function.L1Space Mathlib.Probability.Kernel.Disintegration.Basic Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Data.Finset.NatDivisors Mathlib.MeasureTheory.Measure.Tilted Mathlib.Analysis.Complex.Liouville Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.GroupTheory.SpecificGroups.Quaternion Mathlib.NumberTheory.Transcendental.Liouville.Measure Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.RingTheory.Extension Mathlib.MeasureTheory.Function.Jacobian Mathlib.NumberTheory.Transcendental.Lindemann.Init.AnalyticalPart Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.MeasureTheory.Function.LpOrder Mathlib.Analysis.Convex.Measure Mathlib.Probability.Moments Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.Analysis.Normed.Lp.LpEquiv Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.Algebra.Module.CharacterModule Mathlib.NumberTheory.Padics.PadicVal.Basic Mathlib.MeasureTheory.Group.FundamentalDomain Mathlib.Algebra.Module.Torsion Mathlib.Analysis.Complex.Conformal Mathlib.Analysis.Normed.Group.AddCircle Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.RingTheory.RootsOfUnity.Complex Mathlib.NumberTheory.Padics.RingHoms Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics Mathlib.LinearAlgebra.CliffordAlgebra.Grading Mathlib.Data.Real.Pi.Bounds Mathlib.MeasureTheory.Decomposition.Lebesgue Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.Algebra.Category.Ring.Under.Limits Mathlib.Topology.Algebra.PontryaginDual Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity Mathlib.MeasureTheory.Function.LocallyIntegrable Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence Mathlib.Topology.MetricSpace.Holder Mathlib.RingTheory.Smooth.StandardSmooth Mathlib.LinearAlgebra.CliffordAlgebra.Basic Mathlib.NumberTheory.ModularForms.Basic Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.RingTheory.WittVector.Frobenius Mathlib.LinearAlgebra.Matrix.SesquilinearForm Mathlib.Analysis.NormedSpace.DualNumber Mathlib.Probability.Process.Stopping Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.NumberTheory.NumberField.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.FieldTheory.CardinalEmb Mathlib.NumberTheory.Modular Mathlib.RingTheory.WittVector.Basic Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk Mathlib.MeasureTheory.Integral.MeanInequalities Mathlib.GroupTheory.Transfer Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty Mathlib.RingTheory.Smooth.Kaehler Mathlib.Analysis.Normed.Algebra.Basic Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.RingTheory.WittVector.Isocrystal Mathlib.Geometry.Manifold.IntegralCurve.UniformTime Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.RingTheory.Trace.Quotient Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality Mathlib.LinearAlgebra.Matrix.Hermitian Mathlib.Analysis.Calculus.Monotone Mathlib.RingTheory.Polynomial.Selmer Mathlib.RingTheory.Unramified.Basic Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv Mathlib.Analysis.SumIntegralComparisons Mathlib.MeasureTheory.VectorMeasure.WithDensity Mathlib.LinearAlgebra.Reflection Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.NumberTheory.FermatPsp Mathlib.RingTheory.Kaehler.Basic Mathlib.GroupTheory.Sylow Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField Mathlib.NumberTheory.ZetaValues Mathlib.Topology.MetricSpace.HolderNorm Mathlib.Analysis.Complex.Positivity Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.Analysis.Fourier.FourierTransform Mathlib.LinearAlgebra.Matrix.LDL Mathlib.Probability.Independence.Integrable Mathlib.Algebra.Lie.Weights.Killing Mathlib.Analysis.Matrix Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup Mathlib.Analysis.SpecialFunctions.Pow.Real Mathlib.RingTheory.Smooth.Pi Mathlib.Probability.IdentDistrib Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.RingTheory.Complex Mathlib.Dynamics.TopologicalEntropy.Semiconj Mathlib.Analysis.Convolution Mathlib.RingTheory.Unramified.Locus Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.RingTheory.Etale.Pi Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.LinearAlgebra.Eigenspace.Semisimple Mathlib.FieldTheory.KummerExtension Mathlib.NumberTheory.LucasPrimality Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.LinearAlgebra.QuadraticForm.Isometry Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.Analysis.Complex.Arg Mathlib.Topology.MetricSpace.Kuratowski Mathlib.Analysis.MellinInversion Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear Mathlib.RingTheory.AdicCompletion.Algebra Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Analysis.Complex.UpperHalfPlane.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.Analysis.Normed.Ring.IsPowMulFaithful Mathlib.NumberTheory.Padics.Hensel Mathlib.MeasureTheory.Covering.Differentiation Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.LinearAlgebra.QuadraticForm.TensorProduct Mathlib.Analysis.Complex.Hadamard Mathlib.RingTheory.Etale.Basic Mathlib.RingTheory.LinearDisjoint Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap Mathlib.FieldTheory.JacobsonNoether Mathlib.LinearAlgebra.Dimension.Torsion.Basic Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Analysis.BoundedVariation Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Analysis.InnerProductSpace.Semisimple Mathlib.Combinatorics.SimpleGraph.Regularity.Bound Mathlib.RingTheory.WittVector.Teichmuller Mathlib.NumberTheory.WellApproximable Mathlib.RingTheory.LocalRing.Module Mathlib.MeasureTheory.Measure.Lebesgue.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Contraction Mathlib.NumberTheory.LSeries.Convergence Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Probability.Process.Adapted Mathlib.Analysis.Convex.Cone.Proper Mathlib.Probability.Distributions.Pareto Mathlib.NumberTheory.DirichletCharacter.Bounds Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.FieldTheory.PurelyInseparable Mathlib.RingTheory.RingHom.Unramified Mathlib.Algebra.Polynomial.Module.FiniteDimensional Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.RingTheory.WittVector.IsPoly Mathlib.RingTheory.Kaehler.TensorProduct Mathlib.MeasureTheory.Integral.Pi Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.GroupTheory.SpecificGroups.Cyclic Mathlib.Analysis.Complex.UpperHalfPlane.Exp Mathlib.NumberTheory.NumberField.Embeddings Mathlib.MeasureTheory.Function.Intersectivity Mathlib.Dynamics.TopologicalEntropy.CoverEntropy Mathlib.Analysis.CStarAlgebra.lpSpace Mathlib.Probability.Process.Filtration Mathlib.MeasureTheory.Integral.Periodic Mathlib.NumberTheory.Harmonic.Bounds Mathlib.Analysis.MellinTransform Mathlib.RingTheory.Flat.Equalizer Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating Mathlib.NumberTheory.LSeries.Linearity Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card Mathlib.MeasureTheory.Integral.Gamma Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Integral.IntegrableOn Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.RingTheory.WittVector.Defs Mathlib.Probability.Kernel.Condexp Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.GroupTheory.Order.Min Mathlib.LinearAlgebra.CliffordAlgebra.Prod Mathlib.FieldTheory.Galois.Infinite Mathlib.Algebra.Lie.Classical Mathlib.Analysis.SpecialFunctions.Complex.Circle Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma Mathlib.Geometry.Euclidean.Triangle Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Analysis.Complex.IntegerCompl Mathlib.GroupTheory.SpecificGroups.KleinFour Mathlib.Probability.Distributions.Gamma Mathlib.Probability.Martingale.OptionalStopping Mathlib.RingTheory.Flat.Stability Mathlib.Probability.Martingale.BorelCantelli Mathlib.NumberTheory.Padics.ProperSpace Mathlib.Probability.Density Mathlib.Analysis.Complex.OpenMapping Mathlib.Probability.ProbabilityMassFunction.Integrals Mathlib.RingTheory.WittVector.FrobeniusFractionField Mathlib.LinearAlgebra.Matrix.ToLinearEquiv Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.RingTheory.IntegralDomain Mathlib.Analysis.ODE.PicardLindelof Mathlib.RingTheory.RootsOfUnity.Minpoly Mathlib.Probability.ConditionalExpectation Mathlib.MeasureTheory.Integral.SetIntegral Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.GroupTheory.Frattini Mathlib.RingTheory.WittVector.DiscreteValuationRing Mathlib.FieldTheory.PolynomialGaloisGroup Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.GroupTheory.PGroup Mathlib.NumberTheory.ModularForms.CongruenceSubgroups Mathlib.Analysis.SpecialFunctions.Pow.NNReal Mathlib.Algebra.Category.Grp.Injective Mathlib.LinearAlgebra.RootSystem.RootPositive Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.MeasureTheory.Group.Integral Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.RingTheory.Unramified.Finite Mathlib.RingTheory.Kaehler.JacobiZariski Mathlib.Probability.Integration Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.NumberTheory.Bertrand Mathlib.GroupTheory.Schreier Mathlib.RingTheory.NormTrace Mathlib.LinearAlgebra.RootSystem.Hom Mathlib.Combinatorics.Additive.CauchyDavenport Mathlib.Analysis.SpecialFunctions.Gamma.Deriv Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.RingTheory.RootsOfUnity.Basic Mathlib.Probability.Kernel.Integral Mathlib.MeasureTheory.Integral.Average Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.Probability.Independence.Conditional Mathlib.NumberTheory.AbelSummation Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog Mathlib.LinearAlgebra.Matrix.FixedDetMatrices Mathlib.RingTheory.Perfection Mathlib.RingTheory.Norm.Basic Mathlib.Data.Real.Pi.Wallis Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Notation Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.Probability.CDF Mathlib.LinearAlgebra.ExteriorAlgebra.Basic Mathlib.Data.Nat.Totient Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.GroupTheory.SpecificGroups.ZGroup Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic Mathlib.Probability.Martingale.Centering Mathlib.Analysis.Calculus.ContDiff.WithLp Mathlib.LinearAlgebra.QuadraticForm.Dual Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.LinearAlgebra.RootSystem.Defs Mathlib.RingTheory.WittVector.MulP Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate Mathlib.Analysis.Normed.Algebra.UnitizationL1 |
1 |
Declarations diff
+ disjoint_divisors_filter_isPrimePow
- Nat.disjoint_divisors_filter_isPrimePow
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.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jan 10, 2025
Moves a theorem to reduce the `NumberTheory` -> `Algebra` imports.
Contributor
|
Pull request successfully merged into master. Build succeeded: |
grunweg
pushed a commit
that referenced
this pull request
Jan 11, 2025
Moves a theorem to reduce the `NumberTheory` -> `Algebra` imports.
Julian
added a commit
that referenced
this pull request
Jan 12, 2025
* origin/master: (88 commits) chore(scripts): update nolints.json (#20672) chore: de-simp `map_eq_zero_iff_eq_one` (#20662) feat(Combinatorics/SimpleGraph): add independent sets (#18608) chore(CategoryTheory/Limits/Cones): functoriality of `mapCone` (#20641) feat(Algebra/Category/ModuleCat): pullback of presheaves of modules (#17366) feat(AlgebraicTopology): model categories (#19158) chore(CategoryTheory): make NormalEpi/MonoCategory and RegularEpi/MonoCategory props (#19548) feat(Data/List/ReduceOption): add replicate theorems (#20644) feat: approximate subgroups (#20050) feat: use scoped trace nodes in linarith (#19855) feat: disjoint union of charted spaces (#20619) feat: add some term elaborators for reduction (#15192) feat(Topology/Category): category of delta-generated spaces (#19499) add a variable_alias for Quantale and AddQuantale (#19282) feat(Computability/DFA): implement `isRegular_iff` (#19940) chore: unpin and bump batteries and importgraph (#20651) chore: split `Mathlib/Algebra/Group/Int` (#20624) feat: three lemmas related to Hausdorff distance (#20585) chore: `initialize_simps_projections` for `Submodule` (#20582) feat(Order): Boolean algebra structure on idempotents (#20618) chore(CategoryTheory): moving/renaming Subpresheaf (#20583) refactor(IntermediateField/Adjoin): Split off relation to `Algebra.adjoin` (#20630) feat: sets of doubling strictly less than 3/2 (#20572) chore(TensorProduct): universe polymorphism in EquationalCriterion (#20452) feat: `s \ t ∩ u = (s ∩ u) \ t` (#20298) feat: product of subalgebras (#20202) feat: `Submodule.restrictScalars` commutes with `pow` (#20581) feat: `a ∈ s ^ n` iff there exists a sequence `f` of `n` elements of `s` such that `∏ i, f i = a` (#20580) chore: make `FooHom.coe_id` a `norm_cast` lemma (#20576) chore: use ofNat more (#20546) feat(CategoryTheory/Shift/Opposite and CategoryTheory/Shift/Pullback): `CommShift` structures on adjunctions are compatible with opposites and pullbacks (#20363) feat(FieldTheory/Differential/Liouville): prove the algebraic case of Liouville's theorem (#16797) refactor: remove the `CompactSpace` field from `Unique{NonUnital}ContinuousFunctionalCalculus` (#20590) feat: Make `PNat.recOn` induction eliminator (#20617) feat(Analysis/SpecialFunctions/Pow/Real): add some lemmas (#20608) feat: If `s ∆ t` is finite, then `s ∆ u` is finite iff `t ∆ u` is (#20574) feat: `⨅ i, f i ≤ ⨆ i, f i` (#20573) chore(Geometry/Manifold): move SmoothManifoldWithCorners.lean to IsManifold.lean (#20611) feat: AbsoluteValue.IsNontrivial (#20588) chore(Data/Finsupp): split off extensionality from `Defs.lean` (#19092) chore(Data/Set): split the `CoeSort` instance to its own file (#19031) feat(Algebra/Order/Archimedean/Basic): powers between two elements (#20612) feature(Algebra/Ring/Idempotents): product of an idempotent and its complement (#20286) chore: cleanup more `erw` (#20601) chore(GroupTheory/CoprodI): shorten proof of lift_word_prod_nontrivial_of_not_empty (#20587) chore: cleanup imports in PrimePow/Divisors (#20626) chore: split Algebra/BigOperators/Group/List (#20625) chore: reduce Topology->Order imports by moving content (#20627) chore(Algebra/Lie/DirectSum): shorten proof of lieAlgebraOf.map_lie' (#20592) refactor: Split `FieldTheory/Adjoin.lean` into `Defs.lean` and `Basic.lean` (#20333) ...
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Moves a theorem to reduce the
NumberTheory->Algebraimports.