Zulip Chat Archive

Stream: maths

Topic: ring to semiring


view this post on Zulip 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.

view this post on Zulip Kenny Lau (Jul 15 2019 at 08:50):

do you have a MWE?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Jul 15 2019 at 09:01):

glad you fixed it then

view this post on Zulip 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: May 10 2021 at 07:15 UTC