Theorems · Definition · group theory

IsUnit.unit

{M : Type u_1} → [inst : Monoid M] → {a : M} → IsUnit a → Mˣ

The element of the group of units, corresponding to an element of a monoid which is a unit. When α is a DivisionMonoid, use IsUnit.unit' instead.

Defined in

Mathlib.Algebra.Group.Units.Defs

Cited by

252 results in Mathlib

Foundations

Depth 10 from the axioms, rests on 42 definitions · uses Classical.choice

Assumes

Monoid