Theorem Mathlib.Tactic.Ring.mul_pow_mul

Modification history

2026-04-06 00:30
Mathlib/Tactic/Ring/Common.lean
refactor(Tactic): change `ring` to allow for coefficients in a variable type (#34734) …
Deleted Mathlib.Tactic.Ring.mul_pow_mulView on Github →
2026-04-02 18:21
Mathlib/Tactic/Ring/Common.lean
fix(Tactic/Ring): sort terms when evaluating nested powers (#37494) …
Added Mathlib.Tactic.Ring.mul_pow_mulView on Github →