mathlib
0827a30c - feat(tactic/noncomm_ring): add noncomm_ring tactic (#2858)

Commit
5 years ago
feat(tactic/noncomm_ring): add noncomm_ring tactic (#2858) Fixes https://github.com/leanprover-community/mathlib/issues/2727 Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Oliver Nash
Parents
Loading