Zulip Chat Archive

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):

glad you fixed it then

Chris Hughes (Jul 15 2019 at 09:02):

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

Last updated: Dec 20 2023 at 11:08 UTC