Identity_Property_in_Semigroup
Provedidentity-elementsproofwikisemigroups
In a semigroup, if there exists an element s such that for all a there exist x, y with sx = a = ys, then the semigroup has an identity.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Identity_Property_in_Semigroup {S : Type _} [Semigroup S] (s : S) (h : ∀ a : S, ∃ x y : S, s * x = a ∧ y * s = a) : ∃ e : S, ∀ a : S, e * a = a ∧ a * e = a := by sorrySource