# Zulip Chat Archive

## Stream: maths

### Topic: (a * b) * c * d = (d * (b * c)) * a

#### Johan Commelin (Feb 11 2019 at 17:54):

What is the fastest way to prove such a statement in an arbitrary structure with associative and commutative multiplication? I am currently in a `with_zero G`

where `G`

is a comm_group. That prevents me from using `abel`

or such.

#### Johan Commelin (Feb 11 2019 at 17:55):

I guess there is room for a `perm`

tactic that takes a assoc comm operator, and proves that two permutations are equal.

#### Chris Hughes (Feb 11 2019 at 18:02):

`simp [mul_comm, mul_assoc, mul_left_comm]`

is fairly reliable.

#### Kevin Buzzard (Feb 11 2019 at 18:05):

When Kenny and I were faced with stuff like this we were doing cases on it; if a = 0 then both sides are 0 and if not then a = some a; now case on b and kill the zero case; etc. When all zero cases are killed, `change`

to `some ((a * b) * c * d) = ...`

, apply injectivity of `some`

and then use `abel`

. But if Chris' technique works that would be great. I guess your monoid isn't even cancellative though.

#### Johan Commelin (Feb 11 2019 at 18:18):

Thanks @Chris Hughes! That works like a charm!

Last updated: May 06 2021 at 17:38 UTC