Zulip Chat Archive

Stream: Is there code for X?

Topic: add_sub_swap


view this post on Zulip Johan Commelin (Mar 08 2021 at 12:21):

example {G : Type*} [add_comm_group G] (x y z : G) : x + y - z = x - z + y :=
by library_search -- fails

view this post on Zulip Rob Lewis (Mar 08 2021 at 12:24):

by abel?

view this post on Zulip Rob Lewis (Mar 08 2021 at 12:25):

library_search says (sub_add_eq_add_sub x z y).symm

view this post on Zulip Johan Commelin (Mar 08 2021 at 12:28):

Hmm, my library search failed... sorry

view this post on Zulip Johan Commelin (Mar 08 2021 at 12:28):

Thanks for finding the proof


Last updated: May 17 2021 at 16:26 UTC