Group_has_Latin_Square_Property
Provedgroup-has-latin-square-propertygroup-theoryproofwiki
Let (G, *) be a group. Then for all a, b in G, there exists a unique g in G such that a * g = b, and a unique h in G such that h * a = b.
Preamble
import Mathlib.Algebra.Group.Basic
Formal statement
theorem Group_has_Latin_Square_Property {G : Type _} [Group G] (a b : G) : (∃! g : G, a * g = b) ∧ (∃! h : G, h * a = b) := by sorrySource