Theorems · Definition · group theory

Units.mkOfMulEqOne

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

For a, b in a Dedekind-finite monoid such that a * b = 1, makes a unit out of a.

Defined in

Mathlib.Algebra.Group.Units.Defs

Cited by

15 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

MonoidIsDedekindFiniteMonoid