Zulip Chat Archive
Stream: Is there code for X?
Topic: add_sub_swap
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
Rob Lewis (Mar 08 2021 at 12:24):
by abel?
Rob Lewis (Mar 08 2021 at 12:25):
library_search says (sub_add_eq_add_sub x z y).symm
Johan Commelin (Mar 08 2021 at 12:28):
Hmm, my library search failed... sorry
Johan Commelin (Mar 08 2021 at 12:28):
Thanks for finding the proof
Last updated: Dec 20 2023 at 11:08 UTC