Equivalence_of_Axiom_Schemata_for_Groups
Provedgroup-theoryproofwiki
In the definition of a group, the axioms for the existence of an identity element and closure under taking inverses can be replaced by the existence of a left identity and left inverses for all elements.
Preamble
import Mathlib.Algebra.Group.Defs
Formal statement
theorem Equivalence_of_Axiom_Schemata_for_Groups {G : Type _} [Mul G] (assoc : ∀ a b c : G, a * b * c = a * (b * c)) (e : G) (left_id : ∀ g : G, e * g = g) (left_inv : ∀ g : G, ∃ g' : G, g' * g = e) : (∀ g : G, g * e = g) ∧ (∀ g : G, ∃ g' : G, g * g' = e) := by sorrySource