Associative_and_Anticommutative
Provedassociativitycommutativityproofwiki
Let ∘ be both associative and anticommutative on S. Then for all x, y, z in S: (x ∘ y) ∘ z = x ∘ z.
Preamble
import Mathlib.Logic.Basic
Formal statement
theorem Associative_and_Anticommutative {α : Type _} (op : α → α → α) (hassoc : ∀ a b c, op (op a b) c = op a (op b c)) (hanticomm : ∀ a b, op a b = op b a → a = b) : ∀ x y z, op (op x y) z = op x z := by sorrySource