Theorems · Definition · group theory
Submonoid.units
{M : Type u_1} → [inst : Monoid M] → Submonoid M → Subgroup MˣThe units of S, packaged as a subgroup of Mˣ.
- Defined in
- Mathlib.Algebra.Group.Submonoid.Units
- Cited by
- 40 results in Mathlib
- Foundations
- Depth 23 from the axioms · uses propext
- Assumes
- Monoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Monoidstatement and proof · cited by 3,887
- Subgroupstatement · cited by 3,593
- Submonoidstatement and proof · cited by 3,086
- Unitsstatement and proof · cited by 2,804
- Submonoid.comapproof · cited by 179
- Units.coeHomproof · cited by 44
Cited by46
Results whose statement or proof uses this declaration.
- ofUnits_units_gcstatement · cited by 11
- ofUnits_units_gcistatement · cited by 10
- Submonoid.unitsEquivUnitsTypestatement and proof · cited by 8
- RestrictedProduct.unitsEquivstatement and proof · cited by 3
- MulChar.domRestrict_ofUnitHomstatement and proof · cited by 2
- MulChar.domRestrictHom_surjectiveproof · cited by 1
- Submonoid.unitsEquivIsUnitSubmonoidstatement · cited by 1
- Submonoid.val_unitsEquivUnitsType_symm_apply_coestatement · cited by 1
- Submonoid.mem_units_of_val_mem_inv_val_memstatement · cited by 1
- IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_onestatement and proof · cited by 1
- RestrictedProduct.unitsEquiv_applystatement · cited by 0
- Submonoid.mul_mem_unitsstatement and proof · cited by 0