mathlib3
18a80ea2 - chore(tactic/noncomm_ring): allow simp to fail (#3268)

Commit

6 years ago

chore(tactic/noncomm_ring): allow simp to fail (#3268) Fixes #3267. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author

kim-em

Parents