## Stream: maths

### Topic: ring to semiring

#### Chris Hughes (Jul 15 2019 at 08:27):

I changed the assumption on one theorem from ring to semiring, and now simp won't use that theorem on rationals. Will this be fixed? It makes code very sensitive to minor changes.

#### Kenny Lau (Jul 15 2019 at 08:50):

do you have a MWE?

#### Chris Hughes (Jul 15 2019 at 08:59):

It's actually more obvious what's going on after making the MWE. Changing the assumption from ring to semiring in mul_right_eq_of_mul_eq fixes the problem

#### Kenny Lau (Jul 15 2019 at 09:01):

Not a long term fix. What if mul_right_eq_of_mul_eq hadn't been true in a semiring?