## Stream: general

### Topic: abelian failure

#### 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


#### Johan Commelin (Feb 15 2019 at 11:43):

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

#### Mario Carneiro (Feb 15 2019 at 11:47):

I think abel was never implemented on multiplicative groups

#### Kenny Lau (Feb 15 2019 at 11:49):

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

#### Johan Commelin (Feb 15 2019 at 11:50):

transfer to_additive; abel

#### 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

#### Mario Carneiro (Feb 15 2019 at 11:51):

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

#### Kevin Kappelmann (Sep 09 2019 at 12:29):

Any idea why abel fails for the second example here?

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


#### Keeley Hoek (Sep 09 2019 at 12:50):

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

#### Kevin Kappelmann (Sep 09 2019 at 13:03):

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


Last updated: May 06 2021 at 22:13 UTC