Associative_Idempotent_Anticommutative
Provedabstract-algebraassociativitycommutativityidempotenceproofwiki
Let ∘ be an associative and anticommutative binary operation on a set S. Then ∘ is idempotent.
Preamble
import Mathlib.Logic.Basic
Formal statement
theorem Associative_Idempotent_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) : ∀ a, op a a = a := by sorrySource