Tactic for CommGroup

Stream: Is there code for X?

[Alfredo Moreira-Rosa]

Hello, is there a tactic to solve goals on CommGroup (no addition) like ring for Semi-Ring ?

[Aaron Liu]

There's abel for AddCommGroup

[Alfredo Moreira-Rosa]

yeah, but mine is not abelian ...

[Aaron Liu]

ecyrbe said:

yeah, but mine is not abelian ...

But it's Commutative? As in CommGroup?

[Alfredo Moreira-Rosa]

yes, only has multiplication, commutative and associative

[Yaël Dillies]

It's sadly well known that abel only works for additive groups... PRs welcome and guidance offered though :slight_smile:

[Aaron Liu]

ecyrbe said:

yes, only has multiplication, commutative and associative

That would be a CommSemigroup, which I usually use ac_rfl for

[Alfredo Moreira-Rosa]

it's a full comm group, it has inversion and division

[Alfredo Moreira-Rosa]

let me try ac_rfl

[Alfredo Moreira-Rosa]

...no luck, not enough

[Alfredo Moreira-Rosa]

I just realised that i can just redefine my multiplication as an addition operator and get an AddCommGroup, and then use moduleor abel tactics to solve the goals.