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 α→ FreeMonoid α sending each element x to [x];
• FreeMonoid.lift: natural equivalence between α → M→ M and FreeMonoid α →* M→* M
• FreeMonoid.map: embedding of α → β→ β into FreeMonoid α →* FreeMonoid β→* FreeMonoid β given by List.map.

ink

def FreeAddMonoid (α : Type u_1) : Type u_1

Free nonabelian additive monoid over a given alphabet

Equations

• FreeAddMonoid α = List α

ink

def FreeMonoid (α : Type u_1) : Type u_1

Free monoid over a given alphabet.

Equations

• FreeMonoid α = List α

ink

instance FreeAddMonoid.instDecidableEqFreeAddMonoid {α : Type u_1} [inst : DecidableEq α] : DecidableEq (FreeAddMonoid α)

Equations

• FreeAddMonoid.instDecidableEqFreeAddMonoid = instDecidableEqList

ink

instance FreeMonoid.instDecidableEqFreeMonoid {α : Type u_1} [inst : DecidableEq α] : DecidableEq (FreeMonoid α)

Equations

• FreeMonoid.instDecidableEqFreeMonoid = instDecidableEqList

ink

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

The identity equivalence between FreeAddMonoid α and List α.

Equations

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

ink

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

The identity equivalence between FreeMonoid α and List α.

Equations

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

ink

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

The identity equivalence between List α and FreeAddMonoid α.

Equations

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

ink

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

The identity equivalence between List α and FreeMonoid α.

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

def FreeAddMonoid.instAddCancelMonoidFreeAddMonoid.proof_1 {α : 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

Equations

• One or more equations did not get rendered due to their size.

ink

def FreeAddMonoid.instAddCancelMonoidFreeAddMonoid.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

Equations

• One or more equations did not get rendered due to their size.

ink

def FreeAddMonoid.instAddCancelMonoidFreeAddMonoid.proof_3 {α : Type u_1} : ∀ (n : ℕ) (x : FreeAddMonoid α), nsmulRec (n + 1) x = nsmulRec (n + 1) x

Equations

• (_ : nsmulRec (n + 1) x = nsmulRec (n + 1) x) = (_ : nsmulRec (n + 1) x = nsmulRec (n + 1) x)

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

def FreeAddMonoid.instAddCancelMonoidFreeAddMonoid.proof_2 {α : Type u_1} : ∀ (x : FreeAddMonoid α), nsmulRec 0 x = nsmulRec 0 x

Equations

• (_ : nsmulRec 0 x = nsmulRec 0 x) = (_ : nsmulRec 0 x = nsmulRec 0 x)

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• FreeAddMonoid.instInhabitedFreeAddMonoid = { default := 0 }

ink

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

Equations

• FreeMonoid.instInhabitedFreeMonoid = { default := 1 }

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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]

ink

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]

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

def FreeAddMonoid.recOn {α : Type u_1} {C : FreeAddMonoid α → Sort u_2} (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 + xs instead of [] and x :: xs.

Equations

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

ink

def FreeMonoid.recOn {α : Type u_1} {C : FreeMonoid α → Sort u_2} (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

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

def FreeAddMonoid.casesOn {α : Type u_1} {C : FreeAddMonoid α → Sort u_2} (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

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

ink

def FreeMonoid.casesOn {α : Type u_1} {C : FreeMonoid α → Sort u_2} (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

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

def FreeAddMonoid.sumAux {M : Type u_1} [inst : 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 x = FreeAddMonoid.sumAux.match_1 (fun x => M) x (fun _ => 0) fun x xs => List.foldl (fun x x_1 => x + x_1) x xs

ink

abbrev FreeAddMonoid.sumAux.match_1 {M : Type u_1} (motive : List M → Sort u_2) : (x : List M) → (Unit → motive []) → ((x : M) → (xs : List M) → motive (x :: xs)) → motive x

Equations

• FreeAddMonoid.sumAux.match_1 motive x h_1 h_2 = List.casesOn x (h_1 ()) fun head tail => h_2 head tail

ink

def FreeMonoid.prodAux {M : Type u_1} [inst : 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 x = match x with | [] => 1 | x :: xs => List.foldl (fun x x_1 => x * x_1) x xs

ink

abbrev FreeAddMonoid.sumAux_eq.match_1 {M : Type u_1} (motive : List M → Prop) : (x : List M) → (Unit → motive []) → ((head : M) → (xs : List M) → motive (head :: xs)) → motive x

Equations

• FreeAddMonoid.sumAux_eq.match_1 motive x h_1 h_2 = List.casesOn x (h_1 ()) fun head tail => h_2 head tail

ink

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

ink

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

ink

def FreeAddMonoid.lift.proof_4 {α : Type u_1} {M : Type u_2} [inst : AddMonoid M] (f : FreeAddMonoid α →+ M) : (fun f => { toZeroHom := { toFun := fun l => FreeAddMonoid.sumAux (List.map f (↑FreeAddMonoid.toList l)), map_zero' := (_ : (fun l => FreeAddMonoid.sumAux (List.map f (↑FreeAddMonoid.toList l))) 0 = (fun l => FreeAddMonoid.sumAux (List.map f (↑FreeAddMonoid.toList l))) 0) }, map_add' := (_ : ∀ (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))) }) ((fun f x => ↑f (FreeAddMonoid.of x)) f) = f

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

def FreeAddMonoid.lift.proof_2 {α : Type u_1} {M : Type u_2} [inst : 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))

Equations

• One or more equations did not get rendered due to their size.

ink

def FreeAddMonoid.lift.proof_3 {α : Type u_1} {M : Type u_2} [inst : AddMonoid M] (f : α → M) : (fun f x => ↑f (FreeAddMonoid.of x)) ((fun f => { toZeroHom := { toFun := fun l => FreeAddMonoid.sumAux (List.map f (↑FreeAddMonoid.toList l)), map_zero' := (_ : (fun l => FreeAddMonoid.sumAux (List.map f (↑FreeAddMonoid.toList l))) 0 = (fun l => FreeAddMonoid.sumAux (List.map f (↑FreeAddMonoid.toList l))) 0) }, map_add' := (_ : ∀ (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))) }) f) = (fun f x => ↑f (FreeAddMonoid.of x)) ((fun f => { toZeroHom := { toFun := fun l => FreeAddMonoid.sumAux (List.map f (↑FreeAddMonoid.toList l)), map_zero' := (_ : (fun l => FreeAddMonoid.sumAux (List.map f (↑FreeAddMonoid.toList l))) 0 = (fun l => FreeAddMonoid.sumAux (List.map f (↑FreeAddMonoid.toList l))) 0) }, map_add' := (_ : ∀ (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))) }) f)

Equations

• One or more equations did not get rendered due to their size.

ink

def FreeAddMonoid.lift {α : Type u_1} {M : Type u_2} [inst : AddMonoid M] : (α → M) ≃ (FreeAddMonoid α →+ M)

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

Equations

• One or more equations did not get rendered due to their size.

ink

def FreeMonoid.lift {α : Type u_1} {M : Type u_2} [inst : Monoid M] : (α → M) ≃ (FreeMonoid α →* M)

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

theorem FreeMonoid.lift_restrict {α : Type u_1} {M : Type u_2} [inst : Monoid M] (f : FreeMonoid α →* M) : ↑FreeMonoid.lift (↑f ∘ FreeMonoid.of) = f

ink

theorem FreeAddMonoid.comp_lift {α : Type u_3} {M : Type u_1} [inst : AddMonoid M] {N : Type u_2} [inst : AddMonoid N] (g : M →+ N) (f : α → M) : AddMonoidHom.comp g (↑FreeAddMonoid.lift f) = ↑FreeAddMonoid.lift (↑g ∘ f)

ink

theorem FreeMonoid.comp_lift {α : Type u_3} {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst : Monoid N] (g : M →* N) (f : α → M) : MonoidHom.comp g (↑FreeMonoid.lift f) = ↑FreeMonoid.lift (↑g ∘ f)

ink

theorem FreeAddMonoid.hom_map_lift {α : Type u_3} {M : Type u_1} [inst : AddMonoid M] {N : Type u_2} [inst : AddMonoid N] (g : M →+ N) (f : α → M) (x : FreeAddMonoid α) : ↑g (↑(↑FreeAddMonoid.lift f) x) = ↑(↑FreeAddMonoid.lift (↑g ∘ f)) x

ink

theorem FreeMonoid.hom_map_lift {α : Type u_3} {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst : Monoid N] (g : M →* N) (f : α → M) (x : FreeMonoid α) : ↑g (↑(↑FreeMonoid.lift f) x) = ↑(↑FreeMonoid.lift (↑g ∘ f)) x

ink

def 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)

Equations

• One or more equations did not get rendered due to their size.

ink

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

Define an additive action of FreeAddMonoid α on β.

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• (_ : 0 +ᵥ x = 0 +ᵥ x) = (_ : 0 +ᵥ x = 0 +ᵥ x)

ink

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

Define a multiplicative action of FreeMonoid α on β.

Equations

• One or more equations did not get rendered due to their size.

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

def 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)

Equations

• One or more equations did not get rendered due to their size.

ink

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

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

Equations

• One or more equations did not get rendered due to their size.

ink

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

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

Equations

• One or more equations did not get rendered due to their size.

ink

@[simp]

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

ink

@[simp]

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

ink

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)

ink

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)

ink

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)

ink

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)

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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