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