Zulip Chat Archive

Stream: general

Topic: ring with natural number division


Chris Hughes (Oct 16 2019 at 11:54):

Is ring supposed to solve this goal? The n / 2 should be treated as atoms right?

example (n : ) : (n / 2) + (n / 2) = 2 * (n / 2) := by ring --fails

Kenny Lau (Oct 16 2019 at 12:03):

but N isn't a ring

Chris Hughes (Oct 16 2019 at 12:04):

ring is supposed to work with commutative semirings I believe.

Mario Carneiro (Oct 16 2019 at 14:09):

#1557


Last updated: Dec 20 2023 at 11:08 UTC