Theorems · Definition · group theory

FreeSemigroup.lift

{α : Type u} → {β : Type v} → [inst : Semigroup β] → (α → β) ≃ (FreeSemigroup α →ₙ* β)

Lifts a function α → β to a semigroup homomorphism FreeSemigroup α → β given a semigroup β.

Defined in

Mathlib.Algebra.Free

Cited by

8 results in Mathlib

Foundations

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

Assumes

Semigroup