Documentation

Mathlib.Algebra.FreeMonoid.Basic

Free monoid over a given alphabet #

Main definitions #

def FreeAddMonoid (α : Type u_6) :
Type u_6

Free nonabelian additive monoid over a given alphabet

Equations
Instances For
    def FreeMonoid (α : Type u_6) :
    Type u_6

    Free monoid over a given alphabet.

    Equations
    Instances For
      Equations
      • FreeAddMonoid.instDecidableEqFreeAddMonoid = instDecidableEqList
      Equations
      • FreeMonoid.instDecidableEqFreeMonoid = instDecidableEqList

      The identity equivalence between FreeAddMonoid α and List α.

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

        The identity equivalence between FreeMonoid α and List α.

        Equations
        Instances For

          The identity equivalence between List α and FreeAddMonoid α.

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

            The identity equivalence between List α and FreeMonoid α.

            Equations
            Instances For
              @[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.instAddCancelMonoidFreeAddMonoid.proof_2 {α : Type u_1} :
              ∀ (x : FreeAddMonoid α), nsmulRec 0 x = nsmulRec 0 x
              theorem 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_1FreeAddMonoid.toList x = FreeAddMonoid.toList x_2
              theorem FreeAddMonoid.instAddCancelMonoidFreeAddMonoid.proof_3 {α : Type u_1} :
              ∀ (n : ) (x : FreeAddMonoid α), nsmulRec (n + 1) x = nsmulRec (n + 1) x
              Equations
              • One or more equations did not get rendered due to their size.
              theorem 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_2FreeAddMonoid.toList x_1 = FreeAddMonoid.toList x_2
              Equations
              • One or more equations did not get rendered due to their size.
              Equations
              • FreeAddMonoid.instInhabitedFreeAddMonoid = { default := 0 }
              Equations
              • FreeMonoid.instInhabitedFreeMonoid = { default := 1 }
              @[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 (List.sum xs) = List.join (List.map (FreeAddMonoid.toList) xs)
              @[simp]
              theorem FreeMonoid.toList_prod {α : Type u_1} (xs : List (FreeMonoid α)) :
              FreeMonoid.toList (List.prod xs) = List.join (List.map (FreeMonoid.toList) xs)
              @[simp]
              theorem FreeAddMonoid.ofList_join {α : Type u_1} (xs : List (List α)) :
              FreeAddMonoid.ofList (List.join xs) = List.sum (List.map (FreeAddMonoid.ofList) xs)
              @[simp]
              theorem FreeMonoid.ofList_join {α : Type u_1} (xs : List (List α)) :
              FreeMonoid.ofList (List.join xs) = List.prod (List.map (FreeMonoid.ofList) xs)
              def FreeAddMonoid.of {α : Type u_1} (x : α) :

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

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

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

                Equations
                Instances For
                  @[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
                  def FreeAddMonoid.recOn {α : Type u_1} {C : FreeAddMonoid αSort u_6} (xs : FreeAddMonoid α) (h0 : C 0) (ih : (x : α) → (xs : FreeAddMonoid α) → C xsC (FreeAddMonoid.of x + xs)) :
                  C xs

                  Recursor for FreeAddMonoid using 0 and FreeAddMonoid.of x + xs instead of [] and x :: xs.

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

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

                    Equations
                    Instances For
                      @[simp]
                      theorem FreeAddMonoid.recOn_zero {α : Type u_1} {C : FreeAddMonoid αSort u_6} (h0 : C 0) (ih : (x : α) → (xs : FreeAddMonoid α) → C xsC (FreeAddMonoid.of x + xs)) :
                      @[simp]
                      theorem FreeMonoid.recOn_one {α : Type u_1} {C : FreeMonoid αSort u_6} (h0 : C 1) (ih : (x : α) → (xs : FreeMonoid α) → C xsC (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 xsC (FreeAddMonoid.of x + xs)) :
                      @[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 (FreeMonoid.of x * xs)) :
                      FreeMonoid.recOn (FreeMonoid.of x * xs) h0 ih = ih x xs (FreeMonoid.recOn xs h0 ih)
                      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
                      Instances For
                        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
                        Instances For
                          @[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)) :
                          @[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)) :
                          @[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)) :
                          @[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.casesOn (FreeMonoid.of x * xs) 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 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 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
                          Instances For
                            abbrev FreeAddMonoid.sumAux.match_1 {M : Type u_1} (motive : List MSort u_2) :
                            (x : List M) → (Unitmotive []) → ((x : M) → (xs : List M) → motive (x :: xs)) → motive x
                            Equations
                            Instances For
                              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
                              Instances For
                                abbrev FreeAddMonoid.sumAux_eq.match_1 {M : Type u_1} (motive : List MProp) :
                                (x : List M) → (Unitmotive []) → ((head : M) → (xs : List M) → motive (head :: xs)) → motive x
                                Equations
                                Instances For
                                  theorem FreeAddMonoid.lift.proof_4 {α : Type u_2} {M : Type u_1} [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
                                  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_1 {α : Type u_2} {M : Type u_1} [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
                                  theorem FreeAddMonoid.lift.proof_3 {α : Type u_1} {M : Type u_2} [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)
                                  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.
                                  Instances For
                                    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.
                                    Instances For
                                      @[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.sum (List.map f l)
                                      @[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.prod (List.map f l)
                                      @[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.sum (List.map f (FreeAddMonoid.toList l))
                                      theorem FreeMonoid.lift_apply {α : Type u_1} {M : Type u_4} [Monoid M] (f : αM) (l : FreeMonoid α) :
                                      ↑(FreeMonoid.lift f) l = List.prod (List.map f (FreeMonoid.toList l))
                                      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) :
                                      AddMonoidHom.comp g (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) :
                                      MonoidHom.comp g (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
                                      def FreeAddMonoid.mkAddAction {α : Type u_1} {β : Type u_2} (f : αββ) :

                                      Define an additive action of FreeAddMonoid α on β.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        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 FreeMonoid.mkMulAction {α : Type u_1} {β : Type u_2} (f : αββ) :

                                        Define a multiplicative action of FreeMonoid α on β.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          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 : β) :
                                          @[simp]
                                          theorem FreeMonoid.of_smul {α : Type u_1} {β : Type u_2} (f : αββ) (x : α) (y : β) :
                                          FreeMonoid.of x y = f x y
                                          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)
                                          theorem 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
                                          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
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            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
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              @[simp]
                                              theorem FreeAddMonoid.map_of {α : Type u_1} {β : Type u_2} (f : αβ) (x : α) :
                                              @[simp]
                                              theorem FreeMonoid.map_of {α : Type u_1} {β : Type u_2} (f : αβ) (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 : αβ) :
                                              theorem FreeMonoid.map_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : βγ) (f : αβ) :