Zulip Chat Archive

Stream: Is there code for X?

Topic: mulabel


view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip 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