Commit 2025-05-13 15:48 d8687ae1

View on Github →

chore: remove some simp attributes on lemmas that simp [*] can prove (#24851)

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean

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

modified theorem Real.rpow_ne_zero

Modified Mathlib/CategoryTheory/Comma/Arrow.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

Modified Mathlib/Data/Fin/Basic.lean

Modified Mathlib/Data/Finset/Card.lean

Modified Mathlib/Data/Int/Cast/Lemmas.lean

modified theorem Commute.intCast_mul_left

modified theorem Commute.intCast_mul_right

modified theorem SemiconjBy.intCast_mul_intCast_mul

Modified Mathlib/Data/Int/Init.lean

modified theorem Int.dvd_div_iff_mul_dvd

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Dynamics/PeriodicPts/Defs.lean

Modified Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean

Modified Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean

Modified Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses/Probability.lean

modified theorem MeasureTheory.prob_compl_eq_one_iff

modified theorem MeasureTheory.prob_compl_eq_zero_iff

Modified Mathlib/NumberTheory/FunctionField.lean

Modified Mathlib/Order/Basic.lean

Modified Mathlib/Order/Max.lean

Modified Mathlib/SetTheory/Cardinal/ToNat.lean