Theorems · Definition · group theory
IsUnit
{M : Type u_1} → [Monoid M] → M → PropAn element a : M of a Monoid is a unit if it has a two-sided inverse.
The actual definition says that a is equal to some u : Mˣ, where
Mˣ is a bundled version of IsUnit.
- Defined in
- Mathlib.Algebra.Group.Units.Defs
- Cited by
- 1,602 results in Mathlib
- Foundations
- Depth 3 from the axioms, rests on 6 definitions · uses no axioms
- Assumes
- Monoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by1,709
Results whose statement or proof uses this declaration.
- quasispectrumproof · cited by 292
- Primeproof · cited by 277
- IsUnit.unitstatement and proof · cited by 252
- Ring.inverseproof · cited by 160
- IsRelPrimeproof · cited by 136
- Units.isUnitstatement · cited by 116
- Squarefreeproof · cited by 112
- IsUnit.mapstatement and proof · cited by 104
- Ne.isUnitstatement · cited by 99
- IsStrictlyPositiveproof · cited by 75
- IsLocalization.map_unitsstatement · cited by 69
- IsUnit.submonoidproof · cited by 56
Showing the 200 most cited of 1,709.