Theorems · Definition · group theory

MonoidHom.subgroupComap

{G : Type u_1} →
  {G' : Type u_2} →
    [inst : Group G] → [inst_1 : Group G'] → (f : G →* G') → (H' : Subgroup G') → ↥(Subgroup.comap f H') →* ↥H'

The MonoidHom from the preimage of a subgroup to itself.

Defined in

Mathlib.Algebra.Group.Subgroup.Map

Cited by

2 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext

Assumes

GroupGroup