mathlib3

c1ada9d1 - fix(tactic/ring): perform definitional rather than syntactic matches on `^` (#18156)

fix(tactic/ring): perform definitional rather than syntactic matches on `^` (#18156) This code is copied from a similar pattern for `has_div.div` a few lines up. Follows on from #18129