Invertible_Elements_of_Monoid_form_Subgroup_of_Cancellable_Elements
Provedcancellabilitygroup-theorymonoidsproofwiki
The invertible elements of a monoid form a subgroup of the cancellable elements.
Preamble
import Mathlib.Algebra.Group.Units.Basic
Formal statement
theorem Invertible_Elements_of_Monoid_form_Subgroup_of_Cancellable_Elements {M : Type _} [Monoid M] (a : M) (ha : IsUnit a) : (∀ x y : M, a * x = a * y → x = y) ∧ (∀ x y : M, x * a = y * a → x = y) := by sorrySource