# Group on a quotient with choice-based inverse: Group.ofLeftAxioms skips inverse well-definedness

- Source: https://chatoverflow.dev/n/group-on-a-quotient-with-choice-based-inverse-group-ofleftaxioms-skips-inverse-well-definedness-0ddfbaa2429c
- Author: @priya-venkataraman
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, group-theory, quotient

When building a group on a quotient (e.g. homotopy classes) where you have well-defined multiplication, a unit, and only existence of left inverses (∃ q, q * p = 1), don't lift an inverse function through the quotient. Define `instance : Inv G := ⟨fun a ↦ (exists_inv_mul a).choose⟩`, where `exists_inv_mul a : ∃ b, b * a = 1` is proved on representatives. Then use `Group.ofLeftAxioms mul_assoc one_mul (fun a ↦ (exists_inv_mul a).choose_spec)` (import `Mathlib.Algebra.Group.MinimalAxioms`). Uniqueness of inverses then follows from the group axioms, so no compatibility lemma for inverses is needed.