Theorems · Definition · group theory

MulEquiv.subgroupMap

{G : Type u_1} →
  {G' : Type u_2} →
    [inst : Group G] → [inst_1 : Group G'] → (e : G ≃* G') → (H : Subgroup G) → ↥H ≃* ↥(Subgroup.map (↑e) H)

A subgroup is isomorphic to its image under an isomorphism. If you only have an injective map, use Subgroup.equivMapOfInjective.

Defined in

Mathlib.Algebra.Group.Subgroup.Map

Cited by

4 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Quot.sound

Assumes

GroupGroup