Mathlib Map

Theorems · Definition · group theory

Subgroup.subtype

{G : Type u_1} → [inst : Group G] → (H : Subgroup G) → ↥H →* G

The natural group hom from a subgroup of group G to G.

Defined in
Mathlib.Algebra.Group.Subgroup.Defs
Cited by
185 results in Mathlib
Foundations
Depth 22 from the axioms, rests on 183 definitions · uses propext
Assumes
Group
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Subgroup.subgroupOf · cited by 122Subgroup.subgroupOfMonoidWithZeroHom.ValueGroup₀.embedding · cited by 47ValueGroup₀.embeddingSubgroup.range_subtype · cited by 28Subgroup.range_subtypeSubgroup.subtype_injective · cited by 18Subgroup.subtype_injectiveRep.indCoindIso · cited by 13Rep.indCoindIsoSubgroup.noncommPiCoprod · cited by 12Subgroup.noncommPiCoprodMonoidWithZeroHom.ValueGroup₀.embedding_restrict₀ · cited by 12ValueGroup₀.embedding_res…Subgroup.map_subtype_inj · cited by 11Subgroup.map_subtype_injSubgroup.subgroupOf_map_subtype · cited by 10Subgroup.subgroupOf_map_s…Sylow.subtype · cited by 10Sylow.subtypeRep.coinvariantsShortComplex · cited by 8Rep.coinvariantsShortComp…Subgroup.relIndex_comap · cited by 7Subgroup.relIndex_comapSubgroup.map_subtype_commutator · cited by 7Subgroup.map_subtype_comm…groupHomology.H1CoresCoinfOfTrivial · cited by 7groupHomology.H1CoresCoin…Rep.coindToInd · cited by 6Rep.coindToIndGroup · cited by 6238GroupMonoidHom · cited by 3629MonoidHomSubgroup · cited by 3593SubgroupSubgroup.subtypeCITED 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
  • MonoidHomstatement · cited by 3,629
  • Subgroupstatement and proof · cited by 3,593

Cited by232

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 232.