Commit 2025-12-02 16:24 1472a119

View on Github →

chore: deprecate Algebra.id.smul_eq_mul (#32346) smul_eq_mul is more general, is defined earlier, and has a shorter name.

Estimated changes

Modified Archive/Wiedijk100Theorems/FriendshipGraphs.lean

Modified Mathlib/Algebra/Algebra/Defs.lean

Modified Mathlib/Algebra/Algebra/Spectrum/Basic.lean

Modified Mathlib/Algebra/Module/PID.lean

Modified Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean

Modified Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean

Modified Mathlib/Analysis/Calculus/FormalMultilinearSeries.lean

Modified Mathlib/Analysis/Calculus/LagrangeMultipliers.lean

Modified Mathlib/Analysis/Complex/RemovableSingularity.lean

Modified Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/Analysis/InnerProductSpace/Dual.lean

Modified Mathlib/Analysis/InnerProductSpace/TwoDim.lean

Modified Mathlib/Analysis/LocallyConvex/Polar.lean

Modified Mathlib/Analysis/LocallyConvex/Separation.lean

Modified Mathlib/Analysis/Normed/Module/HahnBanach.lean

Modified Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean

Modified Mathlib/Analysis/SpecialFunctions/Integrability/Basic.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean

Modified Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean

Modified Mathlib/LinearAlgebra/Contraction.lean

Modified Mathlib/LinearAlgebra/Determinant.lean

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

Modified Mathlib/LinearAlgebra/PiTensorProduct.lean

Modified Mathlib/LinearAlgebra/Trace.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/Set.lean

Modified Mathlib/MeasureTheory/Integral/CircleIntegral.lean

Modified Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

Modified Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

Modified Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

Modified Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean

Modified Mathlib/NumberTheory/WellApproximable.lean

Modified Mathlib/Probability/BorelCantelli.lean

Modified Mathlib/Probability/Distributions/Uniform.lean

Modified Mathlib/Probability/StrongLaw.lean

Modified Mathlib/RingTheory/AdicCompletion/Algebra.lean

Modified Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean

Modified Mathlib/RingTheory/AdicCompletion/Basic.lean

Modified Mathlib/RingTheory/Adjoin/PowerBasis.lean

Modified Mathlib/RingTheory/Conductor.lean

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

Modified Mathlib/RingTheory/Derivation/Lie.lean

Modified Mathlib/RingTheory/DividedPowers/Basic.lean

Modified Mathlib/RingTheory/DividedPowers/SubDPIdeal.lean

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

Modified Mathlib/RingTheory/Ideal/Cotangent.lean

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

Modified Mathlib/RingTheory/MvPowerSeries/Basic.lean

Modified Mathlib/RingTheory/Nullstellensatz.lean

Modified Mathlib/RingTheory/Polynomial/Bernstein.lean

Modified Mathlib/RingTheory/Trace/Basic.lean

Modified Mathlib/RingTheory/WittVector/Isocrystal.lean

Modified Mathlib/Topology/Algebra/Module/CharacterSpace.lean

Modified Mathlib/Topology/ContinuousMap/Algebra.lean

Modified Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean

Modified MathlibTest/instance_diamonds.lean