Theorems · Definition · group theory

FreeAddMonoid.lift

{α : Type u_1} → {M : Type u_4} → [inst : AddMonoid M] → (α → M) ≃ (FreeAddMonoid α →+ M)

Equivalence between maps α → A and additive monoid homomorphisms FreeAddMonoid α →+ A.

Defined in

Mathlib.Algebra.FreeMonoid.Basic

Cited by

24 results in Mathlib

Foundations

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

Assumes

AddMonoid