Commit 2025-10-31 08:48 1d1224bd

View on Github →

chore: deprecate Mul.toSMul in favour of lean4 instance (#31040)

Estimated changes

Modified Mathlib/Algebra/Algebra/Defs.lean

Modified Mathlib/Algebra/Group/Action/Defs.lean

added def Mul.toSMul

Modified Mathlib/RingTheory/Kaehler/Basic.lean

Modified MathlibTest/instance_diamonds.lean