Stream: new members

Topic: Basic algebraic operations

YH (Dec 13 2019 at 20:17):

What's a better way to do something like 3 * m + m by 4 * m?
right now I'm doing 3 * m + m = 3 * m + 1 * m = (3+1) * m = 4 * m.

Kevin Buzzard (Dec 13 2019 at 20:23):

the ring tactic proves this immediately, assuming m is in a semiring.

YH (Dec 13 2019 at 20:30):

I tried ring already, but what I had was h : x ≤ 3 * m + m, and ring doesn't seem work for that?

Kevin Buzzard (Dec 13 2019 at 20:31):

then rw (show 3 * m + m = 4 * m, by ring)

YH (Dec 13 2019 at 20:32):

OK thanks.

Last updated: May 16 2021 at 05:21 UTC