Theorems · Definition · group theory

AddEquiv.addSubgroupMap

{G : Type u_1} →
  {G' : Type u_2} →
    [inst : AddGroup G] → [inst_1 : AddGroup G'] → (e : G ≃+ G') → (H : AddSubgroup G) → ↥H ≃+ ↥(AddSubgroup.map (↑e) H)

An additive subgroup is isomorphic to its image under an isomorphism. If you only have an injective map, use AddSubgroup.equivMapOfInjective.

Defined in

Mathlib.Algebra.Group.Subgroup.Map

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddGroupAddGroup