Stream: new members
Topic: Basic algebraic operations
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):
ring tactic proves this immediately, assuming m is in a semiring.
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):
rw (show 3 * m + m = 4 * m, by ring)
Last updated: May 16 2021 at 05:21 UTC