mathlib
a7b4018a - fix(tactic/ring): bugfixes in ring_nf (#10572)

Commit
4 years ago
fix(tactic/ring): bugfixes in ring_nf (#10572) As reported by @hrmacbeth: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60ring_nf.60.20behaves.20strangely.20with.20def.20in.20original.20goal Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Author
Parents
Loading