Theorems · Definition · group theory

FreeAddGroupBasis.lift

{ι : Type u_1} →
  {G : Type u_3} →
    {H : Type u_4} → [inst : AddGroup G] → [inst_1 : AddGroup H] → FreeAddGroupBasis ι G → (ι → H) ≃ (G →+ H)

Given an additive free group basis of G over ι, there is a canonical bijection between maps from ι to an additive group H and morphisms from G to H.

Defined in

Mathlib.GroupTheory.FreeGroup.IsFreeGroup

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddGroupAddGroup