mathlib

6a7db279 - feat(tactic/ring_exp) allow ring_exp inside of conv blocks (#2369)

feat(tactic/ring_exp) allow ring_exp inside of conv blocks (#2369) * allow ring_exp inside of conv blocks * Update test/ring_exp.lean * Update test/ring_exp.lean * Update test/ring_exp.lean * add docstrings Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>