Mathlib Map

Theorems · Definition · group theory

AddSubgroup.toAddSubmonoid

{G : Type u_3} → [inst : AddGroup G] → AddSubgroup G → AddSubmonoid G

Reinterpret an AddSubgroup as an AddSubmonoid.

Defined in
Mathlib.Algebra.Group.Subgroup.Defs
Cited by
91 results in Mathlib
Foundations
Depth 6 from the axioms · uses no axioms
Assumes
AddGroup
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

AddSubgroup.map · cited by 189AddSubgroup.mapAddSubgroup.comap · cited by 123AddSubgroup.comapAddSubgroup.prod · cited by 34AddSubgroup.prodAddSubgroup.ofAddUnits · cited by 30AddSubgroup.ofAddUnitsAddSubgroup.pi · cited by 26AddSubgroup.piAddSubgroup.toIntSubmodule · cited by 25AddSubgroup.toIntSubmoduleSubgroup.toAddSubgroup · cited by 20Subgroup.toAddSubgroupAddSubgroup.topologicalClosure · cited by 16AddSubgroup.topologicalCl…AddSubgroup.toSubgroup · cited by 15AddSubgroup.toSubgroupAddSubgroup.eq_bot_iff_forall · cited by 11AddSubgroup.eq_bot_iff_fo…PointedCone.lineal · cited by 10PointedCone.linealRingPreordering.support · cited by 9RingPreordering.supportselfAdjoint.submodule · cited by 9selfAdjoint.submoduleValuation.leIdeal · cited by 7Valuation.leIdealValuation.leSubmodule · cited by 7Valuation.leSubmoduleAddGroup · cited by 4410AddGroupAddSubgroup · cited by 3232AddSubgroupAddSubmonoid · cited by 1178AddSubmonoidAddSubgroup.toAddSubmonoidCITED BYCITES

Cites3

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

Cited by135

Results whose statement or proof uses this declaration.