Zulip Chat Archive

Stream: general

Topic: alternating_sum lemmas (was: Canonical form for "n is even")


Reid Barton (Aug 22 2020 at 09:33):

I would guess that simp will already simplify x - (y - z) to x - y + z, so there's no need for _cons_cons'

Chris Wong (Aug 22 2020 at 10:04):

You'd think so, but I've been surprised by how little simp does for add_comm_group. Here, simp fails, and library_search suggests sub_add reversed:

import algebra.group.basic

example {G : Type*} [add_comm_group G] (x y z : G) : x - (y - z) = x - y + z :=
begin
  rw  sub_add,
end

Scott Morrison (Aug 22 2020 at 10:09):

You know about abel?

Chris Wong (Aug 22 2020 at 10:13):

... I did not. Thanks for the suggestion :laughing:


Last updated: Dec 20 2023 at 11:08 UTC