(a * b) * c * d = (d * (b * c)) * a

Stream: maths

[Johan Commelin]

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]

I guess there is room for a perm tactic that takes a assoc comm operator, and proves that two permutations are equal.

[Chris Hughes]

simp [mul_comm, mul_assoc, mul_left_comm] is fairly reliable.

[Kevin Buzzard]

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]

Thanks @Chris Hughes! That works like a charm!