feat(algebra/free_monoid): action of the free_monoid (#16746)

src/algebra/free_monoid.lean

@@ -107,6 +107,17 @@ by { ext, simp }
 lemma hom_map_lift (g : M →* N) (f : α → M) (x : free_monoid α) : g (lift f x) = lift (g ∘ f) x :=
 monoid_hom.ext_iff.1 (comp_lift g f) x
 
+/-- Define a multiplicative action of `free_monoid α` on `β`. -/
+@[to_additive "Define an additive action of `free_add_monoid α` on `β`."]
+def mk_mul_action (f : α → β → β) : mul_action (free_monoid α) β :=
+{ smul := λ l b, list.foldr f b l,
+  one_smul := λ x, rfl,
+  mul_smul := λ xs ys b, list.foldr_append _ _ _ _ }
+
+@[simp, to_additive] lemma of_smul (f : α → β → β) (x : α) (y : β) :
+  (by haveI := mk_mul_action f; exact of x • y) = f x y :=
+rfl
+
 /-- The unique monoid homomorphism `free_monoid α →* free_monoid β` that sends
 each `of x` to `of (f x)`. -/
 @[to_additive "The unique additive monoid homomorphism `free_add_monoid α →+ free_add_monoid β`
@@ -127,4 +138,7 @@ hom_eq $ λ x, rfl
 lemma map_comp (g : β → γ) (f : α → β) : map (g ∘ f) = (map g).comp (map f) :=
 hom_eq $ λ x, rfl
 
+@[simp, to_additive] lemma map_id : map (@id α) = monoid_hom.id (free_monoid α) :=
+hom_eq $ λ x, rfl
+
 end free_monoid