Theorems · Definition · group theory

FreeAddGroup.lift

{α : Type u} → {β : Type v} → [inst : AddGroup β] → (α → β) ≃ (FreeAddGroup α →+ β)

If β is an additive group, then any function from α to β extends uniquely to an additive group homomorphism from the free additive group over α to β

Defined in

Mathlib.GroupTheory.FreeGroup.Basic

Cited by

18 results in Mathlib

Foundations

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

Assumes

AddGroup