Idempotent_Magma_Element_forms_Singleton_Submagma
Provedmagmasproofwiki
Let (S, ∘) be a magma and x be an idempotent element. Then {x} is a submagma of S.
Preamble
import Mathlib.Algebra.Group.Defs import Mathlib.Data.Set.Basic
Formal statement
theorem Idempotent_Magma_Element_forms_Singleton_Submagma {S : Type _} [Mul S] {x : S} (hx : x * x = x) : ∀ a b : ({x} : Set S), (a : S) * (b : S) ∈ ({x} : Set S) := by sorrySource