Mathlib Map

Theorems · Definition · group theory

AddSubgroup.subtype

{G : Type u_1} → [inst : AddGroup G] → (H : AddSubgroup G) → ↥H →+ G

The natural group hom from an AddSubgroup of AddGroup G to G.

Defined in
Mathlib.Algebra.Group.Subgroup.Defs
Cited by
82 results in Mathlib
Foundations
Depth 22 from the axioms · uses propext
Assumes
AddGroup
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

AddSubgroup.addSubgroupOf · cited by 87AddSubgroup.addSubgroupOfSubring.subtype · cited by 22Subring.subtypeAddSubgroup.range_subtype · cited by 16AddSubgroup.range_subtypeSubfield.subtype · cited by 16Subfield.subtypeAddSubgroup.subtype_injective · cited by 10AddSubgroup.subtype_injec…AddSubgroup.goursatFst · cited by 8AddSubgroup.goursatFstAddSubgroup.goursatSnd · cited by 8AddSubgroup.goursatSndCategoryTheory.ShortComplex.abLeftHomologyData · cited by 7ShortComplex.abLeftHomolo…AddSubgroup.relIndex_comap · cited by 7AddSubgroup.relIndex_comapAddSubgroup.noncommPiCoprod · cited by 5AddSubgroup.noncommPiCopr…AddSubgroup.addSubgroupOf_map_subtype · cited by 5AddSubgroup.addSubgroupOf…MeasureTheory.Lp.simpleFunc.coeToLp · cited by 5simpleFunc.coeToLpAddSubgroup.top_subtype_lowerCentralSeries · cited by 4AddSubgroup.top_subtype_l…AddSubgroup.map_subtype_inj · cited by 4AddSubgroup.map_subtype_i…AddSubgroup.isAddCyclic_iff_exists_zmultiples_eq_top · cited by 4AddSubgroup.isAddCyclic_i…AddGroup · cited by 4410AddGroupAddSubgroup · cited by 3232AddSubgroupAddMonoidHom · cited by 3230AddMonoidHomAddSubgroup.subtypeCITED BYCITES

Cites3

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

Cited by99

Results whose statement or proof uses this declaration.