Free monoid over a given alphabet #
Main definitions #
FreeMonoid α
: free monoid over alphabetα
; defined as a synonym forList α
with multiplication given by(++)
.FreeMonoid.of
: embeddingα → FreeMonoid α
sending each elementx
to[x]
;FreeMonoid.lift
: natural equivalence betweenα → M
andFreeMonoid α →* M
FreeMonoid.map
: embedding ofα → β
intoFreeMonoid α →* FreeMonoid β
given byList.map
.
Free nonabelian additive monoid over a given alphabet
Instances For
The identity equivalence between FreeAddMonoid α
and List α
.
Instances For
The identity equivalence between FreeMonoid α
and List α
.
Instances For
The identity equivalence between List α
and FreeAddMonoid α
.
Instances For
The identity equivalence between List α
and FreeMonoid α
.
Instances For
Embeds an element of α
into FreeAddMonoid α
as a singleton list.
Instances For
Embeds an element of α
into FreeMonoid α
as a singleton list.
Instances For
Recursor for FreeAddMonoid
using 0
and
FreeAddMonoid.of x + xs
instead of []
and x :: xs
.
Instances For
Recursor for FreeMonoid
using 1
and FreeMonoid.of x * xs
instead of []
and x :: xs
.
Instances For
A version of List.casesOn
for FreeAddMonoid
using 0
and
FreeAddMonoid.of x + xs
instead of []
and x :: xs
.
Instances For
A version of List.cases_on
for FreeMonoid
using 1
and FreeMonoid.of x * xs
instead of
[]
and x :: xs
.
Instances For
A variant of List.sum
that has [x].sum = x
true definitionally.
The purpose is to make FreeAddMonoid.lift_eval_of
true by rfl
.
Instances For
A variant of List.prod
that has [x].prod = x
true definitionally.
The purpose is to make FreeMonoid.lift_eval_of
true by rfl
.
Instances For
Equivalence between maps α → A
and additive monoid homomorphisms
FreeAddMonoid α →+ A
.
Instances For
Equivalence between maps α → M
and monoid homomorphisms FreeMonoid α →* M
.
Instances For
Define an additive action of FreeAddMonoid α
on β
.
Instances For
Define a multiplicative action of FreeMonoid α
on β
.
Instances For
The unique additive monoid homomorphism FreeAddMonoid α →+ FreeAddMonoid β
that sends each of x
to of (f x)
.
Instances For
The unique monoid homomorphism FreeMonoid α →* FreeMonoid β
that sends
each of x
to of (f x)
.