Products of the lists List.ofFn f

In a monoid, the product of the letters β (w 0) ⋯ β (w (n + 1)) of a word w obtained from a word u of length n by inserting two consecutive letters d, e at the positions p and p + 1 factors as L * β d * β e * R, where L and R depend only on u and p (List.exists_prod_ofFn_insertNth_insertNth). This is how a relation among the products β d * β e passes to the products of all words carrying the letters d, e in a fixed position.

A nonempty product f₀ f₁ ⋯ fₙ is the left fold of f₁, …, fₙ starting from f₀ (List.prod_ofFn_eq_foldl), and multiplicative maps, not necessarily unital, preserve such left folds (List.map_foldl_ofFn_mul). Together they move nonempty products through nonunital homomorphisms.

The product of a word whose letters all equal c except for a single letter a in position p is c ^ p * a * c ^ (n - p) (List.prod_ofFn_ite).

theorem List.exists_prod_ofFn_insertNth_insertNth {D : Type u_1} {M : Type u_2} [Monoid M] (β : D → M) {n : ℕ} (p : Fin (n + 1)) (u : Fin n → D) : ∃ (L : M), ∃ (R : M), ∀ (d e : D), (ofFn fun (t : Fin (n + 1 + 1)) => β (p.castSucc.insertNth d (p.insertNth e u) t)).prod = L * β d * β e * R

Inserting two consecutive letters d, e into a word multiplies its product by β d * β e in a fixed position.

theorem List.prod_ofFn_eq_foldl {M : Type u_1} [Monoid M] {n : ℕ} (f : Fin (n + 1) → M) : (ofFn f).prod = foldl (fun (x1 x2 : M) => x1 * x2) (f 0) (ofFn fun (i : Fin n) => f i.succ)

A nonempty product f₀ f₁ ⋯ fₙ is the left fold of f₁, …, fₙ starting from f₀.

theorem List.map_foldl_ofFn_mul {F : Type u_1} {R : Type u_2} {S : Type u_3} [Mul R] [Mul S] [FunLike F R S] [MulHomClass F R S] (g : F) {n : ℕ} (f : Fin n → R) (x : R) : g (foldl (fun (x1 x2 : R) => x1 * x2) x (ofFn f)) = foldl (fun (x1 x2 : S) => x1 * x2) (g x) (ofFn fun (i : Fin n) => g (f i))

A multiplicative map, not necessarily unital, carries a left fold of products to the left fold of the images.

theorem List.prod_ofFn_ite {M : Type u_1} [Monoid M] (a c : M) (n : ℕ) (p : Fin (n + 1)) : (ofFn fun (i : Fin (n + 1)) => if i = p then a else c).prod = c ^ ↑p * a * c ^ (n - ↑p)

The product of a word of length n + 1 whose letters all equal c except for the letter a in position p is c ^ p * a * c ^ (n - p).