Theorems · Definition · group theory

AddSubgroup.equivMapOfInjective

{G : Type u_1} →
  [inst : AddGroup G] →
    {N : Type u_5} →
      [inst_1 : AddGroup N] → (H : AddSubgroup G) → (f : G →+ N) → Function.Injective ⇑f → ↥H ≃+ ↥(AddSubgroup.map f H)

An additive subgroup is isomorphic to its image under an injective function. If you have an isomorphism, use AddEquiv.addSubgroupMap for better definitional equalities.

Defined in

Mathlib.Algebra.Group.Subgroup.Map

Cited by

3 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Classical.choice

Assumes

AddGroupAddGroup