Theorems · Definition · group theory

FreeAddSemigroup.lift

{α : Type u} → {β : Type v} → [inst : AddSemigroup β] → (α → β) ≃ (FreeAddSemigroup α →ₙ+ β)

Lifts a function α → β to an additive semigroup homomorphism FreeAddSemigroup α → β given an additive semigroup β.

Defined in

Mathlib.Algebra.Free

Cited by

8 results in Mathlib

Foundations

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

Assumes

AddSemigroup