Theorems · Definition · ring theory

invertibleOfRightInverse

{α : Type u} → [inst : Monoid α] → [IsDedekindFiniteMonoid α] → (a b : α) → a * b = 1 → Invertible a

An element in a Dedekind-finite monoid is invertible if it has a right inverse.

Defined in

Mathlib.Algebra.Group.Invertible.Defs

Cited by

0 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

MonoidIsDedekindFiniteMonoid