[Merged by Bors] - feat: generalise algebraMap_injective by weakening its typeclass assumptions#21287
Closed
[Merged by Bors] - feat: generalise algebraMap_injective by weakening its typeclass assumptions#21287
algebraMap_injective by weakening its typeclass assumptions#21287Conversation
…mptions By weakening the assumptions `[Nontrivial A] [NoZeroSMulDivisors R A]` to just `[FaithfulSMul R A]`, results which need to use `algebraMap_injective` can be applied in that case that we have `[Ring A] [CharZero A]` but fail to have `[NoZeroSMulDivisors ℤ A]`. This is the motivation for these changes.
PR summary 14c33aa1b7
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Topology.Algebra.Module.FiniteDimension | 1616 | 1609 | -7 (-0.43%) |
| Mathlib.Algebra.Algebra.Basic | 693 | 692 | -1 (-0.14%) |
Import changes for all files
| Files | Import difference |
|---|---|
412 filesMathlib.Analysis.Analytic.Polynomial Mathlib.Analysis.BoundedVariation Mathlib.Analysis.BoxIntegral.Basic Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.Analysis.BoxIntegral.Integrability Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.Analysis.Calculus.AddTorsor.Coord Mathlib.Analysis.Calculus.BumpFunction.Basic Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Analysis.Calculus.Conformal.InnerProduct Mathlib.Analysis.Calculus.ContDiff.FiniteDimension Mathlib.Analysis.Calculus.ContDiff.RCLike Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.Calculus.FDeriv.Extend Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.Analysis.Calculus.FDeriv.Norm Mathlib.Analysis.Calculus.FDeriv.Symmetric Mathlib.Analysis.Calculus.FirstDerivativeTest Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.Analysis.Calculus.Implicit Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional Mathlib.Analysis.Calculus.LHopital Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.Analysis.Calculus.MeanValue Mathlib.Analysis.Calculus.Monotone Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Calculus.SmoothSeries Mathlib.Analysis.Calculus.Taylor Mathlib.Analysis.Calculus.UniformLimitsDeriv Mathlib.Analysis.Calculus.VectorField Mathlib.Analysis.Complex.AbsMax Mathlib.Analysis.Complex.Angle Mathlib.Analysis.Complex.Arg Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.Complex.Liouville Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.Analysis.Complex.OpenMapping Mathlib.Analysis.Complex.Periodic Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.Analysis.Complex.Positivity Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Analysis.Complex.Schwarz Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Complex.Tietze Mathlib.Analysis.Convex.AmpleSet Mathlib.Analysis.Convex.Cone.Closure Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Analysis.Convex.Cone.Pointed Mathlib.Analysis.Convex.Cone.Proper Mathlib.Analysis.Convex.Continuous Mathlib.Analysis.Convex.Deriv Mathlib.Analysis.Convex.GaugeRescale Mathlib.Analysis.Convex.Integral Mathlib.Analysis.Convex.Intrinsic Mathlib.Analysis.Convex.KreinMilman Mathlib.Analysis.Convex.Measure Mathlib.Analysis.Convex.Normed Mathlib.Analysis.Convex.Side Mathlib.Analysis.Convex.SpecificFunctions.Deriv Mathlib.Analysis.Convex.StrictConvexBetween Mathlib.Analysis.Convex.StrictConvexSpace Mathlib.Analysis.Convex.Strong Mathlib.Analysis.Convex.Uniform Mathlib.Analysis.Convolution Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality Mathlib.Analysis.Fourier.FourierTransform Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Analysis.InnerProductSpace.Basic Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Analysis.InnerProductSpace.Completion Mathlib.Analysis.InnerProductSpace.ConformalLinearMap Mathlib.Analysis.InnerProductSpace.Dual Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.Analysis.InnerProductSpace.LinearMap Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Analysis.InnerProductSpace.OfNorm Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.Analysis.InnerProductSpace.Orthogonal Mathlib.Analysis.InnerProductSpace.Orthonormal Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.Analysis.InnerProductSpace.Positive Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Analysis.InnerProductSpace.Projection Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.Analysis.InnerProductSpace.Subspace Mathlib.Analysis.InnerProductSpace.Symmetric Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.Analysis.LocallyConvex.WeakOperatorTopology Mathlib.Analysis.LocallyConvex.WeakSpace Mathlib.Analysis.Matrix Mathlib.Analysis.MellinInversion Mathlib.Analysis.MellinTransform Mathlib.Analysis.Normed.Affine.AddTorsorBases Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.Analysis.Normed.Module.Complemented Mathlib.Analysis.Normed.Module.Dual Mathlib.Analysis.Normed.Module.FiniteDimension Mathlib.Analysis.Normed.Module.WeakDual Mathlib.Analysis.NormedSpace.HahnBanach.Extension Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual Mathlib.Analysis.NormedSpace.HahnBanach.Separation Mathlib.Analysis.ODE.Gronwall Mathlib.Analysis.ODE.PicardLindelof Mathlib.Analysis.PSeriesComplex Mathlib.Analysis.Quaternion Mathlib.Analysis.RCLike.Inner Mathlib.Analysis.RCLike.Lemmas Mathlib.Analysis.SpecialFunctions.Arsinh Mathlib.Analysis.SpecialFunctions.BinaryEntropy Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.Analysis.SpecialFunctions.ExpDeriv Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Analysis.SpecialFunctions.Gamma.Deriv Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.Analysis.SpecialFunctions.Integrals Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.Analysis.SpecialFunctions.Log.Deriv Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.Analysis.SpecialFunctions.Log.Summable Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.Analysis.SpecialFunctions.Pow.Deriv Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv Mathlib.Analysis.SumIntegralComparisons Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.Combinatorics.Additive.Randomisation Mathlib.Combinatorics.Extremal.RuzsaSzemeredi Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.Data.Complex.ExponentialBounds Mathlib.Data.Real.Pi.Bounds Mathlib.Data.Real.Pi.Leibniz Mathlib.Data.Real.Pi.Wallis Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.Geometry.Euclidean.Basic Mathlib.Geometry.Euclidean.Circumcenter Mathlib.Geometry.Euclidean.Inversion.Basic Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane Mathlib.Geometry.Euclidean.MongePoint Mathlib.Geometry.Euclidean.PerpBisector Mathlib.Geometry.Euclidean.Sphere.Basic Mathlib.Geometry.Euclidean.Sphere.Power Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.Geometry.Euclidean.Sphere.SecondInter Mathlib.Geometry.Euclidean.Triangle Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation Mathlib.Geometry.Manifold.Algebra.LieGroup Mathlib.Geometry.Manifold.Algebra.Monoid Mathlib.Geometry.Manifold.Algebra.SmoothFunctions Mathlib.Geometry.Manifold.Algebra.Structures Mathlib.Geometry.Manifold.AnalyticManifold Mathlib.Geometry.Manifold.BumpFunction Mathlib.Geometry.Manifold.Complex Mathlib.Geometry.Manifold.ContMDiff.Atlas Mathlib.Geometry.Manifold.ContMDiff.Basic Mathlib.Geometry.Manifold.ContMDiff.Defs Mathlib.Geometry.Manifold.ContMDiff.NormedSpace Mathlib.Geometry.Manifold.ContMDiff.Product Mathlib.Geometry.Manifold.ContMDiffMFDeriv Mathlib.Geometry.Manifold.ContMDiffMap Mathlib.Geometry.Manifold.DerivationBundle Mathlib.Geometry.Manifold.Diffeomorph Mathlib.Geometry.Manifold.Instances.Real Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra Mathlib.Geometry.Manifold.IntegralCurve.Basic Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.Geometry.Manifold.IntegralCurve.Transform Mathlib.Geometry.Manifold.IntegralCurve.UniformTime Mathlib.Geometry.Manifold.IsManifold.Basic Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary Mathlib.Geometry.Manifold.LocalDiffeomorph Mathlib.Geometry.Manifold.MFDeriv.Atlas Mathlib.Geometry.Manifold.MFDeriv.Basic Mathlib.Geometry.Manifold.MFDeriv.Defs Mathlib.Geometry.Manifold.MFDeriv.FDeriv Mathlib.Geometry.Manifold.MFDeriv.NormedSpace Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions Mathlib.Geometry.Manifold.MFDeriv.Tangent Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential Mathlib.Geometry.Manifold.Metrizable Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Geometry.Manifold.VectorBundle.Basic Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear Mathlib.Geometry.Manifold.VectorBundle.Hom Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable Mathlib.Geometry.Manifold.VectorBundle.Pullback Mathlib.Geometry.Manifold.VectorBundle.SmoothSection Mathlib.Geometry.Manifold.VectorBundle.Tangent Mathlib.Geometry.Manifold.VectorField Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.LinearAlgebra.Matrix.Hermitian Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.MeasureTheory.Covering.DensityTheorem Mathlib.MeasureTheory.Covering.Differentiation Mathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.MeasureTheory.Covering.OneDim Mathlib.MeasureTheory.Decomposition.IntegralRNDeriv Mathlib.MeasureTheory.Decomposition.Lebesgue Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.MeasureTheory.Decomposition.SignedLebesgue Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.MeasureTheory.Function.Intersectivity Mathlib.MeasureTheory.Function.Jacobian Mathlib.MeasureTheory.Function.L1Space.AEEqFun Mathlib.MeasureTheory.Function.L1Space.Integrable Mathlib.MeasureTheory.Function.L2Space Mathlib.MeasureTheory.Function.LocallyIntegrable Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.MeasureTheory.Function.SpecialFunctions.Inner Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.MeasureTheory.Function.UnifTight Mathlib.MeasureTheory.Function.UniformIntegrable Mathlib.MeasureTheory.Group.AddCircle Mathlib.MeasureTheory.Group.FundamentalDomain Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.MeasureTheory.Group.Integral Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.MeasureTheory.Integral.Average Mathlib.MeasureTheory.Integral.Bochner Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.MeasureTheory.Integral.Gamma Mathlib.MeasureTheory.Integral.IntegrableOn Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.MeasureTheory.Integral.Layercake Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.MeasureTheory.Integral.Periodic Mathlib.MeasureTheory.Integral.Pi Mathlib.MeasureTheory.Integral.Prod Mathlib.MeasureTheory.Integral.SetIntegral Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.MeasureTheory.Measure.Hausdorff Mathlib.MeasureTheory.Measure.Lebesgue.Basic Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.MeasureTheory.Measure.Tilted Mathlib.MeasureTheory.Measure.WithDensityFinite Mathlib.MeasureTheory.Order.UpperLower Mathlib.MeasureTheory.VectorMeasure.WithDensity Mathlib.NumberTheory.AbelSummation Mathlib.NumberTheory.Bertrand Mathlib.NumberTheory.EulerProduct.ExpLog Mathlib.NumberTheory.Harmonic.Bounds Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.LSeries.Basic Mathlib.NumberTheory.LSeries.Convergence Mathlib.NumberTheory.LSeries.Convolution Mathlib.NumberTheory.LSeries.Deriv Mathlib.NumberTheory.LSeries.Injectivity Mathlib.NumberTheory.LSeries.Linearity Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.NumberTheory.LSeries.Positivity Mathlib.NumberTheory.LSeries.SumCoeff Mathlib.NumberTheory.SiegelsLemma Mathlib.NumberTheory.WellApproximable Mathlib.Probability.BorelCantelli Mathlib.Probability.CDF Mathlib.Probability.CondVar Mathlib.Probability.ConditionalExpectation Mathlib.Probability.Density Mathlib.Probability.Distributions.Exponential Mathlib.Probability.Distributions.Gamma Mathlib.Probability.Distributions.Gaussian Mathlib.Probability.Distributions.Pareto Mathlib.Probability.Distributions.Uniform Mathlib.Probability.IdentDistrib Mathlib.Probability.Independence.Conditional Mathlib.Probability.Independence.Integrable Mathlib.Probability.Independence.ZeroOne Mathlib.Probability.Integration Mathlib.Probability.Kernel.Composition.IntegralCompProd Mathlib.Probability.Kernel.Composition.Lemmas Mathlib.Probability.Kernel.Composition.MeasureCompProd Mathlib.Probability.Kernel.Composition.MeasureComp Mathlib.Probability.Kernel.CondDistrib Mathlib.Probability.Kernel.Condexp Mathlib.Probability.Kernel.Disintegration.Basic Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.Probability.Kernel.Disintegration.Density Mathlib.Probability.Kernel.Disintegration.Integral Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.Probability.Kernel.Integral Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Probability.Kernel.RadonNikodym Mathlib.Probability.Kernel.WithDensity Mathlib.Probability.Martingale.Basic Mathlib.Probability.Martingale.BorelCantelli Mathlib.Probability.Martingale.Centering Mathlib.Probability.Martingale.Convergence Mathlib.Probability.Martingale.OptionalSampling Mathlib.Probability.Martingale.OptionalStopping Mathlib.Probability.Martingale.Upcrossing Mathlib.Probability.Moments.Basic Mathlib.Probability.Moments.ComplexMGF Mathlib.Probability.Moments.IntegrableExpMul Mathlib.Probability.Moments.MGFAnalytic Mathlib.Probability.Notation Mathlib.Probability.ProbabilityMassFunction.Integrals Mathlib.Probability.Process.Adapted Mathlib.Probability.Process.Filtration Mathlib.Probability.Process.HittingTime Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Process.Stopping Mathlib.Probability.StrongLaw Mathlib.Probability.Variance Mathlib.RingTheory.Polynomial.Hermite.Gaussian Mathlib.Tactic.FunProp.ContDiff Mathlib.Tactic.FunProp.Differentiable Mathlib.Topology.Algebra.Module.FiniteDimension Mathlib.Topology.CWComplex Mathlib.Topology.Category.TopCat.Sphere Mathlib.Topology.MetricSpace.HausdorffDimension |
-7 |
Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace |
-2 |
67 filesMathlib.Algebra.Algebra.Basic Mathlib.Algebra.Algebra.Equiv Mathlib.Algebra.Algebra.Hom.Rat Mathlib.Algebra.Algebra.Hom Mathlib.Algebra.Algebra.NonUnitalHom Mathlib.Algebra.Algebra.Opposite Mathlib.Algebra.Algebra.Pi Mathlib.Algebra.Algebra.Prod Mathlib.Algebra.Category.Grp.Biproducts Mathlib.Algebra.Category.Grp.FilteredColimits Mathlib.Algebra.Category.Grp.Limits Mathlib.Algebra.Category.MonCat.FilteredColimits Mathlib.Algebra.Category.MonCat.Limits Mathlib.Algebra.Category.Ring.FilteredColimits Mathlib.Algebra.Category.Ring.Limits Mathlib.Algebra.Equiv.TransferInstance Mathlib.Algebra.Group.AddChar Mathlib.Algebra.Homology.Embedding.RestrictionHomology Mathlib.Algebra.Homology.ExactSequence Mathlib.Algebra.Homology.Factorizations.Basic Mathlib.Algebra.Homology.HomologicalComplexAbelian Mathlib.Algebra.Homology.HomologySequence Mathlib.Algebra.Homology.Refinements Mathlib.Algebra.Homology.ShortComplex.ExactFunctor Mathlib.Algebra.Homology.ShortComplex.Exact Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex Mathlib.Algebra.Homology.ShortComplex.Preadditive Mathlib.Algebra.Homology.ShortComplex.ShortExact Mathlib.Algebra.Homology.ShortComplex.SnakeLemma Mathlib.Algebra.Homology.SingleHomology Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra Mathlib.Algebra.Small.Group Mathlib.Algebra.Small.Module Mathlib.Algebra.Small.Ring Mathlib.Algebra.Star.StarAlgHom Mathlib.AlgebraicTopology.AlternatingFaceMapComplex Mathlib.AlgebraicTopology.DoldKan.Notations Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel Mathlib.CategoryTheory.Abelian.Exact Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Sheaf Mathlib.CategoryTheory.Abelian.GrothendieckCategory Mathlib.CategoryTheory.Abelian.Opposite Mathlib.CategoryTheory.Abelian.Refinements Mathlib.CategoryTheory.Abelian.Transfer Mathlib.CategoryTheory.Adjunction.Additive Mathlib.CategoryTheory.Galois.Basic Mathlib.CategoryTheory.Galois.Decomposition Mathlib.CategoryTheory.Galois.GaloisObjects Mathlib.CategoryTheory.Galois.Prorepresentability Mathlib.CategoryTheory.Generator.Abelian Mathlib.CategoryTheory.Generator.Preadditive Mathlib.CategoryTheory.Linear.Yoneda Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive Mathlib.CategoryTheory.Preadditive.Opposite Mathlib.CategoryTheory.Preadditive.Transfer Mathlib.CategoryTheory.Preadditive.Yoneda.Basic Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.CategoryTheory.Shift.Opposite Mathlib.CategoryTheory.Shift.ShiftedHomOpposite Mathlib.CategoryTheory.Sites.Abelian Mathlib.CategoryTheory.Triangulated.Opposite.Basic Mathlib.CategoryTheory.Triangulated.Opposite.Triangle Mathlib.Geometry.RingedSpace.Basic Mathlib.MeasureTheory.Constructions.AddChar |
-1 |
Declarations diff
+ Algebra.charZero_of_charZero
+ FaithfulSMul.ker_algebraMap_eq_bot
+ FaithfulSMul.of_field_isFractionRing
+ NoZeroSMulDivisors.iff_ker_algebraMap_eq_bot
+ NoZeroSMulDivisors.ker_algebraMap_eq_bot
+ NoZeroSMulDivisors.of_ker_algebraMap_eq_bot
+ NoZeroSMulDivisors.trans_faithfulSMul
+ _root_.NeZero.of_faithfulSMul
+ _root_.NoZeroSMulDivisors.algebraMap_eq_one_iff
+ _root_.NoZeroSMulDivisors.algebraMap_eq_zero_iff
+ _root_.NoZeroSMulDivisors.algebraMap_injective
+ algebraMap_comp_intCast
+ algebraMap_comp_natCast
+ faithfulSMul_iff_algebraMap_injective
+ faithfulSMul_iff_injective_smul_one
+ iff_faithfulSMul
+ instFaithfulSMul
+ instance (R : Type*) [NonAssocSemiring R] : FaithfulSMul R R := ⟨fun {r₁ r₂} h ↦ by simpa using h 1⟩
+ instance (priority := 100) (R : Type*) [Ring R] [CharZero R] : FaithfulSMul ℤ R := by
+ instance (priority := 100) : FaithfulSMul R K
+ instance (priority := 100) [CharZero R] : FaithfulSMul ℕ R := by
+ instance (priority := 100) [IsDomain R] : NoZeroSMulDivisors R M := by
+ instance (priority := 100) instOfFaithfulSMul {R A : Type*}
+ instance [Algebra R A] [FaithfulSMul R A] : FaithfulSMul R (FractionRing A) := by
+ instance [IsFractionRing A K] : NoZeroSMulDivisors A (CyclotomicField n K) := by
+ instance [Nontrivial A] [NoZeroSMulDivisors R A] : FaithfulSMul R A
- CyclotomicField.noZeroSMulDivisors
- NoZeroSMulDivisors.trans
- iff_ker_algebraMap_eq_bot
- instance (priority := 100) CharZero.noZeroSMulDivisors_int [Ring R] [NoZeroDivisors R]
- instance (priority := 100) CharZero.noZeroSMulDivisors_nat [Semiring R] [NoZeroDivisors R]
- instance (priority := 100) [NoZeroDivisors K] : NoZeroSMulDivisors R K
- instance [Algebra R A] [NoZeroSMulDivisors R A] : NoZeroSMulDivisors R (FractionRing A) := by
- instance [IsDomain R] : NoZeroSMulDivisors R M := by
- instance [P.IsPrime] : NoZeroSMulDivisors (A ⧸ p) (B ⧸ P)
- ker_algebraMap_eq_bot
- of_ker_algebraMap_eq_bot
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).
Contributor
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit c083b02. |
I am witnessing a bizarre situation where everything builds fine, including `inftyValuation.polynomial` (which typechecks very quickly) but the `simpNF` linter falls over reporting: ``` /- The `simpNF` linter reports: SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM. see note [simp-normal form] for tips how to debug this. https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/ -- Mathlib.NumberTheory.FunctionField ././././Mathlib/NumberTheory/FunctionField.lean:210:1: error: FunctionField.inftyValuation.polynomial LINTER FAILED: simplify fails on left-hand side: failed to synthesize FaithfulSMul (Polynomial Fq) (RatFunc Fq) (deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached Use `set_option synthInstance.maxHeartbeats <num>` to set the limit. ``` This change is a test (which I hope is not successful) to check whether it is the new form of this proof which triggers the failure.
This reverts commit d6c7dbe.
Somewhat mitigated by the fact that this is only a conditional simp lemma (i.e., it needs the hypothesis `p ≠ 0`).
Contributor
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit 9b13d1b. Benchmark Metric Change
===============================================================
- ~Mathlib.Algebra.Lie.Weights.RootSystem instructions 5.8%
- ~Mathlib.FieldTheory.Galois.Infinite instructions 16.5%
- ~Mathlib.FieldTheory.IsAlgClosed.Basic instructions 9.1% |
2 files, Instructions +11.0⬝10⁹
3 files, Instructions +3.0⬝10⁹
6 files, Instructions +2.0⬝10⁹
17 files, Instructions +1.0⬝10⁹
4 files, Instructions -2.0⬝10⁹
|
…rmance impact. It seems unlikely this should matter but maybe worth testing. Also fixing an unrelated naming issue.
Contributor
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit 9ae2bbc. Benchmark Metric Change
===============================================================
- ~Mathlib.Algebra.Lie.Weights.RootSystem instructions 5.8%
- ~Mathlib.FieldTheory.Galois.Infinite instructions 16.4%
- ~Mathlib.FieldTheory.IsAlgClosed.Basic instructions 9.6% |
2 files, Instructions +11.0⬝10⁹
3 files, Instructions +3.0⬝10⁹
7 files, Instructions +2.0⬝10⁹
16 files, Instructions +1.0⬝10⁹
5 files, Instructions -2.0⬝10⁹
|
1 task
Collaborator
|
Here are the benchmark results for commit 3c55810. Benchmark Metric Change
===============================================================
+ ~Mathlib.Algebra.Lie.Weights.RootSystem instructions -17.9% |
2 files, Instructions +3.0⬝10⁹
4 files, Instructions +1.0⬝10⁹
8 files, Instructions -2.0⬝10⁹
|
alreadydone
approved these changes
Feb 1, 2025
Comment on lines
210
to
212
|
|
||
| @[simp] | ||
| theorem inftyValuation.polynomial {p : Fq[X]} (hp : p ≠ 0) : | ||
| inftyValuationDef Fq (algebraMap Fq[X] (RatFunc Fq) p) = | ||
| Multiplicative.ofAdd (p.natDegree : ℤ) := by |
Contributor
Author
There was a problem hiding this comment.
I'd like to test this in isolation so I will come back to this after everything else has built.
It is a legacy of a bizarre situation where I saw everything build fine, including inftyValuation.polynomial (which typechecked very quickly) but the simpNF linter fell over reporting:
/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
-- Mathlib.NumberTheory.FunctionField
././././Mathlib/NumberTheory/FunctionField.lean:210:1: error: FunctionField.inftyValuation.polynomial LINTER FAILED:
simplify fails on left-hand side:
failed to synthesize
FaithfulSMul (Polynomial Fq) (RatFunc Fq)
(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached
Use `set_option synthInstance.maxHeartbeats <num>` to set the limit.
Contributor
Author
There was a problem hiding this comment.
I just ran lake exe runLinter Mathlib locally twice and confirmed that the above simpNF error occurs iff this @[simp] is present. I do not understand why.
Contributor
Author
There was a problem hiding this comment.
I asked about this here
Added a comment with a link there.
…d n K)` On further reflection, I have convinced myself it is best to avoid all possible refactoring while making the other changes in this PR.
alreadydone
approved these changes
Feb 2, 2025
Contributor
alreadydone
left a comment
There was a problem hiding this comment.
Thanks 🎉
maintainer delegate
|
🚀 Pull request has been placed on the maintainer queue by alreadydone. |
algebraMap_injective by weaking its typeclass assumptionsalgebraMap_injective by weakening its typeclass assumptions
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Member
|
Thanks! bors d+ |
Contributor
|
✌️ ocfnash can now approve this pull request. To approve and merge a pull request, simply reply with |
Contributor
Author
|
bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Feb 3, 2025
…sumptions (#21287) As shown in the new lemma `faithfulSMul_iff_algebraMap_injective`, injectivity of `algebraMap R A` is equivalent to the typeclass hypothesis `[FaithfulSMul R A]`. We thus generalise (and rename) the existing lemma `NoZeroSMulDivisors.algebraMap_injective` to `FaithfulSMul.algebraMap_injective`. The rename is responsible for much of the diff. By weakening the assumptions `[Nontrivial A] [NoZeroSMulDivisors R A]` to just `[FaithfulSMul R A]`, results which need to use `algebraMap_injective` can be applied in the case that we have `[Ring A] [CharZero A]` but fail to have `[NoZeroSMulDivisors ℤ A]`. This is the motivation for these changes. There are quite a few places in the library where a lemma consumes an explicit argument of the form `Injective (algebraMap R A)`. Most / all of these should probably be restated to accept the typeclass argument `[FaithfulSMul R A]` but we do not attempt such a refactor here. Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com>
Contributor
|
Pull request successfully merged into master. Build succeeded: |
algebraMap_injective by weakening its typeclass assumptionsalgebraMap_injective by weakening its typeclass assumptions
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
5 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.
As shown in the new lemma
faithfulSMul_iff_algebraMap_injective, injectivity ofalgebraMap R Ais equivalent to the typeclass hypothesis[FaithfulSMul R A]. We thus generalise (and rename) the existing lemmaNoZeroSMulDivisors.algebraMap_injectivetoFaithfulSMul.algebraMap_injective. The rename is responsible for much of the diff.By weakening the assumptions
[Nontrivial A] [NoZeroSMulDivisors R A]to just[FaithfulSMul R A], results which need to usealgebraMap_injectivecan be applied in the case that we have[Ring A] [CharZero A]but fail to have[NoZeroSMulDivisors ℤ A]. This is the motivation for these changes.There are quite a few places in the library where a lemma consumes an explicit argument of the form
Injective (algebraMap R A). Most / all of these should probably be restated to accept the typeclass argument[FaithfulSMul R A]but we do not attempt such a refactor here.