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