## Stream: Is there code for X?

### Topic: mulabel

#### Kevin Buzzard (Jul 23 2020 at 09:09):

import tactic

example (G : Type) [add_comm_group G] (a b : G) :
a + b + -a + -b = 0 :=
begin
abel,
end

example (G : Type) [comm_group G] (a b : G) :
a * b * a⁻¹ * b⁻¹ = 1 :=
begin
-- now what?
sorry
end


#### Johan Commelin (Jul 23 2020 at 09:10):

Pretty clear right? You just push things to the group ring, and use ring :grinning_face_with_smiling_eyes:

#### Johan Commelin (Jul 23 2020 at 09:11):

More seriously, I guess you can apply additive.of_mul_injective or something like that, and then simp; abel. Even more seriously... this should be fixed in abel.

Last updated: May 19 2021 at 03:22 UTC