Theorem Mathlib.Tactic.Ring.Int.smul_eq_mul

Modification history

2026-05-24 07:15
Mathlib/Tactic/Ring/Basic.lean
perf: shortcut instances for `Semiring` (#39719) …
Modified Mathlib.Tactic.Ring.Int.smul_eq_mulView on Github →
2026-04-06 00:30
Mathlib/Tactic/Ring/Basic.lean
refactor(Tactic): change `ring` to allow for coefficients in a variable type (#34734) …
Added Mathlib.Tactic.Ring.Int.smul_eq_mulView on Github →