Zulip Chat Archive

Stream: general

Topic: abelian failure


view this post on Zulip Johan Commelin (Feb 15 2019 at 10:48):

import tactic.abel

universe u

lemma foo (α : Type u) [comm_group α] (b d a c : α) : a * d = d * (b * (a * b⁻¹)) :=
by abel -- abel failed to simplify

lemma bar (α : Type u) [comm_group α] (b d a c : α) : a * d = d * (b * (a * b⁻¹)) :=
begin
  rw mul_comm,
  congr' 1,
  rw mul_left_comm,
  simp,
end

view this post on Zulip Johan Commelin (Feb 15 2019 at 11:43):

@Mario Carneiro Do you know what I'm doing wrong here?

view this post on Zulip Mario Carneiro (Feb 15 2019 at 11:47):

I think abel was never implemented on multiplicative groups

view this post on Zulip Kenny Lau (Feb 15 2019 at 11:49):

aren't they the same as additive groups? [insert mathematician's rant]

view this post on Zulip Johan Commelin (Feb 15 2019 at 11:50):

transfer to_additive; abel

view this post on Zulip Mario Carneiro (Feb 15 2019 at 11:50):

I think the intent was to use additive to do the translation, and I never got around to it

view this post on Zulip Mario Carneiro (Feb 15 2019 at 11:51):

But that better not actually be inverse in a field or I will be annoyed

view this post on Zulip Kevin Kappelmann (Sep 09 2019 at 12:29):

Any idea why abel fails for the second example here?

variables {α : Type*} {a : α}
open_locale add_monoid
example [add_comm_monoid α] : 1a + a = a + a := by abel -- works
example [add_comm_group α] : 1a + a = a + a := by abel -- fails

view this post on Zulip Keeley Hoek (Sep 09 2019 at 12:50):

Note that changing the second abel to repeat { abel } (i.e { abel, abel }) does work

view this post on Zulip Kevin Kappelmann (Sep 09 2019 at 13:03):

Interesting. How about this:

example [add_comm_group α] : 2a - (1a) = a := by abel -- fails

Last updated: May 06 2021 at 22:13 UTC