Documentation

Mathlib.Algebra.FreeMonoid.Basic

Free monoid over a given alphabet #

Main definitions #

def FreeMonoid (α : Type u_6) :
Type u_6

If α is a type, then FreeMonoid α is the free monoid generated by α. This is a monoid equipped with a function FreeMonoid.of : α → FreeMonoid α which has the following universal property: if M is any monoid, and f : α → M is any function, then this function is the composite of FreeMonoid.of and a unique monoid homomorphism FreeMonoid.lift f : FreeMonoid α →* M.

A typical element of FreeMonoid α is a formal product of elements of α. For example if x and y are terms of type α then x * y * y * x is a "typical" element of FreeMonoid α. In particular if α is empty then FreeMonoid α is isomorphic to the trivial monoid, and if α has one term then FreeMonoid α is isomorphic to Multiplicative ℕ. If α has two or more terms then FreeMonoid α is not commutative. One can think of FreeMonoid α as the type of lists of α, with multiplication given by concatenation.

Equations
def FreeAddMonoid (α : Type u_6) :
Type u_6

If α is a type, then FreeAddMonoid α is the free additive monoid generated by α. This is a monoid equipped with a function FreeAddMonoid.of : α → FreeAddMonoid α which has the following universal property: if M is any monoid, and f : α → M is any function, then this function is the composite of FreeAddMonoid.of and a unique monoid homomorphism FreeAddMonoid.lift f : FreeAddMonoid α →+ M.

A typical element of FreeAddMonoid α is a formal sum of elements of α. For example if x and y are terms of type α then x + y + y + x is a "typical" element of FreeAddMonoid α. In particular if α is empty then FreeAddMonoid α is isomorphic to the trivial monoid, and if α has one term then FreeAddMonoid α is isomorphic to . If α has two or more terms then FreeAddMonoid α is not commutative. One can think of FreeAddMonoid α as the type of lists of α, with addition given by concatenation.

Equations
def FreeMonoid.toList {α : Type u_1} :

The identity equivalence between FreeMonoid α and List α.

Equations

The identity equivalence between FreeAddMonoid α and List α.

Equations
def FreeMonoid.ofList {α : Type u_1} :

The identity equivalence between List α and FreeMonoid α.

Equations

The identity equivalence between List α and FreeAddMonoid α.

Equations
@[simp]
@[simp]
@[simp]
theorem FreeMonoid.toList_ofList {α : Type u_1} (l : List α) :
@[simp]
theorem FreeAddMonoid.toList_ofList {α : Type u_1} (l : List α) :
@[simp]
theorem FreeMonoid.ofList_toList {α : Type u_1} (xs : FreeMonoid α) :
ofList (toList xs) = xs
@[simp]
theorem FreeAddMonoid.ofList_toList {α : Type u_1} (xs : FreeAddMonoid α) :
ofList (toList xs) = xs
@[simp]
@[simp]
@[simp]
@[simp]
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
@[simp]
theorem FreeMonoid.toList_one {α : Type u_1} :
@[simp]
theorem FreeAddMonoid.toList_zero {α : Type u_1} :
@[simp]
theorem FreeMonoid.ofList_nil {α : Type u_1} :
@[simp]
theorem FreeAddMonoid.ofList_nil {α : Type u_1} :
@[simp]
theorem FreeMonoid.toList_nil {α : Type u_1} :
@[simp]
@[simp]
theorem FreeMonoid.toList_cons {α : Type u_1} (x : α) (xs : FreeMonoid α) :
toList (x :: xs) = x :: toList xs
@[simp]
theorem FreeAddMonoid.toList_cons {α : Type u_1} (x : α) (xs : FreeAddMonoid α) :
toList (x :: xs) = x :: toList xs
@[simp]
theorem FreeMonoid.toList_mul {α : Type u_1} (xs ys : FreeMonoid α) :
toList (xs * ys) = toList xs ++ toList ys
@[simp]
theorem FreeAddMonoid.toList_add {α : Type u_1} (xs ys : FreeAddMonoid α) :
toList (xs + ys) = toList xs ++ toList ys
@[simp]
theorem FreeMonoid.ofList_append {α : Type u_1} (xs ys : List α) :
ofList (xs ++ ys) = ofList xs * ofList ys
@[simp]
theorem FreeAddMonoid.ofList_append {α : Type u_1} (xs ys : List α) :
ofList (xs ++ ys) = ofList xs + ofList ys
@[simp]
theorem FreeMonoid.toList_prod {α : Type u_1} (xs : List (FreeMonoid α)) :
@[simp]
theorem FreeAddMonoid.toList_sum {α : Type u_1} (xs : List (FreeAddMonoid α)) :
@[simp]
theorem FreeMonoid.ofList_flatten {α : Type u_1} (xs : List (List α)) :
@[simp]
theorem FreeAddMonoid.ofList_flatten {α : Type u_1} (xs : List (List α)) :
def FreeMonoid.of {α : Type u_1} (x : α) :

Embeds an element of α into FreeMonoid α as a singleton list.

Equations
def FreeAddMonoid.of {α : Type u_1} (x : α) :

Embeds an element of α into FreeAddMonoid α as a singleton list.

Equations
@[simp]
theorem FreeMonoid.toList_of {α : Type u_1} (x : α) :
toList (of x) = [x]
@[simp]
theorem FreeAddMonoid.toList_of {α : Type u_1} (x : α) :
toList (of x) = [x]
theorem FreeMonoid.ofList_singleton {α : Type u_1} (x : α) :
theorem FreeAddMonoid.ofList_singleton {α : Type u_1} (x : α) :
@[simp]
theorem FreeMonoid.ofList_cons {α : Type u_1} (x : α) (xs : List α) :
ofList (x :: xs) = of x * ofList xs
@[simp]
theorem FreeAddMonoid.ofList_cons {α : Type u_1} (x : α) (xs : List α) :
ofList (x :: xs) = of x + ofList xs
theorem FreeMonoid.toList_of_mul {α : Type u_1} (x : α) (xs : FreeMonoid α) :
toList (of x * xs) = x :: toList xs
theorem FreeAddMonoid.toList_of_add {α : Type u_1} (x : α) (xs : FreeAddMonoid α) :
toList (of x + xs) = x :: toList xs

Length #

def FreeMonoid.length {α : Type u_1} (a : FreeMonoid α) :

The length of a free monoid element: 1.length = 0 and (a * b).length = a.length + b.length

Equations
def FreeAddMonoid.length {α : Type u_1} (a : FreeAddMonoid α) :

The length of an additive free monoid element: 1.length = 0 and (a + b).length = a.length + b.length

Equations
@[simp]
theorem FreeMonoid.length_one {α : Type u_1} :
length 1 = 0
@[simp]
theorem FreeAddMonoid.length_zero {α : Type u_1} :
length 0 = 0
@[simp]
theorem FreeMonoid.length_eq_zero {α : Type u_1} {a : FreeMonoid α} :
a.length = 0 a = 1
@[simp]
theorem FreeAddMonoid.length_eq_zero {α : Type u_1} {a : FreeAddMonoid α} :
a.length = 0 a = 0
@[simp]
theorem FreeMonoid.length_of {α : Type u_1} (m : α) :
(of m).length = 1
@[simp]
theorem FreeAddMonoid.length_of {α : Type u_1} (m : α) :
(of m).length = 1
theorem FreeMonoid.length_eq_one {α : Type u_1} {a : FreeMonoid α} :
a.length = 1 (m : α), a = of m
theorem FreeAddMonoid.length_eq_one {α : Type u_1} {a : FreeAddMonoid α} :
a.length = 1 (m : α), a = of m
theorem FreeMonoid.length_eq_two {α : Type u_1} {v : FreeMonoid α} :
v.length = 2 (c : α), (d : α), v = of c * of d
theorem FreeAddMonoid.length_eq_two {α : Type u_1} {v : FreeAddMonoid α} :
v.length = 2 (c : α), (d : α), v = of c + of d
theorem FreeMonoid.length_eq_three {α : Type u_1} {v : FreeMonoid α} :
v.length = 3 (a : α), (b : α), (c : α), v = of a * of b * of c
theorem FreeAddMonoid.length_eq_three {α : Type u_1} {v : FreeAddMonoid α} :
v.length = 3 (a : α), (b : α), (c : α), v = of a + of b + of c
@[simp]
theorem FreeMonoid.length_mul {α : Type u_1} (a b : FreeMonoid α) :
(a * b).length = a.length + b.length
@[simp]
theorem FreeAddMonoid.length_add {α : Type u_1} (a b : FreeAddMonoid α) :
(a + b).length = a.length + b.length
@[simp]
theorem FreeMonoid.of_ne_one {α : Type u_1} (a : α) :
of a 1
@[simp]
theorem FreeAddMonoid.of_ne_zero {α : Type u_1} (a : α) :
of a 0
@[simp]
theorem FreeMonoid.one_ne_of {α : Type u_1} (a : α) :
1 of a
@[simp]
theorem FreeAddMonoid.zero_ne_of {α : Type u_1} (a : α) :
0 of a
def FreeMonoid.mem {α : Type u_1} (a : FreeMonoid α) (m : α) :

Membership in a free monoid element

Equations
def FreeAddMonoid.mem {α : Type u_1} (a : FreeAddMonoid α) (m : α) :

Membership in a free monoid element

Equations
theorem FreeMonoid.notMem_one {α : Type u_1} {m : α} :
¬m 1
theorem FreeAddMonoid.notMem_zero {α : Type u_1} {m : α} :
¬m 0
@[deprecated FreeAddMonoid.notMem_zero (since := "2025-05-23")]
theorem FreeAddMonoid.not_mem_zero {α : Type u_1} {m : α} :
¬m 0

Alias of FreeAddMonoid.notMem_zero.

@[deprecated FreeMonoid.notMem_one (since := "2025-05-23")]
theorem FreeMonoid.not_mem_one {α : Type u_1} {m : α} :
¬m 1

Alias of FreeMonoid.notMem_one.

@[simp]
theorem FreeMonoid.mem_of {α : Type u_1} {m n : α} :
m of n m = n
@[simp]
theorem FreeAddMonoid.mem_of {α : Type u_1} {m n : α} :
m of n m = n
theorem FreeMonoid.mem_of_self {α : Type u_1} {m : α} :
m of m
theorem FreeAddMonoid.mem_of_self {α : Type u_1} {m : α} :
m of m
@[simp]
theorem FreeMonoid.mem_mul {α : Type u_1} {m : α} {a b : FreeMonoid α} :
m a * b m a m b
@[simp]
theorem FreeAddMonoid.mem_add {α : Type u_1} {m : α} {a b : FreeAddMonoid α} :
m a + b m a m b
def FreeMonoid.recOn {α : Type u_1} {C : FreeMonoid αSort u_6} (xs : FreeMonoid α) (h0 : C 1) (ih : (x : α) → (xs : FreeMonoid α) → C xsC (of x * xs)) :
C xs

Recursor for FreeMonoid using 1 and FreeMonoid.of x * xs instead of [] and x :: xs.

Equations
def FreeAddMonoid.recOn {α : Type u_1} {C : FreeAddMonoid αSort u_6} (xs : FreeAddMonoid α) (h0 : C 0) (ih : (x : α) → (xs : FreeAddMonoid α) → C xsC (of x + xs)) :
C xs

Recursor for FreeAddMonoid using 0 and FreeAddMonoid.of x + xsinstead of[]andx :: xs`.

Equations
@[simp]
theorem FreeMonoid.recOn_one {α : Type u_1} {C : FreeMonoid αSort u_6} (h0 : C 1) (ih : (x : α) → (xs : FreeMonoid α) → C xsC (of x * xs)) :
recOn 1 h0 ih = h0
@[simp]
theorem FreeAddMonoid.recOn_zero {α : Type u_1} {C : FreeAddMonoid αSort u_6} (h0 : C 0) (ih : (x : α) → (xs : FreeAddMonoid α) → C xsC (of x + xs)) :
recOn 0 h0 ih = h0
@[simp]
theorem FreeMonoid.recOn_of_mul {α : Type u_1} {C : FreeMonoid αSort u_6} (x : α) (xs : FreeMonoid α) (h0 : C 1) (ih : (x : α) → (xs : FreeMonoid α) → C xsC (of x * xs)) :
(of x * xs).recOn h0 ih = ih x xs (xs.recOn h0 ih)
@[simp]
theorem FreeAddMonoid.recOn_of_add {α : Type u_1} {C : FreeAddMonoid αSort u_6} (x : α) (xs : FreeAddMonoid α) (h0 : C 0) (ih : (x : α) → (xs : FreeAddMonoid α) → C xsC (of x + xs)) :
(of x + xs).recOn h0 ih = ih x xs (xs.recOn h0 ih)

Induction #

theorem FreeMonoid.inductionOn {α : Type u_1} {C : FreeMonoid αProp} (z : FreeMonoid α) (one : C 1) (of : ∀ (x : α), C (of x)) (mul : ∀ (x y : FreeMonoid α), C xC yC (x * y)) :
C z

An induction principle on free monoids, with cases for 1, FreeMonoid.of and *.

theorem FreeAddMonoid.inductionOn {α : Type u_1} {C : FreeAddMonoid αProp} (z : FreeAddMonoid α) (one : C 0) (of : ∀ (x : α), C (of x)) (mul : ∀ (x y : FreeAddMonoid α), C xC yC (x + y)) :
C z

An induction principle on free monoids, with cases for 0, FreeAddMonoid.of and +.

theorem FreeMonoid.inductionOn' {α : Type u_1} {p : FreeMonoid αProp} (a : FreeMonoid α) (one : p 1) (mul_of : ∀ (b : α) (a : FreeMonoid α), p ap (of b * a)) :
p a

An induction principle for free monoids which mirrors induction on lists, with cases analogous to the empty list and cons

theorem FreeAddMonoid.inductionOn' {α : Type u_1} {p : FreeAddMonoid αProp} (a : FreeAddMonoid α) (one : p 0) (mul_of : ∀ (b : α) (a : FreeAddMonoid α), p ap (of b + a)) :
p a

An induction principle for free monoids which mirrors induction on lists, with cases analogous to the empty list and cons

def FreeMonoid.casesOn {α : Type u_1} {C : FreeMonoid αSort u_6} (xs : FreeMonoid α) (h0 : C 1) (ih : (x : α) → (xs : FreeMonoid α) → C (of x * xs)) :
C xs

A version of List.cases_on for FreeMonoid using 1 and FreeMonoid.of x * xs instead of [] and x :: xs.

Equations
def FreeAddMonoid.casesOn {α : Type u_1} {C : FreeAddMonoid αSort u_6} (xs : FreeAddMonoid α) (h0 : C 0) (ih : (x : α) → (xs : FreeAddMonoid α) → C (of x + xs)) :
C xs

A version of List.casesOn for FreeAddMonoid using 0 and FreeAddMonoid.of x + xs instead of [] and x :: xs.

Equations
@[simp]
theorem FreeMonoid.casesOn_one {α : Type u_1} {C : FreeMonoid αSort u_6} (h0 : C 1) (ih : (x : α) → (xs : FreeMonoid α) → C (of x * xs)) :
casesOn 1 h0 ih = h0
@[simp]
theorem FreeAddMonoid.casesOn_zero {α : Type u_1} {C : FreeAddMonoid αSort u_6} (h0 : C 0) (ih : (x : α) → (xs : FreeAddMonoid α) → C (of x + xs)) :
casesOn 0 h0 ih = h0
@[simp]
theorem FreeMonoid.casesOn_of_mul {α : Type u_1} {C : FreeMonoid αSort u_6} (x : α) (xs : FreeMonoid α) (h0 : C 1) (ih : (x : α) → (xs : FreeMonoid α) → C (of x * xs)) :
(of x * xs).casesOn h0 ih = ih x xs
@[simp]
theorem FreeAddMonoid.casesOn_of_add {α : Type u_1} {C : FreeAddMonoid αSort u_6} (x : α) (xs : FreeAddMonoid α) (h0 : C 0) (ih : (x : α) → (xs : FreeAddMonoid α) → C (of x + xs)) :
(of x + xs).casesOn h0 ih = ih x xs
theorem FreeMonoid.hom_eq {α : Type u_1} {M : Type u_4} [Monoid M] f g : FreeMonoid α →* M (h : ∀ (x : α), f (of x) = g (of x)) :
f = g
theorem FreeAddMonoid.hom_eq {α : Type u_1} {M : Type u_4} [AddMonoid M] f g : FreeAddMonoid α →+ M (h : ∀ (x : α), f (of x) = g (of x)) :
f = g
theorem FreeMonoid.hom_eq_iff {α : Type u_1} {M : Type u_4} [Monoid M] {f g : FreeMonoid α →* M} :
f = g ∀ (x : α), f (of x) = g (of x)
theorem FreeAddMonoid.hom_eq_iff {α : Type u_1} {M : Type u_4} [AddMonoid M] {f g : FreeAddMonoid α →+ M} :
f = g ∀ (x : α), f (of x) = g (of x)
def FreeMonoid.prodAux {M : Type u_6} [Monoid M] :
List MM

A variant of List.prod that has [x].prod = x true definitionally. The purpose is to make FreeMonoid.lift_eval_of true by rfl.

Equations
def FreeAddMonoid.sumAux {M : Type u_6} [AddMonoid M] :
List MM

A variant of List.sum that has [x].sum = x true definitionally. The purpose is to make FreeAddMonoid.lift_eval_of true by rfl.

Equations
theorem FreeMonoid.prodAux_eq {M : Type u_4} [Monoid M] (l : List M) :
theorem FreeAddMonoid.sumAux_eq {M : Type u_4} [AddMonoid M] (l : List M) :
def FreeMonoid.lift {α : Type u_1} {M : Type u_4} [Monoid M] :
(αM) (FreeMonoid α →* M)

Equivalence between maps α → M and monoid homomorphisms FreeMonoid α →* M.

Equations
  • One or more equations did not get rendered due to their size.
def FreeAddMonoid.lift {α : Type u_1} {M : Type u_4} [AddMonoid M] :
(αM) (FreeAddMonoid α →+ M)

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

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem FreeMonoid.lift_ofList {α : Type u_1} {M : Type u_4} [Monoid M] (f : αM) (l : List α) :
(lift f) (ofList l) = (List.map f l).prod
@[simp]
theorem FreeAddMonoid.lift_ofList {α : Type u_1} {M : Type u_4} [AddMonoid M] (f : αM) (l : List α) :
(lift f) (ofList l) = (List.map f l).sum
@[simp]
theorem FreeMonoid.lift_symm_apply {α : Type u_1} {M : Type u_4} [Monoid M] (f : FreeMonoid α →* M) :
lift.symm f = f of
@[simp]
theorem FreeAddMonoid.lift_symm_apply {α : Type u_1} {M : Type u_4} [AddMonoid M] (f : FreeAddMonoid α →+ M) :
lift.symm f = f of
theorem FreeMonoid.lift_apply {α : Type u_1} {M : Type u_4} [Monoid M] (f : αM) (l : FreeMonoid α) :
(lift f) l = (List.map f (toList l)).prod
theorem FreeAddMonoid.lift_apply {α : Type u_1} {M : Type u_4} [AddMonoid M] (f : αM) (l : FreeAddMonoid α) :
(lift f) l = (List.map f (toList l)).sum
theorem FreeMonoid.lift_comp_of {α : Type u_1} {M : Type u_4} [Monoid M] (f : αM) :
(lift f) of = f
theorem FreeAddMonoid.lift_comp_of {α : Type u_1} {M : Type u_4} [AddMonoid M] (f : αM) :
(lift f) of = f
@[simp]
theorem FreeMonoid.lift_eval_of {α : Type u_1} {M : Type u_4} [Monoid M] (f : αM) (x : α) :
(lift f) (of x) = f x
@[simp]
theorem FreeAddMonoid.lift_eval_of {α : Type u_1} {M : Type u_4} [AddMonoid M] (f : αM) (x : α) :
(lift f) (of x) = f x
@[simp]
theorem FreeMonoid.lift_restrict {α : Type u_1} {M : Type u_4} [Monoid M] (f : FreeMonoid α →* M) :
lift (f of) = f
@[simp]
theorem FreeAddMonoid.lift_restrict {α : Type u_1} {M : Type u_4} [AddMonoid M] (f : FreeAddMonoid α →+ M) :
lift (f of) = f
theorem FreeMonoid.comp_lift {α : Type u_1} {M : Type u_4} [Monoid M] {N : Type u_5} [Monoid N] (g : M →* N) (f : αM) :
g.comp (lift f) = lift (g f)
theorem FreeAddMonoid.comp_lift {α : Type u_1} {M : Type u_4} [AddMonoid M] {N : Type u_5} [AddMonoid N] (g : M →+ N) (f : αM) :
g.comp (lift f) = lift (g f)
theorem FreeMonoid.hom_map_lift {α : Type u_1} {M : Type u_4} [Monoid M] {N : Type u_5} [Monoid N] (g : M →* N) (f : αM) (x : FreeMonoid α) :
g ((lift f) x) = (lift (g f)) x
theorem FreeAddMonoid.hom_map_lift {α : Type u_1} {M : Type u_4} [AddMonoid M] {N : Type u_5} [AddMonoid N] (g : M →+ N) (f : αM) (x : FreeAddMonoid α) :
g ((lift f) x) = (lift (g f)) x
def FreeMonoid.mkMulAction {α : Type u_1} {β : Type u_2} (f : αββ) :

Define a multiplicative action of FreeMonoid α on β.

Equations
def FreeAddMonoid.mkAddAction {α : Type u_1} {β : Type u_2} (f : αββ) :

Define an additive action of FreeAddMonoid α on β.

Equations
theorem FreeMonoid.smul_def {α : Type u_1} {β : Type u_2} (f : αββ) (l : FreeMonoid α) (b : β) :
l b = List.foldr f b (toList l)
theorem FreeAddMonoid.vadd_def {α : Type u_1} {β : Type u_2} (f : αββ) (l : FreeAddMonoid α) (b : β) :
l +ᵥ b = List.foldr f b (toList l)
theorem FreeMonoid.ofList_smul {α : Type u_1} {β : Type u_2} (f : αββ) (l : List α) (b : β) :
theorem FreeAddMonoid.ofList_vadd {α : Type u_1} {β : Type u_2} (f : αββ) (l : List α) (b : β) :
@[simp]
theorem FreeMonoid.of_smul {α : Type u_1} {β : Type u_2} (f : αββ) (x : α) (y : β) :
of x y = f x y
@[simp]
theorem FreeAddMonoid.of_vadd {α : Type u_1} {β : Type u_2} (f : αββ) (x : α) (y : β) :
of x +ᵥ y = f x y

map #

def FreeMonoid.map {α : Type u_1} {β : Type u_2} (f : αβ) :

The unique monoid homomorphism FreeMonoid α →* FreeMonoid β that sends each of x to of (f x).

Equations
def FreeAddMonoid.map {α : Type u_1} {β : Type u_2} (f : αβ) :

The unique additive monoid homomorphism FreeAddMonoid α →+ FreeAddMonoid β that sends each of x to of (f x).

Equations
@[simp]
theorem FreeMonoid.map_of {α : Type u_1} {β : Type u_2} (f : αβ) (x : α) :
(map f) (of x) = of (f x)
@[simp]
theorem FreeAddMonoid.map_of {α : Type u_1} {β : Type u_2} (f : αβ) (x : α) :
(map f) (of x) = of (f x)
theorem FreeMonoid.mem_map {α : Type u_1} {β : Type u_2} {f : αβ} {a : FreeMonoid α} {m : β} :
m (map f) a (n : α), n a f n = m
theorem FreeAddMonoid.mem_map {α : Type u_1} {β : Type u_2} {f : αβ} {a : FreeAddMonoid α} {m : β} :
m (map f) a (n : α), n a f n = m
theorem FreeMonoid.map_map {α : Type u_1} {β : Type u_2} {f : αβ} {α₁ : Type u_6} {g : α₁α} {x : FreeMonoid α₁} :
(map f) ((map g) x) = (map (f g)) x
theorem FreeAddMonoid.map_map {α : Type u_1} {β : Type u_2} {f : αβ} {α₁ : Type u_6} {g : α₁α} {x : FreeAddMonoid α₁} :
(map f) ((map g) x) = (map (f g)) x
@[simp]
theorem FreeMonoid.toList_map {α : Type u_1} {β : Type u_2} (f : αβ) (xs : FreeMonoid α) :
toList ((map f) xs) = List.map f (toList xs)
@[simp]
theorem FreeAddMonoid.toList_map {α : Type u_1} {β : Type u_2} (f : αβ) (xs : FreeAddMonoid α) :
toList ((map f) xs) = List.map f (toList xs)
theorem FreeMonoid.ofList_map {α : Type u_1} {β : Type u_2} (f : αβ) (xs : List α) :
ofList (List.map f xs) = (map f) (ofList xs)
theorem FreeAddMonoid.ofList_map {α : Type u_1} {β : Type u_2} (f : αβ) (xs : List α) :
ofList (List.map f xs) = (map f) (ofList xs)
theorem FreeMonoid.lift_of_comp_eq_map {α : Type u_1} {β : Type u_2} (f : αβ) :
(lift fun (x : α) => of (f x)) = map f
theorem FreeAddMonoid.lift_of_comp_eq_map {α : Type u_1} {β : Type u_2} (f : αβ) :
(lift fun (x : α) => of (f x)) = map f
theorem FreeMonoid.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : βγ) (f : αβ) :
map (g f) = (map g).comp (map f)
theorem FreeAddMonoid.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : βγ) (f : αβ) :
map (g f) = (map g).comp (map f)
@[simp]
@[simp]
theorem FreeMonoid.map_symm_apply_map_eq {α : Type u_1} {β : Type u_2} {x : FreeMonoid α} (e : α β) :
(map e.symm) ((map e) x) = x
@[simp]
theorem FreeAddMonoid.map_symm_apply_map_eq {α : Type u_1} {β : Type u_2} {x : FreeAddMonoid α} (e : α β) :
(map e.symm) ((map e) x) = x
@[simp]
theorem FreeMonoid.map_apply_map_symm_eq {α : Type u_1} {β : Type u_2} {x : FreeMonoid β} (e : α β) :
(map e) ((map e.symm) x) = x
@[simp]
theorem FreeAddMonoid.map_apply_map_symm_eq {α : Type u_1} {β : Type u_2} {x : FreeAddMonoid β} (e : α β) :
(map e) ((map e.symm) x) = x

The only invertible element of the free monoid is 1; this instance enables units_eq_one.

Equations
@[simp]
theorem FreeMonoid.map_surjective {α : Type u_1} {β : Type u_2} {f : αβ} :
@[simp]
theorem FreeAddMonoid.map_surjective {α : Type u_1} {β : Type u_2} {f : αβ} :

reverse #

def FreeMonoid.reverse {α : Type u_1} :

reverses the symbols in a free monoid element

Equations

reverses the symbols in an additive free monoid element

Equations
@[simp]
theorem FreeMonoid.reverse_of {α : Type u_1} (a : α) :
(of a).reverse = of a
@[simp]
theorem FreeAddMonoid.reverse_of {α : Type u_1} (a : α) :
(of a).reverse = of a
theorem FreeMonoid.reverse_mul {α : Type u_1} {a b : FreeMonoid α} :
theorem FreeAddMonoid.reverse_add {α : Type u_1} {a b : FreeAddMonoid α} :
@[simp]
theorem FreeMonoid.reverse_reverse {α : Type u_1} {a : FreeMonoid α} :
@[simp]
@[simp]
def FreeMonoid.freeMonoidCongr {α : Type u_6} {β : Type u_7} (e : α β) :

free monoids over isomorphic types are isomorphic

Equations
def FreeAddMonoid.freeAddMonoidCongr {α : Type u_6} {β : Type u_7} (e : α β) :

if two types are isomorphic, the additive free monoids over those types are isomorphic

Equations
@[simp]
theorem FreeMonoid.freeMonoidCongr_of {α : Type u_6} {β : Type u_7} (e : α β) (a : α) :
(freeMonoidCongr e) (of a) = of (e a)
@[simp]
theorem FreeAddMonoid.freeAddMonoidCongr_of {α : Type u_6} {β : Type u_7} (e : α β) (a : α) :
(freeAddMonoidCongr e) (of a) = of (e a)
@[simp]
theorem FreeMonoid.freeMonoidCongr_symm_of {α : Type u_6} {β : Type u_7} (e : α β) (b : β) :
(freeMonoidCongr e.symm) (of b) = of (e.symm b)
@[simp]
theorem FreeAddMonoid.freeAddMonoidCongr_symm_of {α : Type u_6} {β : Type u_7} (e : α β) (b : β) :