Def Mathlib.Tactic.Ring.Common.ExProd.toSum

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) …

Added Mathlib.Tactic.Ring.Common.ExProd.toSum View on Github →