Free monoid over a given alphabet

Main definitions

• FreeMonoid α: free monoid over alphabet α; defined as a synonym for List α with multiplication given by (++).
• FreeMonoid.of: embedding α → FreeMonoid α sending each element x to [x];
• FreeMonoid.lift: natural equivalence between α → M and FreeMonoid α →* M
• FreeMonoid.map: embedding of α → β into FreeMonoid α →* FreeMonoid β given by List.map.

def FreeAddMonoid (α : Type u_6) : Type u_6

Free nonabelian additive monoid over a given alphabet

Equations

• FreeAddMonoid α = List α

def FreeMonoid (α : Type u_6) : Type u_6

Free monoid over a given alphabet.

Equations

• FreeMonoid α = List α

def FreeAddMonoid.toList {α : Type u_1} : FreeAddMonoid α ≃ List α

The identity equivalence between FreeAddMonoid α and List α.

Equations

• FreeAddMonoid.toList = Equiv.refl (FreeAddMonoid α)

def FreeMonoid.toList {α : Type u_1} : FreeMonoid α ≃ List α

The identity equivalence between FreeMonoid α and List α.

Equations

• FreeMonoid.toList = Equiv.refl (FreeMonoid α)

def FreeAddMonoid.ofList {α : Type u_1} : List α ≃ FreeAddMonoid α

The identity equivalence between List α and FreeAddMonoid α.

Equations

• FreeAddMonoid.ofList = Equiv.refl (List α)

def FreeMonoid.ofList {α : Type u_1} : List α ≃ FreeMonoid α

The identity equivalence between List α and FreeMonoid α.

Equations

• FreeMonoid.ofList = Equiv.refl (List α)

@[simp]

theorem FreeAddMonoid.toList_symm {α : Type u_1} : FreeAddMonoid.toList.symm = FreeAddMonoid.ofList

@[simp]

theorem FreeMonoid.toList_symm {α : Type u_1} : FreeMonoid.toList.symm = FreeMonoid.ofList

@[simp]

theorem FreeAddMonoid.ofList_symm {α : Type u_1} : FreeAddMonoid.ofList.symm = FreeAddMonoid.toList

@[simp]

theorem FreeMonoid.ofList_symm {α : Type u_1} : FreeMonoid.ofList.symm = FreeMonoid.toList

@[simp]

theorem FreeAddMonoid.toList_ofList {α : Type u_1} (l : List α) : FreeAddMonoid.toList (FreeAddMonoid.ofList l) = l

@[simp]

theorem FreeMonoid.toList_ofList {α : Type u_1} (l : List α) : FreeMonoid.toList (FreeMonoid.ofList l) = l

@[simp]

theorem FreeAddMonoid.ofList_toList {α : Type u_1} (xs : FreeAddMonoid α) : FreeAddMonoid.ofList (FreeAddMonoid.toList xs) = xs

@[simp]

theorem FreeMonoid.ofList_toList {α : Type u_1} (xs : FreeMonoid α) : FreeMonoid.ofList (FreeMonoid.toList xs) = xs

@[simp]

theorem FreeAddMonoid.toList_comp_ofList {α : Type u_1} : ⇑FreeAddMonoid.toList ∘ ⇑FreeAddMonoid.ofList = id

@[simp]

theorem FreeMonoid.toList_comp_ofList {α : Type u_1} : ⇑FreeMonoid.toList ∘ ⇑FreeMonoid.ofList = id

@[simp]

theorem FreeAddMonoid.ofList_comp_toList {α : Type u_1} : ⇑FreeAddMonoid.ofList ∘ ⇑FreeAddMonoid.toList = id

@[simp]

theorem FreeMonoid.ofList_comp_toList {α : Type u_1} : ⇑FreeMonoid.ofList ∘ ⇑FreeMonoid.toList = id

theorem FreeAddMonoid.instAddCancelMonoid.proof_1 {α : Type u_1} : ∀ (x : FreeAddMonoid α), nsmulRecAuto 0 x = nsmulRecAuto 0 x

instance FreeAddMonoid.instAddCancelMonoid {α : Type u_1} : AddCancelMonoid (FreeAddMonoid α)

Equations

• FreeAddMonoid.instAddCancelMonoid = AddCancelMonoid.mk ⋯

theorem FreeAddMonoid.instAddCancelMonoid.proof_3 {α : Type u_1} : ∀ (x x_1 x_2 : FreeAddMonoid α), FreeAddMonoid.toList x ++ FreeAddMonoid.toList x_1 = FreeAddMonoid.toList x ++ FreeAddMonoid.toList x_2 → FreeAddMonoid.toList x_1 = FreeAddMonoid.toList x_2

theorem FreeAddMonoid.instAddCancelMonoid.proof_2 {α : Type u_1} : ∀ (n : ℕ) (x : FreeAddMonoid α), nsmulRecAuto (n + 1) x = nsmulRecAuto (n + 1) x

theorem FreeAddMonoid.instAddCancelMonoid.proof_4 {α : Type u_1} : ∀ (x x_1 x_2 : FreeAddMonoid α), FreeAddMonoid.toList x ++ FreeAddMonoid.toList x_1 = FreeAddMonoid.toList x_2 ++ FreeAddMonoid.toList x_1 → FreeAddMonoid.toList x = FreeAddMonoid.toList x_2

instance FreeMonoid.instCancelMonoid {α : Type u_1} : CancelMonoid (FreeMonoid α)

Equations

• FreeMonoid.instCancelMonoid = CancelMonoid.mk ⋯

instance FreeAddMonoid.instInhabited {α : Type u_1} : Inhabited (FreeAddMonoid α)

Equations

• FreeAddMonoid.instInhabited = { default := 0 }

instance FreeMonoid.instInhabited {α : Type u_1} : Inhabited (FreeMonoid α)

Equations

• FreeMonoid.instInhabited = { default := 1 }

instance FreeAddMonoid.instUniqueOfIsEmpty {α : Type u_1} [IsEmpty α] : Unique (FreeAddMonoid α)

Equations

• FreeAddMonoid.instUniqueOfIsEmpty = inferInstanceAs (Unique (List α))

instance FreeMonoid.instUniqueOfIsEmpty {α : Type u_1} [IsEmpty α] : Unique (FreeMonoid α)

Equations

• FreeMonoid.instUniqueOfIsEmpty = inferInstanceAs (Unique (List α))

@[simp]

theorem FreeAddMonoid.toList_zero {α : Type u_1} : FreeAddMonoid.toList 0 = []

@[simp]

theorem FreeMonoid.toList_one {α : Type u_1} : FreeMonoid.toList 1 = []

@[simp]

theorem FreeAddMonoid.ofList_nil {α : Type u_1} : FreeAddMonoid.ofList [] = 0

@[simp]

theorem FreeMonoid.ofList_nil {α : Type u_1} : FreeMonoid.ofList [] = 1

@[simp]

theorem FreeAddMonoid.toList_add {α : Type u_1} (xs : FreeAddMonoid α) (ys : FreeAddMonoid α) : FreeAddMonoid.toList (xs + ys) = FreeAddMonoid.toList xs ++ FreeAddMonoid.toList ys

@[simp]

theorem FreeMonoid.toList_mul {α : Type u_1} (xs : FreeMonoid α) (ys : FreeMonoid α) : FreeMonoid.toList (xs * ys) = FreeMonoid.toList xs ++ FreeMonoid.toList ys

@[simp]

theorem FreeAddMonoid.ofList_append {α : Type u_1} (xs : List α) (ys : List α) : FreeAddMonoid.ofList (xs ++ ys) = FreeAddMonoid.ofList xs + FreeAddMonoid.ofList ys

@[simp]

theorem FreeMonoid.ofList_append {α : Type u_1} (xs : List α) (ys : List α) : FreeMonoid.ofList (xs ++ ys) = FreeMonoid.ofList xs * FreeMonoid.ofList ys

@[simp]

theorem FreeAddMonoid.toList_sum {α : Type u_1} (xs : List (FreeAddMonoid α)) : FreeAddMonoid.toList xs.sum = (List.map (⇑FreeAddMonoid.toList) xs).join

@[simp]

theorem FreeMonoid.toList_prod {α : Type u_1} (xs : List (FreeMonoid α)) : FreeMonoid.toList xs.prod = (List.map (⇑FreeMonoid.toList) xs).join

@[simp]

theorem FreeAddMonoid.ofList_join {α : Type u_1} (xs : List (List α)) : FreeAddMonoid.ofList xs.join = (List.map (⇑FreeAddMonoid.ofList) xs).sum

@[simp]

theorem FreeMonoid.ofList_join {α : Type u_1} (xs : List (List α)) : FreeMonoid.ofList xs.join = (List.map (⇑FreeMonoid.ofList) xs).prod

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

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

Equations

• FreeAddMonoid.of x = FreeAddMonoid.ofList [x]

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

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

Equations

• FreeMonoid.of x = FreeMonoid.ofList [x]

@[simp]

theorem FreeAddMonoid.toList_of {α : Type u_1} (x : α) : FreeAddMonoid.toList (FreeAddMonoid.of x) = [x]

@[simp]

theorem FreeMonoid.toList_of {α : Type u_1} (x : α) : FreeMonoid.toList (FreeMonoid.of x) = [x]

theorem FreeAddMonoid.ofList_singleton {α : Type u_1} (x : α) : FreeAddMonoid.ofList [x] = FreeAddMonoid.of x

theorem FreeMonoid.ofList_singleton {α : Type u_1} (x : α) : FreeMonoid.ofList [x] = FreeMonoid.of x

@[simp]

theorem FreeAddMonoid.ofList_cons {α : Type u_1} (x : α) (xs : List α) : FreeAddMonoid.ofList (x :: xs) = FreeAddMonoid.of x + FreeAddMonoid.ofList xs

@[simp]

theorem FreeMonoid.ofList_cons {α : Type u_1} (x : α) (xs : List α) : FreeMonoid.ofList (x :: xs) = FreeMonoid.of x * FreeMonoid.ofList xs

theorem FreeAddMonoid.toList_of_add {α : Type u_1} (x : α) (xs : FreeAddMonoid α) : FreeAddMonoid.toList (FreeAddMonoid.of x + xs) = x :: FreeAddMonoid.toList xs

theorem FreeMonoid.toList_of_mul {α : Type u_1} (x : α) (xs : FreeMonoid α) : FreeMonoid.toList (FreeMonoid.of x * xs) = x :: FreeMonoid.toList xs

theorem FreeAddMonoid.of_injective {α : Type u_1} : Function.Injective FreeAddMonoid.of

theorem FreeMonoid.of_injective {α : Type u_1} : Function.Injective FreeMonoid.of

Length

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

• a.length = List.length a

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

• a.length = List.length a

@[simp]

theorem FreeAddMonoid.length_zero {α : Type u_1} : FreeAddMonoid.length 0 = 0

@[simp]

theorem FreeMonoid.length_one {α : Type u_1} : FreeMonoid.length 1 = 0

@[simp]

theorem FreeAddMonoid.length_eq_zero {α : Type u_1} {a : FreeAddMonoid α} : a.length = 0 ↔ a = 0

@[simp]

theorem FreeMonoid.length_eq_zero {α : Type u_1} {a : FreeMonoid α} : a.length = 0 ↔ a = 1

@[simp]

theorem FreeAddMonoid.length_of {α : Type u_1} (m : α) : (FreeAddMonoid.of m).length = 1

@[simp]

theorem FreeMonoid.length_of {α : Type u_1} (m : α) : (FreeMonoid.of m).length = 1

theorem FreeMonoid.length_eq_one {α : Type u_1} {a : FreeMonoid α} : a.length = 1 ↔ ∃ (m : α), a = FreeMonoid.of m

theorem FreeAddMonoid.length_eq_two {α : Type u_1} {v : FreeAddMonoid α} : v.length = 2 ↔ ∃ (c : α) (d : α), v = FreeAddMonoid.of c + FreeAddMonoid.of d

theorem FreeMonoid.length_eq_two {α : Type u_1} {v : FreeMonoid α} : v.length = 2 ↔ ∃ (c : α) (d : α), v = FreeMonoid.of c * FreeMonoid.of d

@[simp]

theorem FreeAddMonoid.length_add {α : Type u_1} (a : FreeAddMonoid α) (b : FreeAddMonoid α) : (a + b).length = a.length + b.length

@[simp]

theorem FreeMonoid.length_mul {α : Type u_1} (a : FreeMonoid α) (b : FreeMonoid α) : (a * b).length = a.length + b.length

@[simp]

theorem FreeAddMonoid.of_ne_zero {α : Type u_1} (a : α) : FreeAddMonoid.of a ≠ 0

@[simp]

theorem FreeMonoid.of_ne_one {α : Type u_1} (a : α) : FreeMonoid.of a ≠ 1

@[simp]

theorem FreeAddMonoid.zero_ne_of {α : Type u_1} (a : α) : 0 ≠ FreeAddMonoid.of a

@[simp]

theorem FreeMonoid.one_ne_of {α : Type u_1} (a : α) : 1 ≠ FreeMonoid.of a

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

Membership in a free monoid element

Equations

• a.mem m = (m ∈ FreeAddMonoid.toList a)

def FreeMonoid.mem {α : Type u_1} (a : FreeMonoid α) (m : α) : Prop

Membership in a free monoid element

Equations

• a.mem m = (m ∈ FreeMonoid.toList a)

instance FreeAddMonoid.instMembership {α : Type u_1} : Membership α (FreeAddMonoid α)

Equations

• FreeAddMonoid.instMembership = { mem := FreeAddMonoid.mem }

instance FreeMonoid.instMembership {α : Type u_1} : Membership α (FreeMonoid α)

Equations

• FreeMonoid.instMembership = { mem := FreeMonoid.mem }

theorem FreeAddMonoid.not_mem_zero {α : Type u_1} {m : α} : m ∉ 0

theorem FreeMonoid.not_mem_one {α : Type u_1} {m : α} : m ∉ 1

@[simp]

theorem FreeAddMonoid.mem_of {α : Type u_1} {m : α} {n : α} : m ∈ FreeAddMonoid.of n ↔ m = n

@[simp]

theorem FreeMonoid.mem_of {α : Type u_1} {m : α} {n : α} : m ∈ FreeMonoid.of n ↔ m = n

theorem FreeAddMonoid.mem_of_self {α : Type u_1} {m : α} : m ∈ FreeAddMonoid.of m

theorem FreeMonoid.mem_of_self {α : Type u_1} {m : α} : m ∈ FreeMonoid.of m

@[simp]

theorem FreeAddMonoid.mem_add {α : Type u_1} {m : α} {a : FreeAddMonoid α} {b : FreeAddMonoid α} : m ∈ a + b ↔ m ∈ a ∨ m ∈ b

@[simp]

theorem FreeMonoid.mem_mul {α : Type u_1} {m : α} {a : FreeMonoid α} {b : FreeMonoid α} : m ∈ a * b ↔ m ∈ a ∨ m ∈ b

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

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

Equations

• xs.recOn h0 ih = List.rec h0 ih xs

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

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

Equations

• xs.recOn h0 ih = List.rec h0 ih xs

@[simp]

theorem FreeAddMonoid.recOn_zero {α : Type u_1} {C : FreeAddMonoid α → Sort u_6} (h0 : C 0) (ih : (x : α) → (xs : FreeAddMonoid α) → C xs → C (FreeAddMonoid.of x + xs)) : FreeAddMonoid.recOn 0 h0 ih = h0

@[simp]

theorem FreeMonoid.recOn_one {α : Type u_1} {C : FreeMonoid α → Sort u_6} (h0 : C 1) (ih : (x : α) → (xs : FreeMonoid α) → C xs → C (FreeMonoid.of x * xs)) : FreeMonoid.recOn 1 h0 ih = h0

@[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 xs → C (FreeAddMonoid.of x + xs)) : (FreeAddMonoid.of x + xs).recOn h0 ih = ih x xs (xs.recOn h0 ih)

@[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 xs → C (FreeMonoid.of x * xs)) : (FreeMonoid.of x * xs).recOn h0 ih = ih x xs (xs.recOn h0 ih)

Induction

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

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

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

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

theorem FreeAddMonoid.inductionOn' {α : Type u_1} {p : FreeAddMonoid α → Prop} (a : FreeAddMonoid α) (one : p 0) (mul_of : ∀ (b : α) (a : FreeAddMonoid α), p a → p (FreeAddMonoid.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 FreeMonoid.inductionOn' {α : Type u_1} {p : FreeMonoid α → Prop} (a : FreeMonoid α) (one : p 1) (mul_of : ∀ (b : α) (a : FreeMonoid α), p a → p (FreeMonoid.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 FreeAddMonoid.casesOn {α : Type u_1} {C : FreeAddMonoid α → Sort u_6} (xs : FreeAddMonoid α) (h0 : C 0) (ih : (x : α) → (xs : FreeAddMonoid α) → C (FreeAddMonoid.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

• xs.casesOn h0 ih = List.casesOn xs h0 ih

def FreeMonoid.casesOn {α : Type u_1} {C : FreeMonoid α → Sort u_6} (xs : FreeMonoid α) (h0 : C 1) (ih : (x : α) → (xs : FreeMonoid α) → C (FreeMonoid.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

• xs.casesOn h0 ih = List.casesOn xs h0 ih

@[simp]

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

@[simp]

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

@[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 (FreeAddMonoid.of x + xs)) : (FreeAddMonoid.of x + xs).casesOn h0 ih = ih x xs

@[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 (FreeMonoid.of x * xs)) : (FreeMonoid.of x * xs).casesOn h0 ih = ih x xs

theorem FreeAddMonoid.hom_eq {α : Type u_1} {M : Type u_4} [AddMonoid M] ⦃f : FreeAddMonoid α →+ M⦄ ⦃g : FreeAddMonoid α →+ M⦄ (h : ∀ (x : α), f (FreeAddMonoid.of x) = g (FreeAddMonoid.of x)) : f = g

theorem FreeAddMonoid.hom_eq_iff {α : Type u_1} {M : Type u_4} [AddMonoid M] {f : FreeAddMonoid α →+ M} {g : FreeAddMonoid α →+ M} : f = g ↔ ∀ (x : α), f (FreeAddMonoid.of x) = g (FreeAddMonoid.of x)

theorem FreeMonoid.hom_eq_iff {α : Type u_1} {M : Type u_4} [Monoid M] {f : FreeMonoid α →* M} {g : FreeMonoid α →* M} : f = g ↔ ∀ (x : α), f (FreeMonoid.of x) = g (FreeMonoid.of x)

theorem FreeMonoid.hom_eq {α : Type u_1} {M : Type u_4} [Monoid M] ⦃f : FreeMonoid α →* M⦄ ⦃g : FreeMonoid α →* M⦄ (h : ∀ (x : α), f (FreeMonoid.of x) = g (FreeMonoid.of x)) : f = g

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

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

• FreeAddMonoid.sumAux [] = 0
• FreeAddMonoid.sumAux (x_1 :: xs) = List.foldl (fun (x1 x2 : M) => x1 + x2) x_1 xs

def FreeMonoid.prodAux {M : Type u_6} [Monoid M] : List M → M

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

• FreeMonoid.prodAux [] = 1
• FreeMonoid.prodAux (x_1 :: xs) = List.foldl (fun (x1 x2 : M) => x1 * x2) x_1 xs

theorem FreeAddMonoid.sumAux_eq {M : Type u_4} [AddMonoid M] (l : List M) : FreeAddMonoid.sumAux l = l.sum

theorem FreeMonoid.prodAux_eq {M : Type u_4} [Monoid M] (l : List M) : FreeMonoid.prodAux l = l.prod

theorem FreeAddMonoid.lift.proof_2 {α : Type u_1} {M : Type u_2} [AddMonoid M] (f : α → M) : ∀ (x x_1 : FreeAddMonoid α), FreeAddMonoid.sumAux (List.map f (FreeAddMonoid.toList x ++ FreeAddMonoid.toList x_1)) = FreeAddMonoid.sumAux (List.map f (FreeAddMonoid.toList x)) + FreeAddMonoid.sumAux (List.map f (FreeAddMonoid.toList x_1))

theorem FreeAddMonoid.lift.proof_3 {α : Type u_1} {M : Type u_2} [AddMonoid M] : ∀ (x : α → M), (fun (f : FreeAddMonoid α →+ M) (x : α) => f (FreeAddMonoid.of x)) ((fun (f : α → M) => { toFun := fun (l : FreeAddMonoid α) => FreeAddMonoid.sumAux (List.map f (FreeAddMonoid.toList l)), map_zero' := ⋯, map_add' := ⋯ }) x) = (fun (f : FreeAddMonoid α →+ M) (x : α) => f (FreeAddMonoid.of x)) ((fun (f : α → M) => { toFun := fun (l : FreeAddMonoid α) => FreeAddMonoid.sumAux (List.map f (FreeAddMonoid.toList l)), map_zero' := ⋯, map_add' := ⋯ }) x)

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.

theorem FreeAddMonoid.lift.proof_1 {α : Type u_2} {M : Type u_1} [AddMonoid M] (f : α → M) : (fun (l : FreeAddMonoid α) => FreeAddMonoid.sumAux (List.map f (FreeAddMonoid.toList l))) 0 = (fun (l : FreeAddMonoid α) => FreeAddMonoid.sumAux (List.map f (FreeAddMonoid.toList l))) 0

theorem FreeAddMonoid.lift.proof_4 {α : Type u_1} {M : Type u_2} [AddMonoid M] : ∀ (x : FreeAddMonoid α →+ M), (fun (f : α → M) => { toFun := fun (l : FreeAddMonoid α) => FreeAddMonoid.sumAux (List.map f (FreeAddMonoid.toList l)), map_zero' := ⋯, map_add' := ⋯ }) ((fun (f : FreeAddMonoid α →+ M) (x : α) => f (FreeAddMonoid.of x)) x) = x

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.

@[simp]

theorem FreeAddMonoid.lift_ofList {α : Type u_1} {M : Type u_4} [AddMonoid M] (f : α → M) (l : List α) : (FreeAddMonoid.lift f) (FreeAddMonoid.ofList l) = (List.map f l).sum

@[simp]

theorem FreeMonoid.lift_ofList {α : Type u_1} {M : Type u_4} [Monoid M] (f : α → M) (l : List α) : (FreeMonoid.lift f) (FreeMonoid.ofList l) = (List.map f l).prod

@[simp]

theorem FreeAddMonoid.lift_symm_apply {α : Type u_1} {M : Type u_4} [AddMonoid M] (f : FreeAddMonoid α →+ M) : FreeAddMonoid.lift.symm f = ⇑f ∘ FreeAddMonoid.of

@[simp]

theorem FreeMonoid.lift_symm_apply {α : Type u_1} {M : Type u_4} [Monoid M] (f : FreeMonoid α →* M) : FreeMonoid.lift.symm f = ⇑f ∘ FreeMonoid.of

theorem FreeAddMonoid.lift_apply {α : Type u_1} {M : Type u_4} [AddMonoid M] (f : α → M) (l : FreeAddMonoid α) : (FreeAddMonoid.lift f) l = (List.map f (FreeAddMonoid.toList l)).sum

theorem FreeMonoid.lift_apply {α : Type u_1} {M : Type u_4} [Monoid M] (f : α → M) (l : FreeMonoid α) : (FreeMonoid.lift f) l = (List.map f (FreeMonoid.toList l)).prod

theorem FreeAddMonoid.lift_comp_of {α : Type u_1} {M : Type u_4} [AddMonoid M] (f : α → M) : ⇑(FreeAddMonoid.lift f) ∘ FreeAddMonoid.of = f

theorem FreeMonoid.lift_comp_of {α : Type u_1} {M : Type u_4} [Monoid M] (f : α → M) : ⇑(FreeMonoid.lift f) ∘ FreeMonoid.of = f

@[simp]

theorem FreeAddMonoid.lift_eval_of {α : Type u_1} {M : Type u_4} [AddMonoid M] (f : α → M) (x : α) : (FreeAddMonoid.lift f) (FreeAddMonoid.of x) = f x

@[simp]

theorem FreeMonoid.lift_eval_of {α : Type u_1} {M : Type u_4} [Monoid M] (f : α → M) (x : α) : (FreeMonoid.lift f) (FreeMonoid.of x) = f x

@[simp]

theorem FreeAddMonoid.lift_restrict {α : Type u_1} {M : Type u_4} [AddMonoid M] (f : FreeAddMonoid α →+ M) : FreeAddMonoid.lift (⇑f ∘ FreeAddMonoid.of) = f

@[simp]

theorem FreeMonoid.lift_restrict {α : Type u_1} {M : Type u_4} [Monoid M] (f : FreeMonoid α →* M) : FreeMonoid.lift (⇑f ∘ FreeMonoid.of) = 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 (FreeAddMonoid.lift f) = FreeAddMonoid.lift (⇑g ∘ 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 (FreeMonoid.lift f) = FreeMonoid.lift (⇑g ∘ f)

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 ((FreeAddMonoid.lift f) x) = (FreeAddMonoid.lift (⇑g ∘ f)) x

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 ((FreeMonoid.lift f) x) = (FreeMonoid.lift (⇑g ∘ f)) x

theorem FreeAddMonoid.mkAddAction.proof_1 {α : Type u_2} {β : Type u_1} (f : α → β → β) : ∀ (x : β), 0 +ᵥ x = 0 +ᵥ x

theorem FreeAddMonoid.mkAddAction.proof_2 {α : Type u_1} {β : Type u_2} (f : α → β → β) : ∀ (x x_1 : FreeAddMonoid α) (x_2 : β), List.foldr f x_2 (FreeAddMonoid.toList x ++ FreeAddMonoid.toList x_1) = List.foldr f (List.foldr f x_2 (FreeAddMonoid.toList x_1)) (FreeAddMonoid.toList x)

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

Define an additive action of FreeAddMonoid α on β.

Equations

• FreeAddMonoid.mkAddAction f = AddAction.mk ⋯ ⋯

def FreeMonoid.mkMulAction {α : Type u_1} {β : Type u_2} (f : α → β → β) : MulAction (FreeMonoid α) β

Define a multiplicative action of FreeMonoid α on β.

Equations

• FreeMonoid.mkMulAction f = MulAction.mk ⋯ ⋯

theorem FreeAddMonoid.vadd_def {α : Type u_1} {β : Type u_2} (f : α → β → β) (l : FreeAddMonoid α) (b : β) : l +ᵥ b = List.foldr f b (FreeAddMonoid.toList l)

theorem FreeMonoid.smul_def {α : Type u_1} {β : Type u_2} (f : α → β → β) (l : FreeMonoid α) (b : β) : l • b = List.foldr f b (FreeMonoid.toList l)

theorem FreeAddMonoid.ofList_vadd {α : Type u_1} {β : Type u_2} (f : α → β → β) (l : List α) (b : β) : FreeAddMonoid.ofList l +ᵥ b = List.foldr f b l

theorem FreeMonoid.ofList_smul {α : Type u_1} {β : Type u_2} (f : α → β → β) (l : List α) (b : β) : FreeMonoid.ofList l • b = List.foldr f b l

@[simp]

theorem FreeAddMonoid.of_vadd {α : Type u_1} {β : Type u_2} (f : α → β → β) (x : α) (y : β) : FreeAddMonoid.of x +ᵥ y = f x y

@[simp]

theorem FreeMonoid.of_smul {α : Type u_1} {β : Type u_2} (f : α → β → β) (x : α) (y : β) : FreeMonoid.of x • y = f x y

map

theorem FreeAddMonoid.map.proof_2 {α : Type u_1} {β : Type u_2} (f : α → β) : ∀ (x x_1 : FreeAddMonoid α), List.map f (FreeAddMonoid.toList x ++ FreeAddMonoid.toList x_1) = List.map f (FreeAddMonoid.toList x) ++ List.map f (FreeAddMonoid.toList x_1)

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

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

Equations

• FreeAddMonoid.map f = { toFun := fun (l : FreeAddMonoid α) => FreeAddMonoid.ofList (List.map f (FreeAddMonoid.toList l)), map_zero' := ⋯, map_add' := ⋯ }

theorem FreeAddMonoid.map.proof_1 {α : Type u_2} {β : Type u_1} (f : α → β) : (fun (l : FreeAddMonoid α) => FreeAddMonoid.ofList (List.map f (FreeAddMonoid.toList l))) 0 = (fun (l : FreeAddMonoid α) => FreeAddMonoid.ofList (List.map f (FreeAddMonoid.toList l))) 0

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

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

Equations

• FreeMonoid.map f = { toFun := fun (l : FreeMonoid α) => FreeMonoid.ofList (List.map f (FreeMonoid.toList l)), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem FreeAddMonoid.map_of {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) : (FreeAddMonoid.map f) (FreeAddMonoid.of x) = FreeAddMonoid.of (f x)

@[simp]

theorem FreeMonoid.map_of {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) : (FreeMonoid.map f) (FreeMonoid.of x) = FreeMonoid.of (f x)

theorem FreeAddMonoid.mem_map {α : Type u_1} {β : Type u_2} {f : α → β} {a : FreeAddMonoid α} {m : β} : m ∈ (FreeAddMonoid.map f) a ↔ ∃ n ∈ a, f n = m

theorem FreeMonoid.mem_map {α : Type u_1} {β : Type u_2} {f : α → β} {a : FreeMonoid α} {m : β} : m ∈ (FreeMonoid.map f) a ↔ ∃ n ∈ a, f n = m

theorem FreeAddMonoid.map_map {α : Type u_1} {β : Type u_2} {f : α → β} {α₁ : Type u_6} {g : α₁ → α} {x : FreeAddMonoid α₁} : (FreeAddMonoid.map f) ((FreeAddMonoid.map g) x) = (FreeAddMonoid.map (f ∘ g)) x

theorem FreeMonoid.map_map {α : Type u_1} {β : Type u_2} {f : α → β} {α₁ : Type u_6} {g : α₁ → α} {x : FreeMonoid α₁} : (FreeMonoid.map f) ((FreeMonoid.map g) x) = (FreeMonoid.map (f ∘ g)) x

theorem FreeAddMonoid.toList_map {α : Type u_1} {β : Type u_2} (f : α → β) (xs : FreeAddMonoid α) : FreeAddMonoid.toList ((FreeAddMonoid.map f) xs) = List.map f (FreeAddMonoid.toList xs)

theorem FreeMonoid.toList_map {α : Type u_1} {β : Type u_2} (f : α → β) (xs : FreeMonoid α) : FreeMonoid.toList ((FreeMonoid.map f) xs) = List.map f (FreeMonoid.toList xs)

theorem FreeAddMonoid.ofList_map {α : Type u_1} {β : Type u_2} (f : α → β) (xs : List α) : FreeAddMonoid.ofList (List.map f xs) = (FreeAddMonoid.map f) (FreeAddMonoid.ofList xs)

theorem FreeMonoid.ofList_map {α : Type u_1} {β : Type u_2} (f : α → β) (xs : List α) : FreeMonoid.ofList (List.map f xs) = (FreeMonoid.map f) (FreeMonoid.ofList xs)

theorem FreeAddMonoid.lift_of_comp_eq_map {α : Type u_1} {β : Type u_2} (f : α → β) : (FreeAddMonoid.lift fun (x : α) => FreeAddMonoid.of (f x)) = FreeAddMonoid.map f

theorem FreeMonoid.lift_of_comp_eq_map {α : Type u_1} {β : Type u_2} (f : α → β) : (FreeMonoid.lift fun (x : α) => FreeMonoid.of (f x)) = FreeMonoid.map f

theorem FreeAddMonoid.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) : FreeAddMonoid.map (g ∘ f) = (FreeAddMonoid.map g).comp (FreeAddMonoid.map f)

theorem FreeMonoid.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) : FreeMonoid.map (g ∘ f) = (FreeMonoid.map g).comp (FreeMonoid.map f)

@[simp]

theorem FreeAddMonoid.map_id {α : Type u_1} : FreeAddMonoid.map id = AddMonoidHom.id (FreeAddMonoid α)

@[simp]

theorem FreeMonoid.map_id {α : Type u_1} : FreeMonoid.map id = MonoidHom.id (FreeMonoid α)

theorem FreeAddMonoid.uniqueAddUnits.proof_1 {α : Type u_1} (u : AddUnits (FreeAddMonoid α)) : u = default

instance FreeAddMonoid.uniqueAddUnits {α : Type u_1} : Unique (AddUnits (FreeAddMonoid α))

Equations

• FreeAddMonoid.uniqueAddUnits = { toInhabited := AddUnits.instInhabited, uniq := ⋯ }

instance FreeMonoid.uniqueUnits {α : Type u_1} : Unique (FreeMonoid α)ˣ

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

Equations

• FreeMonoid.uniqueUnits = { toInhabited := Units.instInhabited, uniq := ⋯ }

@[simp]

theorem FreeAddMonoid.map_surjective {α : Type u_1} {β : Type u_2} {f : α → β} : Function.Surjective ⇑(FreeAddMonoid.map f) ↔ Function.Surjective f

@[simp]

theorem FreeMonoid.map_surjective {α : Type u_1} {β : Type u_2} {f : α → β} : Function.Surjective ⇑(FreeMonoid.map f) ↔ Function.Surjective f

reverse

def FreeAddMonoid.reverse {α : Type u_1} : FreeAddMonoid α → FreeAddMonoid α

reverses the symbols in an additive free monoid element

Equations

• FreeAddMonoid.reverse = List.reverse

def FreeMonoid.reverse {α : Type u_1} : FreeMonoid α → FreeMonoid α

reverses the symbols in a free monoid element

Equations

• FreeMonoid.reverse = List.reverse

@[simp]

theorem FreeAddMonoid.reverse_of {α : Type u_1} (a : α) : (FreeAddMonoid.of a).reverse = FreeAddMonoid.of a

@[simp]

theorem FreeMonoid.reverse_of {α : Type u_1} (a : α) : (FreeMonoid.of a).reverse = FreeMonoid.of a

theorem FreeAddMonoid.reverse_add {α : Type u_1} {a : FreeAddMonoid α} {b : FreeAddMonoid α} : (a + b).reverse = b.reverse + a.reverse

theorem FreeMonoid.reverse_mul {α : Type u_1} {a : FreeMonoid α} {b : FreeMonoid α} : (a * b).reverse = b.reverse * a.reverse

@[simp]

theorem FreeAddMonoid.reverse_reverse {α : Type u_1} {a : FreeAddMonoid α} : a.reverse.reverse = a

@[simp]

theorem FreeMonoid.reverse_reverse {α : Type u_1} {a : FreeMonoid α} : a.reverse.reverse = a

@[simp]

theorem FreeAddMonoid.length_reverse {α : Type u_1} {a : FreeAddMonoid α} : a.reverse.length = a.length

@[simp]

theorem FreeMonoid.length_reverse {α : Type u_1} {a : FreeMonoid α} : a.reverse.length = a.length