Def Mathlib.Tactic.RingNF.rewrite

Modification history

2022-11-15 22:02

Mathlib/Tactic/Ring/RingNF.lean

feat: refactoring RingNF, `ring1_nf` tactic (#601) …

Added Mathlib.Tactic.RingNF.rewrite View on Github →