Mathlib Map

Theorems · Definition · group theory

Subgroup.toSubmonoid

{G : Type u_3} → [inst : Group G] → Subgroup G → Submonoid G

Reinterpret a Subgroup as a Submonoid.

Defined in
Mathlib.Algebra.Group.Subgroup.Defs
Cited by
114 results in Mathlib
Foundations
Depth 6 from the axioms, rests on 30 definitions · uses no axioms
Assumes
Group
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Subgroup.map · cited by 301Subgroup.mapSubgroup.comap · cited by 154Subgroup.comapSubgroup.prod · cited by 35Subgroup.prodSubgroup.ofUnits · cited by 31Subgroup.ofUnitspinGroup · cited by 25pinGroupSubgroup.pi · cited by 23Subgroup.piSubgroup.toAddSubgroup · cited by 20Subgroup.toAddSubgroupAddSubgroup.toSubgroup · cited by 15AddSubgroup.toSubgroupSubgroup.topologicalClosure · cited by 12Subgroup.topologicalClosu…Subgroup.subgroupOf_map_subtype · cited by 10Subgroup.subgroupOf_map_s…Subgroup.closure_toSubmonoid · cited by 9Subgroup.closure_toSubmon…MonoidHom.subgroupMap · cited by 8MonoidHom.subgroupMapSubgroup.eq_bot_iff_forall · cited by 7Subgroup.eq_bot_iff_forallIntermediateField.fixingSubgroup_isOpen · cited by 5IntermediateField.fixingS…Subgroup.fg_iff_submonoid_fg · cited by 5Subgroup.fg_iff_submonoid…Group · cited by 6238GroupSubgroup · cited by 3593SubgroupSubmonoid · cited by 3086SubmonoidSubgroup.toSubmonoidCITED BYCITES

Cites3

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Groupstatement and proof · cited by 6,238
  • Subgroupstatement and proof · cited by 3,593
  • Submonoidstatement · cited by 3,086

Cited by141

Results whose statement or proof uses this declaration.