Free monoid over a given alphabet

Main definitions

• FreeMonoid α: free monoid over alphabet α; defined as a one-field structure around 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.

structure 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.

• ofList :: (
• toList : List α

  The underlying list

• )

theorem FreeMonoid.ext {α : Type u_6} {x y : FreeMonoid α} (toList : x.toList = y.toList) : x = y

theorem FreeMonoid.ext_iff {α : Type u_6} {x y : FreeMonoid α} : x = y ↔ x.toList = y.toList

structure 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.

• ofList :: (
• toList : List α

  The underlying list

• )

theorem FreeAddMonoid.ext {α : Type u_6} {x y : FreeAddMonoid α} (toList : x.toList = y.toList) : x = y

theorem FreeAddMonoid.ext_iff {α : Type u_6} {x y : FreeAddMonoid α} : x = y ↔ x.toList = y.toList

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[deprecated FreeMonoid.ofList_toList (since := "2026-10-23")]

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

Alias of FreeMonoid.ofList_toList.

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

Alias of FreeAddMonoid.ofList_toList.

@[deprecated FreeMonoid.toList_ofList (since := "2026-10-23")]

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

Alias of FreeMonoid.toList_ofList.

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

Alias of FreeAddMonoid.toList_ofList.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

• FreeMonoid.instInhabited = { default := 1 }

@[instance_reducible]

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

Equations

• FreeAddMonoid.instInhabited = { default := 0 }

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FreeMonoid.ofList_flatten {α : Type u_1} (xs : List (List α)) : { toList := xs.flatten } = (List.map ofList xs).prod

@[simp]

theorem FreeAddMonoid.ofList_flatten {α : Type u_1} (xs : List (List α)) : { toList := xs.flatten } = (List.map ofList xs).sum

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

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

Equations

• FreeMonoid.of x = { toList := [x] }

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

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

Equations

• FreeAddMonoid.of x = { toList := [x] }

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

theorem FreeMonoid.forall {α : Type u_1} {p : FreeMonoid α → Prop} : (∀ (x : FreeMonoid α), p x) ↔ ∀ (l : List α), p { toList := l }

theorem FreeAddMonoid.forall {α : Type u_1} {p : FreeAddMonoid α → Prop} : (∀ (x : FreeAddMonoid α), p x) ↔ ∀ (l : List α), p { toList := l }

theorem FreeMonoid.exists {α : Type u_1} {p : FreeMonoid α → Prop} : (∃ (x : FreeMonoid α), p x) ↔ ∃ (l : List α), p { toList := l }

theorem FreeAddMonoid.exists {α : Type u_1} {p : FreeAddMonoid α → Prop} : (∃ (x : FreeAddMonoid α), p x) ↔ ∃ (l : List α), p { toList := l }

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

The natural equivalence between FreeMonoid α and List α.

Equations

• FreeMonoid.toListEquiv = { toFun := FreeMonoid.toList, invFun := FreeMonoid.ofList, left_inv := ⋯, right_inv := ⋯ }

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

The natural equivalence between FreeAddMonoid α and List α.

Equations

• FreeAddMonoid.toListEquiv = { toFun := FreeAddMonoid.toList, invFun := FreeAddMonoid.ofList, left_inv := ⋯, right_inv := ⋯ }

Length

@[deprecated "use `a.toList.length` instead" (since := "2026-10-23")]

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 = a.toList.length

@[deprecated "use `a.toList.length` instead" (since := "2026-10-23")]

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

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

Equations

• a.length = a.toList.length

@[deprecated List.length_nil (since := "2026-10-23")]

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

@[deprecated List.length_nil (since := "2026-10-23")]

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

@[deprecated List.length_eq_zero_iff (since := "2026-10-23")]

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

@[deprecated List.length_eq_zero_iff (since := "2026-10-23")]

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

@[deprecated List.length_singleton (since := "2026-10-23")]

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

@[deprecated List.length_singleton (since := "2026-10-23")]

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

@[deprecated "no replacement" (since := "2026-10-23")]

theorem FreeMonoid.length_surjective {α : Type u_1} [Nonempty α] : Function.Surjective length

@[deprecated "no replacement" (since := "2026-10-23")]

theorem FreeAddMonoid.length_surjective {α : Type u_1} [Nonempty α] : Function.Surjective length

@[deprecated List.length_eq_one_iff (since := "2026-10-23")]

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

@[deprecated List.length_eq_one_iff (since := "2026-10-23")]

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

@[deprecated List.length_eq_two (since := "2026-10-23")]

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

@[deprecated List.length_eq_two (since := "2026-10-23")]

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

@[deprecated List.length_eq_three (since := "2026-10-23")]

theorem FreeMonoid.length_eq_three {α : Type u_1} {v : FreeMonoid α} : v.length = 3 ↔ ∃ (a : α), ∃ (b : α), ∃ (c : α), v = of a * of b * of c

@[deprecated List.length_eq_three (since := "2026-10-23")]

theorem FreeAddMonoid.length_eq_three {α : Type u_1} {v : FreeAddMonoid α} : v.length = 3 ↔ ∃ (a : α), ∃ (b : α), ∃ (c : α), v = of a + of b + of c

@[deprecated List.length_eq_four (since := "2026-10-23")]

theorem FreeMonoid.length_eq_four {α : Type u_1} {v : FreeMonoid α} : v.length = 4 ↔ ∃ (a : α), ∃ (b : α), ∃ (c : α), ∃ (d : α), v = of a * of b * of c * of d

@[deprecated List.length_eq_four (since := "2026-10-23")]

theorem FreeAddMonoid.length_eq_four {α : Type u_1} {v : FreeAddMonoid α} : v.length = 4 ↔ ∃ (a : α), ∃ (b : α), ∃ (c : α), ∃ (d : α), v = of a + of b + of c + of d

@[deprecated List.length_append (since := "2026-10-23")]

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

@[deprecated List.length_append (since := "2026-10-23")]

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

@[deprecated "use `m ∈ a.toList` instead" (since := "2026-10-23")]

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

Membership in a free monoid element

Equations

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

@[deprecated "use `m ∈ a.toList` instead" (since := "2026-10-23")]

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

Membership in a free additive monoid element

Equations

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

@[instance_reducible, deprecated "use `m ∈ a.toList` instead" (since := "2026-10-23")]

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

Equations

• FreeMonoid.instMembership = { mem := fun (a : FreeMonoid α) (m : α) => m ∈ a.toList }

@[instance_reducible, deprecated "use `m ∈ a.toList` instead" (since := "2026-10-23")]

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

Equations

• FreeAddMonoid.instMembership = { mem := fun (a : FreeAddMonoid α) (m : α) => m ∈ a.toList }

@[deprecated "use `m ∈ a.toList` instead" (since := "2026-10-23")]

theorem FreeMonoid.notMem_one {α : Type u_1} {m : α} : ¬m ∈ 1

@[deprecated "use `m ∈ a.toList` instead" (since := "2026-10-23")]

theorem FreeAddMonoid.notMem_zero {α : Type u_1} {m : α} : ¬m ∈ 0

@[deprecated "use `m ∈ a.toList` instead" (since := "2026-10-23")]

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

@[deprecated "use `m ∈ a.toList` instead" (since := "2026-10-23")]

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

@[deprecated "use `m ∈ a.toList` instead" (since := "2026-10-23")]

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

@[deprecated "use `m ∈ a.toList` instead" (since := "2026-10-23")]

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

@[deprecated "use `m ∈ a.toList` instead" (since := "2026-10-23")]

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

@[deprecated "use `m ∈ a.toList` instead" (since := "2026-10-23")]

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

def FreeMonoid.mulRecOn {α : Type u_1} {motive : FreeMonoid α → Sort u_6} (xs : FreeMonoid α) (one : motive 1) (of_mul : (x : α) → (xs : FreeMonoid α) → motive xs → motive (of x * xs)) : motive xs

Recursor for FreeMonoid using 1 and FreeMonoid.of x * xs.

Equations

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

def FreeAddMonoid.addRecOn {α : Type u_1} {motive : FreeAddMonoid α → Sort u_6} (xs : FreeAddMonoid α) (zero : motive 0) (of_add : (x : α) → (xs : FreeAddMonoid α) → motive xs → motive (of x + xs)) : motive xs

Recursor for FreeAddMonoid using 0 and FreeAddMonoid.of x + xs.

Equations

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

@[simp]

theorem FreeMonoid.mulRecOn_one {α : Type u_1} {motive : FreeMonoid α → Sort u_6} (one : motive 1) (of_mul : (x : α) → (xs : FreeMonoid α) → motive xs → motive (of x * xs)) : mulRecOn 1 one of_mul = one

@[simp]

theorem FreeAddMonoid.addRecOn_zero {α : Type u_1} {motive : FreeAddMonoid α → Sort u_6} (zero : motive 0) (of_add : (x : α) → (xs : FreeAddMonoid α) → motive xs → motive (of x + xs)) : addRecOn 0 zero of_add = zero

@[simp]

theorem FreeMonoid.mulRecOn_of_mul {α : Type u_1} {motive : FreeMonoid α → Sort u_6} (x : α) (xs : FreeMonoid α) (one : motive 1) (of_mul : (x : α) → (xs : FreeMonoid α) → motive xs → motive (of x * xs)) : mulRecOn (of x * xs) one of_mul = of_mul x xs (mulRecOn xs one of_mul)

@[simp]

theorem FreeAddMonoid.addRecOn_of_add {α : Type u_1} {motive : FreeAddMonoid α → Sort u_6} (x : α) (xs : FreeAddMonoid α) (zero : motive 0) (of_add : (x : α) → (xs : FreeAddMonoid α) → motive xs → motive (of x + xs)) : addRecOn (of x + xs) zero of_add = of_add x xs (addRecOn xs zero of_add)

@[deprecated FreeMonoid.mulRecOn_one (since := "2026-10-23")]

theorem FreeMonoid.recOn_one {α : Type u_1} {motive : FreeMonoid α → Sort u_6} (one : motive 1) (of_mul : (x : α) → (xs : FreeMonoid α) → motive xs → motive (of x * xs)) : mulRecOn 1 one of_mul = one

Alias of FreeMonoid.mulRecOn_one.

theorem FreeAddMonoid.recOn_zero {α : Type u_1} {motive : FreeAddMonoid α → Sort u_6} (zero : motive 0) (of_add : (x : α) → (xs : FreeAddMonoid α) → motive xs → motive (of x + xs)) : addRecOn 0 zero of_add = zero

Alias of FreeAddMonoid.addRecOn_zero.

@[deprecated FreeMonoid.mulRecOn_of_mul (since := "2026-10-23")]

theorem FreeMonoid.recOn_of_mul {α : Type u_1} {motive : FreeMonoid α → Sort u_6} (x : α) (xs : FreeMonoid α) (one : motive 1) (of_mul : (x : α) → (xs : FreeMonoid α) → motive xs → motive (of x * xs)) : mulRecOn (of x * xs) one of_mul = of_mul x xs (mulRecOn xs one of_mul)

Alias of FreeMonoid.mulRecOn_of_mul.

theorem FreeAddMonoid.recOn_of_add {α : Type u_1} {motive : FreeAddMonoid α → Sort u_6} (x : α) (xs : FreeAddMonoid α) (zero : motive 0) (of_add : (x : α) → (xs : FreeAddMonoid α) → motive xs → motive (of x + xs)) : addRecOn (of x + xs) zero of_add = of_add x xs (addRecOn xs zero of_add)

Alias of FreeAddMonoid.addRecOn_of_add.

Induction

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

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

theorem FreeAddMonoid.inductionOn {α : Type u_1} {motive : FreeAddMonoid α → Prop} (z : FreeAddMonoid α) (zero : motive 0) (of : ∀ (x : α), motive (of x)) (add : ∀ (x y : FreeAddMonoid α), motive x → motive y → motive (x + y)) : motive z

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

theorem FreeMonoid.inductionOn' {α : Type u_1} {motive : FreeMonoid α → Prop} (a : FreeMonoid α) (one : motive 1) (of_mul : ∀ (b : α) (a : FreeMonoid α), motive a → motive (of b * a)) : motive 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} {motive : FreeAddMonoid α → Prop} (a : FreeAddMonoid α) (zero : motive 0) (of_add : ∀ (b : α) (a : FreeAddMonoid α), motive a → motive (of b + a)) : motive a

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

def FreeMonoid.mulCasesOn {α : Type u_1} {motive : FreeMonoid α → Sort u_6} (xs : FreeMonoid α) (one : motive 1) (of_mul : (x : α) → (xs : FreeMonoid α) → motive (of x * xs)) : motive xs

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

Equations

• FreeMonoid.mulCasesOn xs one of_mul = FreeMonoid.mulRecOn xs one fun (x : α) (xs : FreeMonoid α) (x_1 : motive xs) => of_mul x xs

def FreeAddMonoid.addCasesOn {α : Type u_1} {motive : FreeAddMonoid α → Sort u_6} (xs : FreeAddMonoid α) (zero : motive 0) (of_add : (x : α) → (xs : FreeAddMonoid α) → motive (of x + xs)) : motive xs

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

Equations

• FreeAddMonoid.addCasesOn xs one of_mul = FreeAddMonoid.addRecOn xs one fun (x : α) (xs : FreeAddMonoid α) (x_1 : motive xs) => of_mul x xs

@[simp]

theorem FreeMonoid.mulCasesOn_one {α : Type u_1} {motive : FreeMonoid α → Sort u_6} (one : motive 1) (of_mul : (x : α) → (xs : FreeMonoid α) → motive (of x * xs)) : mulCasesOn 1 one of_mul = one

@[simp]

theorem FreeAddMonoid.addCasesOn_zero {α : Type u_1} {motive : FreeAddMonoid α → Sort u_6} (zero : motive 0) (of_add : (x : α) → (xs : FreeAddMonoid α) → motive (of x + xs)) : addCasesOn 0 zero of_add = zero

@[simp]

theorem FreeMonoid.mulCasesOn_of_mul {α : Type u_1} {motive : FreeMonoid α → Sort u_6} (x : α) (xs : FreeMonoid α) (one : motive 1) (of_mul : (x : α) → (xs : FreeMonoid α) → motive (of x * xs)) : mulCasesOn (of x * xs) one of_mul = of_mul x xs

@[simp]

theorem FreeAddMonoid.addCasesOn_of_add {α : Type u_1} {motive : FreeAddMonoid α → Sort u_6} (x : α) (xs : FreeAddMonoid α) (zero : motive 0) (of_add : (x : α) → (xs : FreeAddMonoid α) → motive (of x + xs)) : addCasesOn (of x + xs) zero of_add = of_add x xs

@[deprecated FreeMonoid.mulCasesOn_one (since := "2026-10-23")]

theorem FreeMonoid.casesOn_one {α : Type u_1} {motive : FreeMonoid α → Sort u_6} (one : motive 1) (of_mul : (x : α) → (xs : FreeMonoid α) → motive (of x * xs)) : mulCasesOn 1 one of_mul = one

Alias of FreeMonoid.mulCasesOn_one.

theorem FreeAddMonoid.casesOn_zero {α : Type u_1} {motive : FreeAddMonoid α → Sort u_6} (zero : motive 0) (of_add : (x : α) → (xs : FreeAddMonoid α) → motive (of x + xs)) : addCasesOn 0 zero of_add = zero

Alias of FreeAddMonoid.addCasesOn_zero.

@[deprecated FreeMonoid.mulCasesOn_of_mul (since := "2026-10-23")]

theorem FreeMonoid.casesOn_of_mul {α : Type u_1} {motive : FreeMonoid α → Sort u_6} (x : α) (xs : FreeMonoid α) (one : motive 1) (of_mul : (x : α) → (xs : FreeMonoid α) → motive (of x * xs)) : mulCasesOn (of x * xs) one of_mul = of_mul x xs

Alias of FreeMonoid.mulCasesOn_of_mul.

theorem FreeAddMonoid.casesOn_of_add {α : Type u_1} {motive : FreeAddMonoid α → Sort u_6} (x : α) (xs : FreeAddMonoid α) (zero : motive 0) (of_add : (x : α) → (xs : FreeAddMonoid α) → motive (of x + xs)) : addCasesOn (of x + xs) zero of_add = of_add x xs

Alias of FreeAddMonoid.addCasesOn_of_add.

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

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)

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

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

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

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

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) { toList := 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) { toList := 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 l.toList).prod

theorem FreeAddMonoid.lift_apply {α : Type u_1} {M : Type u_4} [AddMonoid M] (f : α → M) (l : FreeAddMonoid α) : (lift f) l = (List.map f l.toList).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

@[instance_reducible]

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

Define a multiplicative action of FreeMonoid α on β.

Equations

• FreeMonoid.mkMulAction f = { smul := fun (l : FreeMonoid α) (b : β) => List.foldr f b l.toList, mul_smul := ⋯, one_smul := ⋯ }

@[instance_reducible]

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

Define an additive action of FreeAddMonoid α on β.

Equations

• FreeAddMonoid.mkAddAction f = { vadd := fun (l : FreeAddMonoid α) (b : β) => List.foldr f b l.toList, add_vadd := ⋯, zero_vadd := ⋯ }

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

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

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

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

@[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 : α → β) : 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 α) => { toList := List.map f l.toList }, map_one' := ⋯, map_mul' := ⋯ }

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 α) => { toList := List.map f l.toList }, map_zero' := ⋯, map_add' := ⋯ }

@[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 α) : ((map f) xs).toList = List.map f xs.toList

@[simp]

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

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

theorem FreeAddMonoid.ofList_map {α : Type u_1} {β : Type u_2} (f : α → β) (xs : List α) : { toList := List.map f xs } = (map f) { toList := 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]

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

@[simp]

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

@[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

@[instance_reducible]

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

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

Equations

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

@[instance_reducible]

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

Equations

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

@[simp]

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

@[simp]

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

reverse

@[deprecated "use `star` in `Mathlib.Algebra.Star.Free` instead" (since := "2026-10-23")]

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

Reverse the symbols in a FreeMonoid α.

Equations

• x.reverse = { toList := x.toList.reverse }

@[deprecated "use `star` in `Mathlib.Algebra.Star.Free` instead" (since := "2026-10-23")]

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

Reverses the symbols in a FreeAddMonoid α.

Equations

• x.reverse = { toList := x.toList.reverse }

@[deprecated "use `star_of` in `Mathlib.Algebra.Star.Free` instead" (since := "2026-10-23")]

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

@[deprecated "use `star_of` in `Mathlib.Algebra.Star.Free` instead" (since := "2026-10-23")]

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

@[deprecated "use `star_mul` instead" (since := "2026-10-23")]

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

@[deprecated "use `star_mul` instead" (since := "2026-10-23")]

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

@[deprecated "use `star_star` instead" (since := "2026-10-23")]

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

@[deprecated "use `star_star` instead" (since := "2026-10-23")]

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

@[deprecated List.length_reverse (since := "2026-10-23")]

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

@[deprecated List.length_reverse (since := "2026-10-23")]

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

def FreeMonoid.freeMonoidCongr {α : Type u_6} {β : Type u_7} (e : α ≃ β) : FreeMonoid α ≃* FreeMonoid β

Free monoids over isomorphic types are isomorphic.

Equations

• FreeMonoid.freeMonoidCongr e = { toFun := ⇑(FreeMonoid.map ⇑e), invFun := ⇑(FreeMonoid.map ⇑e.symm), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

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

Free additive monoids over isomorphic types are isomorphic.

Equations

• FreeAddMonoid.freeAddMonoidCongr e = { toFun := ⇑(FreeAddMonoid.map ⇑e), invFun := ⇑(FreeAddMonoid.map ⇑e.symm), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[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.symm_freeMonoidCongr {α : Type u_6} {β : Type u_7} (e : α ≃ β) : (freeMonoidCongr e).symm = freeMonoidCongr e.symm

@[simp]

theorem FreeAddMonoid.symm_freeAddMonoidCongr {α : Type u_6} {β : Type u_7} (e : α ≃ β) : (freeAddMonoidCongr e).symm = freeAddMonoidCongr e.symm

@[deprecated FreeMonoid.freeMonoidCongr_of (since := "2026-10-21")]

theorem FreeMonoid.freeMonoidCongr_symm_of {α : Type u_6} {β : Type u_7} (e : α ≃ β) (b : β) : (freeMonoidCongr e.symm) (of b) = of (e.symm b)

@[deprecated FreeAddMonoid.freeAddMonoidCongr_of (since := "2026-10-21")]

theorem FreeAddMonoid.freeAddMonoidCongr_symm_of {α : Type u_6} {β : Type u_7} (e : α ≃ β) (b : β) : (freeAddMonoidCongr e.symm) (of b) = of (e.symm b)