Mathlib.Algebra.BigOperators.Group.List.Basic

List.prod_eq_foldl theorem

: ∀ {l : List M}, l.prod = foldl (· * ·) 1 l

Full source

@[to_additive]
theorem prod_eq_foldl : ∀ {l : List M}, l.prod = foldl (· * ·) 1 l
  | [] => rfl
  | cons a l => by
    rw [prod_cons, prod_eq_foldl, ← foldl_assoc (α := M) (op := (· * ·))]
    simp

Product of List Equals Left Fold with Multiplication

Informal description

For any list $l$ of elements in a monoid $M$, the product of the elements in $l$ is equal to the left-fold of the list using the monoid multiplication operation with initial value $1$, i.e., $\text{prod}(l) = \text{foldl}(\cdot * \cdot, 1, l)$.

List.prod_append theorem

: (l₁ ++ l₂).prod = l₁.prod * l₂.prod

Full source

@[to_additive (attr := simp)]
theorem prod_append : (l₁ ++ l₂).prod = l₁.prod * l₂.prod :=
  calc
    (l₁ ++ l₂).prod = foldr (· * ·) (1 * foldr (· * ·) 1 l₂) l₁ := by simp [List.prod]
    _ = l₁.prod * l₂.prod := foldr_assoc

Product of Concatenated Lists Equals Product of Parts

Informal description

For any two lists $l_1$ and $l_2$ of elements in a monoid $M$, the product of the concatenated list $l_1 \mathbin{+\!\!\!+} l_2$ is equal to the product of $l_1$ multiplied by the product of $l_2$, i.e., $(l_1 \mathbin{+\!\!\!+} l_2).\text{prod} = l_1.\text{prod} \cdot l_2.\text{prod}$.

List.prod_concat theorem

: (l.concat a).prod = l.prod * a

Full source

@[to_additive]
theorem prod_concat : (l.concat a).prod = l.prod * a := by
  rw [concat_eq_append, prod_append, prod_singleton]

Product of List with Appended Element Equals Product Times Element

Informal description

For any list $l$ of elements in a monoid $M$ and any element $a \in M$, the product of the list obtained by appending $a$ to $l$ (denoted $l.\text{concat}\ a$) is equal to the product of $l$ multiplied by $a$, i.e., $(l.\text{concat}\ a).\text{prod} = l.\text{prod} \cdot a$.

List.prod_flatten theorem

{l : List (List M)} : l.flatten.prod = (l.map List.prod).prod

Full source

@[to_additive (attr := simp)]
theorem prod_flatten {l : List (List M)} : l.flatten.prod = (l.map List.prod).prod := by
  induction l with
  | nil => simp
  | cons head tail ih => simp only [*, List.flatten, map, prod_append, prod_cons]

Product of Flattened List Equals Product of Sublist Products

Informal description

For any list of lists $l$ of elements in a monoid $M$, the product of the flattened list $l.\text{flatten}$ is equal to the product of the list obtained by mapping the product function over each sublist of $l$, i.e., $\prod (\text{flatten}\ l) = \prod (\text{map}\ \prod\ l)$.

List.rel_prod theorem

{R : M → N → Prop} (h : R 1 1) (hf : (R ⇒ R ⇒ R) (· * ·) (· * ·)) : (Forall₂ R ⇒ R) prod prod

Full source

@[to_additive]
theorem rel_prod {R : M → N → Prop} (h : R 1 1) (hf : (R ⇒ R ⇒ R) (· * ·) (· * ·)) :
    (Forall₂Forall₂ R ⇒ R) prod prod :=
  rel_foldr hf h

Preservation of List Product Under Element-wise Relation $R$

Informal description

Let $M$ and $N$ be monoids with multiplicative operations $(\cdot)$ and identities $1$. Given a binary relation $R : M \to N \to \text{Prop}$ such that: 1. $R(1,1)$ holds, and 2. For all $x_1, x_2 \in M$ and $y_1, y_2 \in N$, if $R(x_1, y_1)$ and $R(x_2, y_2)$ hold, then $R(x_1 \cdot x_2, y_1 \cdot y_2)$ holds. Then for any two lists $l_1 : \text{List}\ M$ and $l_2 : \text{List}\ N$ related by $\text{Forall}_2\ R\ l_1\ l_2$ (i.e., element-wise via $R$), we have $R(\text{prod}\ l_1, \text{prod}\ l_2)$, where $\text{prod}$ denotes the product of all elements in the list.

List.prod_hom_nonempty theorem

{l : List M} {F : Type*} [FunLike F M N] [MulHomClass F M N] (f : F) (hl : l ≠ []) : (l.map f).prod = f l.prod

Full source

@[to_additive]
theorem prod_hom_nonempty {l : List M} {F : Type*} [FunLike F M N] [MulHomClass F M N] (f : F)
    (hl : l ≠ []) : (l.map f).prod = f l.prod :=
  match l, hl with | x :: xs, hl => by induction xs generalizing x <;> aesop

Homomorphism Property for Nonempty List Products: $\prod f(x) = f(\prod x)$

Informal description

Let $M$ and $N$ be multiplicative structures, and let $f \colon M \to N$ be a multiplication-preserving homomorphism. For any nonempty list $l$ of elements of $M$, the product of the list obtained by applying $f$ to each element of $l$ is equal to $f$ applied to the product of $l$. That is, \[ \prod_{x \in l} f(x) = f\left(\prod_{x \in l} x\right). \]

List.prod_hom theorem

(l : List M) {F : Type*} [FunLike F M N] [MonoidHomClass F M N] (f : F) : (l.map f).prod = f l.prod

Full source

@[to_additive]
theorem prod_hom (l : List M) {F : Type*} [FunLike F M N] [MonoidHomClass F M N] (f : F) :
    (l.map f).prod = f l.prod := by
  simp only [prod, foldr_map, ← map_one f]
  exact l.foldr_hom f (fun x y => (map_mul f x y).symm)

Homomorphism Property for List Products: $\prod f(x) = f(\prod x)$

Informal description

Let $M$ and $N$ be monoids, and let $f \colon M \to N$ be a monoid homomorphism. For any list $l$ of elements of $M$, the product of the list obtained by applying $f$ to each element of $l$ is equal to $f$ applied to the product of $l$. That is, \[ \prod_{x \in l} f(x) = f\left(\prod_{x \in l} x\right). \]

List.prod_hom₂_nonempty theorem

 {l : List ι} (f : M → N → P) (hf : ∀ a b c d, f (a * b) (c * d) = f a c * f b d) (f₁ : ι → M) (f₂ : ι → N)
  (hl : l ≠ []) : (l.map fun i => f (f₁ i) (f₂ i)).prod = f (l.map f₁).prod (l.map f₂).prod

Full source

@[to_additive]
theorem prod_hom₂_nonempty {l : List ι} (f : M → N → P)
    (hf : ∀ a b c d, f (a * b) (c * d) = f a c * f b d) (f₁ : ι → M) (f₂ : ι → N) (hl : l ≠ []) :
    (l.map fun i => f (f₁ i) (f₂ i)).prod = f (l.map f₁).prod (l.map f₂).prod := by
  match l, hl with | x :: xs, hl => induction xs generalizing x <;> aesop

Product Homomorphism Property for Nonempty Lists

Informal description

Let $M$, $N$, $P$ be monoids, and let $f : M \to N \to P$ be a function satisfying the property that for all $a, b \in M$ and $c, d \in N$, we have $f(a \cdot b, c \cdot d) = f(a, c) \cdot f(b, d)$. Given a nonempty list $l$ of elements of type $\iota$, and functions $f_1 : \iota \to M$ and $f_2 : \iota \to N$, the product of the list obtained by mapping each element $i \in l$ to $f(f_1(i), f_2(i))$ is equal to $f$ applied to the product of the list obtained by mapping $f_1$ over $l$ and the product of the list obtained by mapping $f_2$ over $l$. That is, \[ \prod_{i \in l} f(f_1(i), f_2(i)) = f\left(\prod_{i \in l} f_1(i), \prod_{i \in l} f_2(i)\right). \]

List.prod_hom₂ theorem

 (l : List ι) (f : M → N → P) (hf : ∀ a b c d, f (a * b) (c * d) = f a c * f b d) (hf' : f 1 1 = 1) (f₁ : ι → M)
  (f₂ : ι → N) : (l.map fun i => f (f₁ i) (f₂ i)).prod = f (l.map f₁).prod (l.map f₂).prod

Full source

@[to_additive]
theorem prod_hom₂ (l : List ι) (f : M → N → P) (hf : ∀ a b c d, f (a * b) (c * d) = f a c * f b d)
    (hf' : f 1 1 = 1) (f₁ : ι → M) (f₂ : ι → N) :
    (l.map fun i => f (f₁ i) (f₂ i)).prod = f (l.map f₁).prod (l.map f₂).prod := by
  rw [prod, prod, prod, foldr_map, foldr_map, foldr_map,
    ← l.foldr_hom₂ f _ _ (fun x y => f (f₁ x) (f₂ x) * y) _ _ (by simp [hf]), hf']

Product Homomorphism Property for Lists of Monoid Elements

Informal description

Let $M$, $N$, $P$ be monoids and let $f : M \to N \to P$ be a function satisfying: 1. For all $a, b \in M$ and $c, d \in N$, we have $f(a \cdot b, c \cdot d) = f(a, c) \cdot f(b, d)$. 2. $f(1, 1) = 1$. Then for any list $l$ of elements of type $\iota$ and functions $f_1 : \iota \to M$, $f_2 : \iota \to N$, the product of the list obtained by applying $f$ component-wise to $(f_1(i), f_2(i))$ for each $i \in l$ equals $f$ applied to the products of the lists obtained by mapping $f_1$ and $f_2$ over $l$ respectively. That is, \[ \prod_{i \in l} f(f_1(i), f_2(i)) = f\left(\prod_{i \in l} f_1(i), \prod_{i \in l} f_2(i)\right). \]

List.prod_map_mul theorem

 {α : Type*} [CommMonoid α] {l : List ι} {f g : ι → α} :
  (l.map fun i => f i * g i).prod = (l.map f).prod * (l.map g).prod

Full source

@[to_additive (attr := simp)]
theorem prod_map_mul {α : Type*} [CommMonoid α] {l : List ι} {f g : ι → α} :
    (l.map fun i => f i * g i).prod = (l.map f).prod * (l.map g).prod :=
  l.prod_hom₂ (· * ·) mul_mul_mul_comm (mul_one _) _ _

Product of Pointwise Products Equals Product of Products in a Commutative Monoid

Informal description

Let $\alpha$ be a commutative monoid, and let $l$ be a list of elements of type $\iota$. For any two functions $f, g : \iota \to \alpha$, the product of the list obtained by mapping each element $i \in l$ to $f(i) \cdot g(i)$ is equal to the product of the list obtained by mapping $f$ over $l$ multiplied by the product of the list obtained by mapping $g$ over $l$. That is, \[ \prod_{i \in l} (f(i) \cdot g(i)) = \left(\prod_{i \in l} f(i)\right) \cdot \left(\prod_{i \in l} g(i)\right). \]

List.prod_map_hom theorem

 (L : List ι) (f : ι → M) {G : Type*} [FunLike G M N] [MonoidHomClass G M N] (g : G) :
  (L.map (g ∘ f)).prod = g (L.map f).prod

Full source

@[to_additive]
theorem prod_map_hom (L : List ι) (f : ι → M) {G : Type*} [FunLike G M N] [MonoidHomClass G M N]
    (g : G) :
    (L.map (g ∘ f)).prod = g (L.map f).prod := by rw [← prod_hom, map_map]

Homomorphism Property for List Products under Composition: $\prod g(f(x)) = g(\prod f(x))$

Informal description

Let $M$ and $N$ be monoids, and let $g \colon M \to N$ be a monoid homomorphism. For any list $L$ of elements of type $\iota$ and any function $f \colon \iota \to M$, the product of the list obtained by applying $g \circ f$ to each element of $L$ is equal to $g$ applied to the product of the list obtained by mapping $f$ over $L$. That is, \[ \prod_{i \in L} g(f(i)) = g\left(\prod_{i \in L} f(i)\right). \]

List.prod_take_mul_prod_drop theorem

(L : List M) (i : ℕ) : (L.take i).prod * (L.drop i).prod = L.prod

Full source

@[to_additive (attr := simp)]
theorem prod_take_mul_prod_drop (L : List M) (i : ℕ) :
    (L.take i).prod * (L.drop i).prod = L.prod := by
  simp [← prod_append]

Product of Take and Drop Equals Total Product in a Monoid

Informal description

For any list $L$ of elements in a monoid $M$ and any natural number $i$, the product of the first $i$ elements of $L$ multiplied by the product of the remaining elements equals the product of the entire list. That is, $\prod(\text{take}(L, i)) \cdot \prod(\text{drop}(L, i)) = \prod(L)$.

List.prod_take_succ theorem

(L : List M) (i : ℕ) (p : i < L.length) : (L.take (i + 1)).prod = (L.take i).prod * L[i]

Full source

@[to_additive (attr := simp)]
theorem prod_take_succ (L : List M) (i : ℕ) (p : i < L.length) :
    (L.take (i + 1)).prod = (L.take i).prod * L[i] := by
  rw [← take_concat_get' _ _ p, prod_append]
  simp

Recursive Product Formula for List Segments in a Monoid

Informal description

For any list $L$ of elements in a monoid $M$ and any natural number $i$ such that $i$ is less than the length of $L$, the product of the first $i+1$ elements of $L$ is equal to the product of the first $i$ elements multiplied by the $(i+1)$-th element of $L$. That is, \[ \prod(\text{take}(L, i+1)) = \prod(\text{take}(L, i)) \cdot L[i]. \]

List.length_pos_of_prod_ne_one theorem

(L : List M) (h : L.prod ≠ 1) : 0 < L.length

Full source

/-- A list with product not one must have positive length. -/
@[to_additive "A list with sum not zero must have positive length."]
theorem length_pos_of_prod_ne_one (L : List M) (h : L.prod ≠ 1) : 0 < L.length := by
  cases L
  · simp at h
  · simp

Non-identity Product Implies Non-empty List in a Monoid

Informal description

For any list $L$ of elements in a monoid $M$, if the product of the elements in $L$ is not equal to the multiplicative identity $1$, then the length of $L$ is positive, i.e., $0 < \text{length}(L)$.

List.length_pos_of_one_lt_prod theorem

[Preorder M] (L : List M) (h : 1 < L.prod) : 0 < L.length

Full source

/-- A list with product greater than one must have positive length. -/
@[to_additive length_pos_of_sum_pos "A list with positive sum must have positive length."]
theorem length_pos_of_one_lt_prod [Preorder M] (L : List M) (h : 1 < L.prod) : 0 < L.length :=
  length_pos_of_prod_ne_one L h.ne'

Non-empty List from Product Greater Than One in a Monoid

Informal description

For any list $L$ of elements in a monoid $M$ equipped with a preorder, if the product of the elements in $L$ is strictly greater than the multiplicative identity $1$, then the length of $L$ is positive, i.e., $0 < \text{length}(L)$.

List.length_pos_of_prod_lt_one theorem

[Preorder M] (L : List M) (h : L.prod < 1) : 0 < L.length

Full source

/-- A list with product less than one must have positive length. -/
@[to_additive "A list with negative sum must have positive length."]
theorem length_pos_of_prod_lt_one [Preorder M] (L : List M) (h : L.prod < 1) : 0 < L.length :=
  length_pos_of_prod_ne_one L h.ne

Non-empty List from Product Less Than One in Preordered Monoid

Informal description

For any list $L$ of elements in a preordered monoid $M$, if the product of the elements in $L$ is strictly less than the multiplicative identity $1$, then the length of $L$ is positive, i.e., $0 < \text{length}(L)$.

List.prod_set theorem

 :
  ∀ (L : List M) (n : ℕ) (a : M),
    (L.set n a).prod = ((L.take n).prod * if n < L.length then a else 1) * (L.drop (n + 1)).prod

Full source

@[to_additive]
theorem prod_set :
    ∀ (L : List M) (n : ℕ) (a : M),
      (L.set n a).prod =
        ((L.take n).prod * if n < L.length then a else 1) * (L.drop (n + 1)).prod
  | x :: xs, 0, a => by simp [set]
  | x :: xs, i + 1, a => by
    simp [set, prod_set xs i a, mul_assoc, Nat.add_lt_add_iff_right]
  | [], _, _ => by simp [set, (Nat.zero_le _).not_lt, Nat.zero_le]

Product of List with Modified Element in Monoid

Informal description

For any list $L$ of elements in a monoid $M$, any natural number $n$, and any element $a \in M$, the product of the list obtained by setting the $n$-th element of $L$ to $a$ is equal to the product of the first $n$ elements of $L$ multiplied by $a$ (if $n$ is a valid index in $L$) or $1$ (otherwise), and then multiplied by the product of the remaining elements after the $(n+1)$-th position. That is, \[ \text{prod}(L.\text{set}(n, a)) = \left(\text{prod}(L.\text{take}(n)) \cdot \begin{cases} a & \text{if } n < \text{length}(L) \\ 1 & \text{otherwise} \end{cases}\right) \cdot \text{prod}(L.\text{drop}(n+1)). \]

List.getElem?_zero_mul_tail_prod theorem

(l : List M) : l[0]?.getD 1 * l.tail.prod = l.prod

Full source

/-- We'd like to state this as `L.headI * L.tail.prod = L.prod`, but because `L.headI` relies on an
inhabited instance to return a garbage value on the empty list, this is not possible.
Instead, we write the statement in terms of `L[0]?.getD 1`.
-/
@[to_additive "We'd like to state this as `L.headI + L.tail.sum = L.sum`, but because `L.headI`
  relies on an inhabited instance to return a garbage value on the empty list, this is not possible.
  Instead, we write the statement in terms of `L[0]?.getD 0`."]
theorem getElem?_zero_mul_tail_prod (l : List M) : l[0]?.getD 1 * l.tail.prod = l.prod := by
  cases l <;> simp

Product of List Head and Tail Equals Total Product in Monoid

Informal description

For any list $l$ of elements in a monoid $M$, the product of the first element (with a default value of $1$ if the list is empty) and the product of the tail of the list equals the product of the entire list. That is, $l[0]_\text{default} \cdot \text{prod}(l_{\text{tail}}) = \text{prod}(l)$, where $l[0]_\text{default}$ is the first element of $l$ if it exists, and $1$ otherwise.

List.headI_mul_tail_prod_of_ne_nil theorem

[Inhabited M] (l : List M) (h : l ≠ []) : l.headI * l.tail.prod = l.prod

Full source

/-- Same as `get?_zero_mul_tail_prod`, but avoiding the `List.headI` garbage complication by
  requiring the list to be nonempty. -/
@[to_additive "Same as `get?_zero_add_tail_sum`, but avoiding the `List.headI` garbage complication
  by requiring the list to be nonempty."]
theorem headI_mul_tail_prod_of_ne_nil [Inhabited M] (l : List M) (h : l ≠ []) :
    l.headI * l.tail.prod = l.prod := by cases l <;> [contradiction; simp]

Product of Head and Tail Equals Total Product for Nonempty Lists in Monoid

Informal description

For any nonempty list $l$ of elements in a monoid $M$, the product of the first element (using the default value if the list is empty) and the product of the tail of the list equals the product of the entire list. That is, $\text{head}(l) \cdot \text{prod}(\text{tail}(l)) = \text{prod}(l)$, where $\text{head}(l)$ is the first element of $l$ and $\text{tail}(l)$ is the list without its first element.

Commute.list_prod_right theorem

(l : List M) (y : M) (h : ∀ x ∈ l, Commute y x) : Commute y l.prod

Full source

@[to_additive]
theorem _root_.Commute.list_prod_right (l : List M) (y : M) (h : ∀ x ∈ l, Commute y x) :
    Commute y l.prod := by
  induction l with
  | nil => simp
  | cons z l IH =>
    rw [List.forall_mem_cons] at h
    rw [List.prod_cons]
    exact Commute.mul_right h.1 (IH h.2)

Commutation with Product of Commuting Elements in List

Informal description

Let $M$ be a monoid, $l$ be a list of elements in $M$, and $y \in M$. If $y$ commutes with every element $x$ in $l$ (i.e., $y \cdot x = x \cdot y$ for all $x \in l$), then $y$ commutes with the product of all elements in $l$ (i.e., $y \cdot \prod_{x \in l} x = (\prod_{x \in l} x) \cdot y$).

Commute.list_prod_left theorem

(l : List M) (y : M) (h : ∀ x ∈ l, Commute x y) : Commute l.prod y

Full source

@[to_additive]
theorem _root_.Commute.list_prod_left (l : List M) (y : M) (h : ∀ x ∈ l, Commute x y) :
    Commute l.prod y :=
  ((Commute.list_prod_right _ _) fun _ hx => (h _ hx).symm).symm

Product of Commuting Elements Commutes with Fixed Element

Informal description

Let $M$ be a monoid, $l$ be a list of elements in $M$, and $y \in M$. If every element $x$ in $l$ commutes with $y$ (i.e., $x \cdot y = y \cdot x$ for all $x \in l$), then the product of all elements in $l$ commutes with $y$ (i.e., $(\prod_{x \in l} x) \cdot y = y \cdot (\prod_{x \in l} x)$).

List.prod_range_succ theorem

(f : ℕ → M) (n : ℕ) : ((range n.succ).map f).prod = ((range n).map f).prod * f n

Full source

@[to_additive] lemma prod_range_succ (f : ℕ → M) (n : ℕ) :
    ((range n.succ).map f).prod = ((range n).map f).prod * f n := by
  rw [range_succ, map_append, map_singleton, prod_append, prod_cons, prod_nil, mul_one]

Recursive product formula for range: $\prod_{i=0}^n f(i) = \left(\prod_{i=0}^{n-1} f(i)\right) \cdot f(n)$

Informal description

For any function $f \colon \mathbb{N} \to M$ from the natural numbers to a monoid $M$ and any natural number $n$, the product of the list $[f(0), f(1), \dots, f(n)]$ is equal to the product of the list $[f(0), f(1), \dots, f(n-1)]$ multiplied by $f(n)$. In symbols: \[ \prod_{i=0}^n f(i) = \left(\prod_{i=0}^{n-1} f(i)\right) \cdot f(n) \]

List.prod_range_succ' theorem

(f : ℕ → M) (n : ℕ) : ((range n.succ).map f).prod = f 0 * ((range n).map fun i ↦ f i.succ).prod

Full source

/-- A variant of `prod_range_succ` which pulls off the first term in the product rather than the
last. -/
@[to_additive
"A variant of `sum_range_succ` which pulls off the first term in the sum rather than the last."]
lemma prod_range_succ' (f : ℕ → M) (n : ℕ) :
    ((range n.succ).map f).prod = f 0 * ((range n).map fun i ↦ f i.succ).prod := by
  rw [range_succ_eq_map]
  simp [Function.comp_def]

Product of a range with first term factored out

Informal description

For any monoid $M$, function $f \colon \mathbb{N} \to M$, and natural number $n$, the product of the list $[f(0), f(1), \dots, f(n)]$ is equal to $f(0)$ multiplied by the product of the list $[f(1), f(2), \dots, f(n)]$. In symbols: \[ \prod_{i=0}^n f(i) = f(0) \cdot \prod_{i=1}^n f(i) \]

List.prod_eq_one theorem

(hl : ∀ x ∈ l, x = 1) : l.prod = 1

Full source

@[to_additive] lemma prod_eq_one (hl : ∀ x ∈ l, x = 1) : l.prod = 1 := by
  induction l with
  | nil => rfl
  | cons i l hil =>
    rw [List.prod_cons, hil fun x hx ↦ hl _ (mem_cons_of_mem i hx),
      hl _ mem_cons_self, one_mul]

Product of List of Identities is Identity

Informal description

If every element $x$ in a list $l$ of a monoid $M$ equals the identity element $1$, then the product of all elements in $l$ is also $1$.

List.exists_mem_ne_one_of_prod_ne_one theorem

(h : l.prod ≠ 1) : ∃ x ∈ l, x ≠ (1 : M)

Full source

@[to_additive] lemma exists_mem_ne_one_of_prod_ne_one (h : l.prod ≠ 1) :
    ∃ x ∈ l, x ≠ (1 : M) := by simpa only [not_forall, exists_prop] using mt prod_eq_one h

Existence of Non-Identity Element in List with Non-Identity Product

Informal description

If the product of all elements in a list $l$ of a monoid $M$ is not equal to the identity element $1$, then there exists an element $x \in l$ such that $x \neq 1$.

List.prod_erase_of_comm theorem

[DecidableEq M] (ha : a ∈ l) (comm : ∀ x ∈ l, ∀ y ∈ l, x * y = y * x) : a * (l.erase a).prod = l.prod

Full source

@[to_additive]
lemma prod_erase_of_comm [DecidableEq M] (ha : a ∈ l) (comm : ∀ x ∈ l, ∀ y ∈ l, x * y = y * x) :
    a * (l.erase a).prod = l.prod := by
  induction l with
  | nil => simp only [not_mem_nil] at ha
  | cons b l ih =>
    obtain rfl | ⟨ne, h⟩ := List.eq_or_ne_mem_of_mem ha
    · simp only [erase_cons_head, prod_cons]
    rw [List.erase, beq_false_of_ne ne.symm, List.prod_cons, List.prod_cons, ← mul_assoc,
      comm a ha b mem_cons_self, mul_assoc,
      ih h fun x hx y hy ↦ comm _ (List.mem_cons_of_mem b hx) _ (List.mem_cons_of_mem b hy)]

Product of List with Erased Element under Commutativity: $a \cdot \prod (l \setminus \{a\}) = \prod l$

Informal description

Let $M$ be a monoid with a decidable equality, and let $l$ be a list of elements in $M$. For any element $a \in l$, if the elements of $l$ pairwise commute (i.e., $x * y = y * x$ for all $x, y \in l$), then the product of $l$ is equal to $a$ multiplied by the product of the list obtained by removing $a$ from $l$.

List.prod_map_eq_pow_single theorem

 [DecidableEq α] {l : List α} (a : α) (f : α → M) (hf : ∀ a', a' ≠ a → a' ∈ l → f a' = 1) :
  (l.map f).prod = f a ^ l.count a

Full source

@[to_additive]
lemma prod_map_eq_pow_single [DecidableEq α] {l : List α} (a : α) (f : α → M)
    (hf : ∀ a', a' ≠ a → a' ∈ l → f a' = 1) : (l.map f).prod = f a ^ l.count a := by
  induction l generalizing a with
  | nil => rw [map_nil, prod_nil, count_nil, _root_.pow_zero]
  | cons a' as h =>
    specialize h a fun a' ha' hfa' => hf a' ha' (mem_cons_of_mem _ hfa')
    rw [List.map_cons, List.prod_cons, count_cons, h]
    simp only [beq_iff_eq]
    split_ifs with ha'
    · rw [ha', _root_.pow_succ']
    · rw [hf a' ha' mem_cons_self, one_mul, add_zero]

Product of Mapped List Equals Power of Single Element

Informal description

Let $\alpha$ be a type with decidable equality, $M$ a monoid, $l$ a list of elements of $\alpha$, $a \in \alpha$, and $f \colon \alpha \to M$ a function such that for all $a' \in \alpha$, if $a' \neq a$ and $a' \in l$, then $f(a') = 1$. Then the product of the list obtained by applying $f$ to each element of $l$ is equal to $f(a)$ raised to the power of the number of occurrences of $a$ in $l$, i.e., \[ \prod_{x \in l} f(x) = f(a)^{\text{count}(a, l)}. \]

List.prod_eq_pow_single theorem

[DecidableEq M] (a : M) (h : ∀ a', a' ≠ a → a' ∈ l → a' = 1) : l.prod = a ^ l.count a

Full source

@[to_additive]
lemma prod_eq_pow_single [DecidableEq M] (a : M) (h : ∀ a', a' ≠ a → a' ∈ l → a' = 1) :
    l.prod = a ^ l.count a :=
  _root_.trans (by rw [map_id]) (prod_map_eq_pow_single a id h)

Product of List Equals Power of Single Non-Identity Element

Informal description

Let $M$ be a monoid with decidable equality and $l$ a list of elements in $M$. For a given element $a \in M$, if every element $a' \in l$ with $a' \neq a$ equals the identity element $1$, then the product of the list $l$ is equal to $a$ raised to the power of the number of occurrences of $a$ in $l$, i.e., \[ \prod_{x \in l} x = a^{\text{count}(a, l)}. \]

List.prod_erase theorem

[DecidableEq M] (ha : a ∈ l) : a * (l.erase a).prod = l.prod

Full source

@[to_additive (attr := simp)]
lemma prod_erase [DecidableEq M] (ha : a ∈ l) : a * (l.erase a).prod = l.prod :=
  prod_erase_of_comm ha fun x _ y _ ↦ mul_comm x y

Product of List Equals Element Times Product of List Without That Element

Informal description

Let $M$ be a monoid with decidable equality and $l$ a list of elements in $M$. For any element $a \in l$, the product of $l$ is equal to $a$ multiplied by the product of the list obtained by removing the first occurrence of $a$ from $l$, i.e., \[ a \cdot \left(\prod_{x \in l \setminus \{a\}} x\right) = \prod_{x \in l} x. \]

List.prod_map_erase theorem

[DecidableEq α] (f : α → M) {a} : ∀ {l : List α}, a ∈ l → f a * ((l.erase a).map f).prod = (l.map f).prod

Full source

@[to_additive (attr := simp)]
lemma prod_map_erase [DecidableEq α] (f : α → M) {a} :
    ∀ {l : List α}, a ∈ l → f a * ((l.erase a).map f).prod = (l.map f).prod
  | b :: l, h => by
    obtain rfl | ⟨ne, h⟩ := List.eq_or_ne_mem_of_mem h
    · simp only [map, erase_cons_head, prod_cons]
    · simp only [map, erase_cons_tail (not_beq_of_ne ne.symm), prod_cons, prod_map_erase _ h,
        mul_left_comm (f a) (f b)]

Product Preservation under Element Removal and Mapping in Commutative Monoids

Informal description

Let $\alpha$ be a type with decidable equality and $M$ a commutative monoid. For any function $f : \alpha \to M$, element $a \in \alpha$, and list $l$ of elements in $\alpha$ containing $a$, we have: \[ f(a) \cdot \left(\prod_{x \in l \setminus \{a\}} f(x)\right) = \prod_{x \in l} f(x) \] where $l \setminus \{a\}$ denotes the list obtained by removing the first occurrence of $a$ from $l$.

List.Perm.prod_eq theorem

(h : Perm l₁ l₂) : prod l₁ = prod l₂

Full source

@[to_additive] lemma Perm.prod_eq (h : Perm l₁ l₂) : prod l₁ = prod l₂ := h.foldr_op_eq

Product Invariance under Permutation in Commutative Monoids

Informal description

For any two lists $l_1$ and $l_2$ of elements in a commutative monoid $M$, if $l_1$ is a permutation of $l_2$ (denoted $l_1 \sim l_2$), then the product of the elements in $l_1$ is equal to the product of the elements in $l_2$, i.e., \[ \prod_{x \in l_1} x = \prod_{x \in l_2} x. \]

List.prod_reverse theorem

(l : List M) : prod l.reverse = prod l

Full source

@[to_additive (attr := simp)]
lemma prod_reverse (l : List M) : prod l.reverse = prod l := (reverse_perm l).prod_eq

Product Invariance under List Reversal in Commutative Monoids

Informal description

For any list $l$ of elements in a commutative monoid $M$, the product of the elements in the reversed list equals the product of the elements in the original list, i.e., \[ \prod_{x \in \text{reverse}(l)} x = \prod_{x \in l} x. \]

List.prod_mul_prod_eq_prod_zipWith_mul_prod_drop theorem

 : ∀ l l' : List M, l.prod * l'.prod = (zipWith (· * ·) l l').prod * (l.drop l'.length).prod * (l'.drop l.length).prod

Full source

@[to_additive]
lemma prod_mul_prod_eq_prod_zipWith_mul_prod_drop :
    ∀ l l' : List M,
      l.prod * l'.prod =
        (zipWith (· * ·) l l').prod * (l.drop l'.length).prod * (l'.drop l.length).prod
  | [], ys => by simp [Nat.zero_le]
  | xs, [] => by simp [Nat.zero_le]
  | x :: xs, y :: ys => by
    simp only [drop, length, zipWith_cons_cons, prod_cons]
    conv =>
      lhs; rw [mul_assoc]; right; rw [mul_comm, mul_assoc]; right
      rw [mul_comm, prod_mul_prod_eq_prod_zipWith_mul_prod_drop xs ys]
    simp [mul_assoc]

Product Decomposition via ZipWith and Drop in Commutative Monoids

Informal description

For any two lists $l$ and $l'$ of elements in a commutative monoid $M$, the product of $l$ multiplied by the product of $l'$ is equal to the product of the list obtained by component-wise multiplication of $l$ and $l'$ (via `zipWith`), multiplied by the product of the remaining elements in $l$ after dropping the first $|l'|$ elements, and multiplied by the product of the remaining elements in $l'$ after dropping the first $|l|$ elements. In symbols: \[ \prod_{x \in l} x \cdot \prod_{y \in l'} y = \left( \prod_{i} (l_i \cdot l'_i) \right) \cdot \left( \prod_{x \in \text{drop } |l'| \ l} x \right) \cdot \left( \prod_{y \in \text{drop } |l| \ l'} y \right) \]

List.prod_mul_prod_eq_prod_zipWith_of_length_eq theorem

(l l' : List M) (h : l.length = l'.length) : l.prod * l'.prod = (zipWith (· * ·) l l').prod

Full source

@[to_additive]
lemma prod_mul_prod_eq_prod_zipWith_of_length_eq (l l' : List M) (h : l.length = l'.length) :
    l.prod * l'.prod = (zipWith (· * ·) l l').prod := by
  apply (prod_mul_prod_eq_prod_zipWith_mul_prod_drop l l').trans
  rw [← h, drop_length, h, drop_length, prod_nil, mul_one, mul_one]

Product Equality for ZipWith of Equal-Length Lists in Commutative Monoid

Informal description

For any two lists $l$ and $l'$ of elements in a commutative monoid $M$ with equal lengths, the product of $l$ multiplied by the product of $l'$ is equal to the product of the list obtained by component-wise multiplication of $l$ and $l'$ (via `zipWith`). In symbols: \[ \prod_{x \in l} x \cdot \prod_{y \in l'} y = \prod_{i} (l_i \cdot l'_i) \]

List.prod_map_ite theorem

 (p : α → Prop) [DecidablePred p] (f g : α → M) (l : List α) :
  (l.map fun a => if p a then f a else g a).prod = ((l.filter p).map f).prod * ((l.filter fun a ↦ ¬p a).map g).prod

Full source

@[to_additive]
lemma prod_map_ite (p : α → Prop) [DecidablePred p] (f g : α → M) (l : List α) :
    (l.map fun a => if p a then f a else g a).prod =
      ((l.filter p).map f).prod * ((l.filter fun a ↦ ¬p a).map g).prod := by
  induction l with
  | nil => simp
  | cons x xs ih =>
    simp only [map_cons, filter_cons, prod_cons, nodup_cons, ne_eq, mem_cons, count_cons] at ih ⊢
    rw [ih]
    clear ih
    by_cases hx : p x
    · simp only [hx, ↓reduceIte, decide_not, decide_true, map_cons, prod_cons, not_true_eq_false,
        decide_false, Bool.false_eq_true, mul_assoc]
    · simp only [hx, ↓reduceIte, decide_not, decide_false, Bool.false_eq_true, not_false_eq_true,
      decide_true, map_cons, prod_cons, mul_left_comm]

Product of Conditional Map Equals Product of Filtered Maps in Commutative Monoid

Informal description

Let $M$ be a commutative monoid, $p$ be a predicate on a type $\alpha$, and $f, g$ be functions from $\alpha$ to $M$. For any list $l$ of elements of $\alpha$, the product of the list obtained by mapping each element $a \in l$ to $f(a)$ if $p(a)$ holds and to $g(a)$ otherwise is equal to the product of the list obtained by mapping $f$ over the elements of $l$ satisfying $p$ multiplied by the product of the list obtained by mapping $g$ over the elements of $l$ not satisfying $p$. In symbols: \[ \prod_{a \in l} \text{if } p(a) \text{ then } f(a) \text{ else } g(a) = \left( \prod_{a \in l, p(a)} f(a) \right) \cdot \left( \prod_{a \in l, \neg p(a)} g(a) \right) \]

List.prod_map_filter_mul_prod_map_filter_not theorem

 (p : α → Prop) [DecidablePred p] (f : α → M) (l : List α) :
  ((l.filter p).map f).prod * ((l.filter fun x => ¬p x).map f).prod = (l.map f).prod

Full source

@[to_additive]
lemma prod_map_filter_mul_prod_map_filter_not (p : α → Prop) [DecidablePred p] (f : α → M)
    (l : List α) :
    ((l.filter p).map f).prod * ((l.filter fun x => ¬p x).map f).prod = (l.map f).prod := by
  rw [← prod_map_ite]
  simp only [ite_self]

Product of Filtered Lists Equals Product of Original List in Commutative Monoid

Informal description

Let $M$ be a commutative monoid, $p$ be a predicate on a type $\alpha$, and $f$ be a function from $\alpha$ to $M$. For any list $l$ of elements of $\alpha$, the product of the images of $f$ over the elements of $l$ satisfying $p$ multiplied by the product of the images of $f$ over the elements of $l$ not satisfying $p$ equals the product of the images of $f$ over all elements of $l$. In symbols: \[ \left( \prod_{a \in l, p(a)} f(a) \right) \cdot \left( \prod_{a \in l, \neg p(a)} f(a) \right) = \prod_{a \in l} f(a) \]

List.prod_inv_reverse theorem

: ∀ L : List G, L.prod⁻¹ = (L.map fun x => x⁻¹).reverse.prod

Full source

/-- This is the `List.prod` version of `mul_inv_rev` -/
@[to_additive "This is the `List.sum` version of `add_neg_rev`"]
theorem prod_inv_reverse : ∀ L : List G, L.prod⁻¹ = (L.map fun x => x⁻¹).reverse.prod
  | [] => by simp
  | x :: xs => by simp [prod_inv_reverse xs]

Inverse of Product Equals Reverse Product of Inverses for Lists

Informal description

For any list $L$ of elements in a group $G$, the inverse of the product of $L$ is equal to the product of the inverses of the elements of $L$ taken in reverse order, i.e., $$(L.\text{prod})^{-1} = \left(\text{map } (\lambda x, x^{-1}) \, L\right).\text{reverse}.\text{prod}.$$

List.prod_reverse_noncomm theorem

: ∀ L : List G, L.reverse.prod = (L.map fun x => x⁻¹).prod⁻¹

Full source

/-- A non-commutative variant of `List.prod_reverse` -/
@[to_additive "A non-commutative variant of `List.sum_reverse`"]
theorem prod_reverse_noncomm : ∀ L : List G, L.reverse.prod = (L.map fun x => x⁻¹).prod⁻¹ := by
  simp [prod_inv_reverse]

Product of Reversed List Equals Inverse of Product of Inverses in Group

Informal description

For any list $L$ of elements in a group $G$, the product of the reversed list equals the inverse of the product of the inverses of the elements of $L$, i.e., $$L.\text{reverse}.\text{prod} = \left(\text{map } (\lambda x, x^{-1}) \, L\right).\text{prod}^{-1}.$$

List.prod_drop_succ theorem

: ∀ (L : List G) (i : ℕ) (p : i < L.length), (L.drop (i + 1)).prod = L[i]⁻¹ * (L.drop i).prod

Full source

/-- Counterpart to `List.prod_take_succ` when we have an inverse operation -/
@[to_additive (attr := simp)
  "Counterpart to `List.sum_take_succ` when we have a negation operation"]
theorem prod_drop_succ :
    ∀ (L : List G) (i : ℕ) (p : i < L.length), (L.drop (i + 1)).prod = L[i]L[i]⁻¹ * (L.drop i).prod
  | [], _, p => False.elim (Nat.not_lt_zero _ p)
  | _ :: _, 0, _ => by simp
  | _ :: xs, i + 1, p => prod_drop_succ xs i (Nat.lt_of_succ_lt_succ p)

Product of Dropped List via Inverse Multiplication

Informal description

For any list $L$ of elements in a group $G$ and any natural number $i$ such that $i < \text{length}(L)$, the product of the list obtained by dropping the first $i+1$ elements of $L$ is equal to the inverse of the $i$-th element of $L$ multiplied by the product of the list obtained by dropping the first $i$ elements of $L$. That is, $$(L \text{ drop } (i+1)).\text{prod} = L[i]^{-1} \cdot (L \text{ drop } i).\text{prod}.$$

List.prod_range_div' theorem

(n : ℕ) (f : ℕ → G) : ((range n).map fun k ↦ f k / f (k + 1)).prod = f 0 / f n

Full source

/-- Cancellation of a telescoping product. -/
@[to_additive "Cancellation of a telescoping sum."]
theorem prod_range_div' (n : ℕ) (f : ℕ → G) :
    ((range n).map fun k ↦ f k / f (k + 1)).prod = f 0 / f n := by
  induction n with
  | zero => exact (div_self' (f 0)).symm
  | succ n h =>
    rw [range_succ, map_append, map_singleton, prod_append, prod_singleton, h, div_mul_div_cancel]

Telescoping Product Identity: $\prod_{k=0}^{n-1} \frac{f(k)}{f(k+1)} = \frac{f(0)}{f(n)}$

Informal description

For any natural number $n$ and any function $f \colon \mathbb{N} \to G$ where $G$ is a group, the product of the list formed by mapping each $k$ in the range $[0, n-1]$ to the ratio $f(k) / f(k+1)$ equals $f(0) / f(n)$. That is, $$\prod_{k=0}^{n-1} \frac{f(k)}{f(k+1)} = \frac{f(0)}{f(n)}.$$

List.prod_inv theorem

: ∀ L : List G, L.prod⁻¹ = (L.map fun x => x⁻¹).prod

Full source

/-- This is the `List.prod` version of `mul_inv` -/
@[to_additive "This is the `List.sum` version of `add_neg`"]
theorem prod_inv : ∀ L : List G, L.prod⁻¹ = (L.map fun x => x⁻¹).prod
  | [] => by simp
  | x :: xs => by simp [mul_comm, prod_inv xs]

Inverse of Product Equals Product of Inverses in Commutative Group

Informal description

For any list $L$ of elements in a commutative group $G$, the inverse of the product of the elements in $L$ is equal to the product of the inverses of the elements in $L$. That is, $$(L.\text{prod})^{-1} = \left(\text{map } (\lambda x, x^{-1}) L\right).\text{prod}$$

List.prod_range_div theorem

(n : ℕ) (f : ℕ → G) : ((range n).map fun k ↦ f (k + 1) / f k).prod = f n / f 0

Full source

/-- Cancellation of a telescoping product. -/
@[to_additive "Cancellation of a telescoping sum."]
theorem prod_range_div (n : ℕ) (f : ℕ → G) :
    ((range n).map fun k ↦ f (k + 1) / f k).prod = f n / f 0 := by
  have h : ((·⁻¹) ∘ fun k ↦ f (k + 1) / f k) = fun k ↦ f k / f (k + 1) := by ext; apply inv_div
  rw [← inv_inj, prod_inv, map_map, inv_div, h, prod_range_div']

Telescoping Product Identity: $\prod_{k=0}^{n-1} \frac{f(k+1)}{f(k)} = \frac{f(n)}{f(0)}$

Informal description

For any natural number $n$ and any function $f \colon \mathbb{N} \to G$ where $G$ is a group, the product of the list formed by mapping each $k$ in the range $[0, n-1]$ to the ratio $f(k+1) / f(k)$ equals $f(n) / f(0)$. That is, $$\prod_{k=0}^{n-1} \frac{f(k+1)}{f(k)} = \frac{f(n)}{f(0)}.$$

List.prod_set' theorem

(L : List G) (n : ℕ) (a : G) : (L.set n a).prod = L.prod * if hn : n < L.length then L[n]⁻¹ * a else 1

Full source

/-- Alternative version of `List.prod_set` when the list is over a group -/
@[to_additive "Alternative version of `List.sum_set` when the list is over a group"]
theorem prod_set' (L : List G) (n : ℕ) (a : G) :
    (L.set n a).prod = L.prod * if hn : n < L.length then L[n]⁻¹ * a else 1 := by
  refine (prod_set L n a).trans ?_
  split_ifs with hn
  · rw [mul_comm _ a, mul_assoc a, prod_drop_succ L n hn, mul_comm _ (drop n L).prod, ←
      mul_assoc (take n L).prod, prod_take_mul_prod_drop, mul_comm a, mul_assoc]
  · simp only [take_of_length_le (le_of_not_lt hn), prod_nil, mul_one,
      drop_eq_nil_of_le ((le_of_not_lt hn).trans n.le_succ)]

Product of List with Modified Element in Commutative Group: $\text{prod}(L.\text{set}(n, a)) = \text{prod}(L) \cdot (L[n]^{-1} \cdot a \text{ if } n < \text{length}(L) \text{ else } 1)$

Informal description

Let $G$ be a commutative group and $L$ a list of elements in $G$. For any natural number $n$ and element $a \in G$, the product of the list obtained by setting the $n$-th element of $L$ to $a$ is equal to the product of $L$ multiplied by $L[n]^{-1} \cdot a$ if $n$ is a valid index in $L$, and by $1$ otherwise. That is, \[ \text{prod}(L.\text{set}(n, a)) = \text{prod}(L) \cdot \begin{cases} L[n]^{-1} \cdot a & \text{if } n < \text{length}(L) \\ 1 & \text{otherwise}. \end{cases} \]

List.prod_map_ite_eq theorem

 {A : Type*} [DecidableEq A] (l : List A) (f g : A → G) (a : A) :
  (l.map fun x => if x = a then f x else g x).prod = (f a / g a) ^ (l.count a) * (l.map g).prod

Full source

@[to_additive]
lemma prod_map_ite_eq {A : Type*} [DecidableEq A] (l : List A) (f g : A → G) (a : A) :
    (l.map fun x => if x = a then f x else g x).prod
      = (f a / g a) ^ (l.count a) * (l.map g).prod := by
  induction l with
  | nil => simp
  | cons x xs ih =>
    simp only [map_cons, prod_cons, nodup_cons, ne_eq, mem_cons, count_cons] at ih ⊢
    rw [ih]
    clear ih
    by_cases hx : x = a
    · simp only [hx, ite_true, div_pow, pow_add, pow_one, div_eq_mul_inv, mul_assoc, mul_comm,
        mul_left_comm, mul_inv_cancel_left, beq_self_eq_true]
    · simp only [hx, ite_false, ne_comm.mp hx, add_zero, mul_assoc, mul_comm (g x) _, beq_iff_eq]

Product of Conditional Map: $\prod_{x \in l} (\text{if } x = a \text{ then } f(x) \text{ else } g(x)) = (f(a)/g(a))^{\text{count}(a, l)} \cdot \prod_{x \in l} g(x)$

Informal description

Let $A$ be a type with decidable equality, $G$ a commutative group, $l$ a list of elements of $A$, and $f, g : A \to G$ two functions. For any $a \in A$, the product of the list obtained by mapping each element $x$ of $l$ to $f(x)$ if $x = a$ and to $g(x)$ otherwise, is equal to $(f(a) / g(a))^{n} \cdot \prod_{x \in l} g(x)$, where $n$ is the number of occurrences of $a$ in $l$.

List.sum_const_nat theorem

(m n : ℕ) : sum (replicate m n) = m * n

Full source

theorem sum_const_nat (m n : ℕ) : sum (replicate m n) = m * n :=
  sum_replicate m n

Sum of Replicated Natural Numbers: $\sum (\text{replicate}\ m\ n) = m \cdot n$

Informal description

For any natural numbers $m$ and $n$, the sum of a list consisting of $m$ copies of $n$ is equal to $m$ multiplied by $n$, i.e., $\sum (\text{replicate}\ m\ n) = m \cdot n$.

List.headI_add_tail_sum theorem

(L : List ℕ) : L.headI + L.tail.sum = L.sum

Full source

/-- This relies on `default ℕ = 0`. -/
theorem headI_add_tail_sum (L : List ℕ) : L.headI + L.tail.sum = L.sum := by
  cases L <;> simp

Head-Tail Sum Decomposition for Lists of Natural Numbers

Informal description

For any list $L$ of natural numbers, the sum of the first element of $L$ (or $0$ if $L$ is empty) and the sum of the remaining elements equals the total sum of the list, i.e., $\text{head}(L) + \text{sum}(\text{tail}(L)) = \text{sum}(L)$.

List.headI_le_sum theorem

(L : List ℕ) : L.headI ≤ L.sum

Full source

/-- This relies on `default ℕ = 0`. -/
theorem headI_le_sum (L : List ℕ) : L.headI ≤ L.sum :=
  Nat.le.intro (headI_add_tail_sum L)

Head Element is Bounded by Sum in Lists of Natural Numbers

Informal description

For any list $L$ of natural numbers, the first element of $L$ (or $0$ if $L$ is empty) is less than or equal to the sum of all elements in $L$, i.e., $\text{head}(L) \leq \text{sum}(L)$.

List.tail_sum theorem

(L : List ℕ) : L.tail.sum = L.sum - L.headI

Full source

/-- This relies on `default ℕ = 0`. -/
theorem tail_sum (L : List ℕ) : L.tail.sum = L.sum - L.headI := by
  rw [← headI_add_tail_sum L, add_comm, Nat.add_sub_cancel_right]

Tail Sum Equals Total Sum Minus Head for Lists of Natural Numbers

Informal description

For any list $L$ of natural numbers, the sum of the tail of $L$ (i.e., all elements except the first) equals the total sum of $L$ minus its first element (or $0$ if $L$ is empty), i.e., $\text{sum}(\text{tail}(L)) = \text{sum}(L) - \text{head}(L)$.

List.alternatingProd_nil theorem

: alternatingProd ([] : List α) = 1

Full source

@[to_additive (attr := simp)]
theorem alternatingProd_nil : alternatingProd ([] : List α) = 1 :=
  rfl

Alternating Product of Empty List is One

Informal description

The alternating product of the empty list is equal to $1$.

List.alternatingProd_singleton theorem

(a : α) : alternatingProd [a] = a

Full source

@[to_additive (attr := simp)]
theorem alternatingProd_singleton (a : α) : alternatingProd [a] = a :=
  rfl

Alternating Product of Singleton List

Informal description

For any element $a$ of type $\alpha$, the alternating product of the singleton list containing $a$ is equal to $a$ itself, i.e., $\text{alternatingProd}([a]) = a$.

List.alternatingProd_cons_cons' theorem

(a b : α) (l : List α) : alternatingProd (a :: b :: l) = a * b⁻¹ * alternatingProd l

Full source

@[to_additive]
theorem alternatingProd_cons_cons' (a b : α) (l : List α) :
    alternatingProd (a :: b :: l) = a * b⁻¹ * alternatingProd l :=
  rfl

Alternating product of a list with two initial elements: $a \cdot b^{-1} \cdot \text{alternatingProd}(l)$

Informal description

For any elements $a, b$ in a type $\alpha$ with a division and inverse structure, and for any list $l$ of elements in $\alpha$, the alternating product of the list $a :: b :: l$ is equal to $a \cdot b^{-1} \cdot \text{alternatingProd}(l)$.

List.alternatingProd_cons_cons theorem

[DivInvMonoid α] (a b : α) (l : List α) : alternatingProd (a :: b :: l) = a / b * alternatingProd l

Full source

@[to_additive]
theorem alternatingProd_cons_cons [DivInvMonoid α] (a b : α) (l : List α) :
    alternatingProd (a :: b :: l) = a / b * alternatingProd l := by
  rw [div_eq_mul_inv, alternatingProd_cons_cons']

Alternating Product of List with Two Initial Elements: $(a / b) \cdot \text{alternatingProd}(l)$

Informal description

Let $\alpha$ be a division-inversion monoid. For any elements $a, b \in \alpha$ and any list $l$ of elements in $\alpha$, the alternating product of the list $a :: b :: l$ satisfies $\text{alternatingProd}(a :: b :: l) = (a / b) \cdot \text{alternatingProd}(l)$.

List.alternatingProd_cons' theorem

: ∀ (a : α) (l : List α), alternatingProd (a :: l) = a * (alternatingProd l)⁻¹

Full source

@[to_additive]
theorem alternatingProd_cons' :
    ∀ (a : α) (l : List α), alternatingProd (a :: l) = a * (alternatingProd l)⁻¹
  | a, [] => by rw [alternatingProd_nil, inv_one, mul_one, alternatingProd_singleton]
  | a, b :: l => by
    rw [alternatingProd_cons_cons', alternatingProd_cons' b l, mul_inv, inv_inv, mul_assoc]

Alternating Product of Cons List: $a \cdot (\text{alternatingProd}(l))^{-1}$

Informal description

For any element $a$ in a type $\alpha$ with a multiplicative inverse operation and any list $l$ of elements in $\alpha$, the alternating product of the list $a :: l$ is equal to $a$ multiplied by the inverse of the alternating product of $l$, i.e., $$\text{alternatingProd}(a :: l) = a \cdot (\text{alternatingProd}(l))^{-1}.$$

List.alternatingProd_cons theorem

(a : α) (l : List α) : alternatingProd (a :: l) = a / alternatingProd l

Full source

@[to_additive (attr := simp)]
theorem alternatingProd_cons (a : α) (l : List α) :
    alternatingProd (a :: l) = a / alternatingProd l := by
  rw [div_eq_mul_inv, alternatingProd_cons']

Alternating Product of Cons List: $a / \text{alternatingProd}(l)$

Informal description

For any element $a$ in a type $\alpha$ with a division operation and any list $l$ of elements in $\alpha$, the alternating product of the list $a :: l$ is equal to $a$ divided by the alternating product of $l$, i.e., $$\text{alternatingProd}(a :: l) = \frac{a}{\text{alternatingProd}(l)}.$$

List.sum_nat_mod theorem

(l : List ℕ) (n : ℕ) : l.sum % n = (l.map (· % n)).sum % n

Full source

lemma sum_nat_mod (l : List ℕ) (n : ℕ) : l.sum % n = (l.map (· % n)).sum % n := by
  induction l with
  | nil => simp only [Nat.zero_mod, map_nil]
  | cons a l ih =>
    simpa only [map_cons, sum_cons, Nat.mod_add_mod, Nat.add_mod_mod] using congr((a + $ih) % n)

Modular Arithmetic Property for List Sum of Natural Numbers

Informal description

For any list $l$ of natural numbers and any natural number $n$, the sum of the elements of $l$ modulo $n$ is equal to the sum of the elements of $l$ where each element is taken modulo $n$, all modulo $n$. In symbols: $$\left(\sum_{x \in l} x\right) \bmod n = \left(\sum_{x \in l} (x \bmod n)\right) \bmod n$$

List.prod_nat_mod theorem

(l : List ℕ) (n : ℕ) : l.prod % n = (l.map (· % n)).prod % n

Full source

lemma prod_nat_mod (l : List ℕ) (n : ℕ) : l.prod % n = (l.map (· % n)).prod % n := by
  induction l with
  | nil => simp only [Nat.zero_mod, map_nil]
  | cons a l ih =>
    simpa only [prod_cons, map_cons, Nat.mod_mul_mod, Nat.mul_mod_mod] using congr((a * $ih) % n)

Modular Arithmetic Property for List Product of Natural Numbers

Informal description

For any list $l$ of natural numbers and any natural number $n$, the product of the elements of $l$ modulo $n$ is equal to the product of the elements of $l$ where each element is taken modulo $n$, all modulo $n$. In symbols: $$(\prod_{x \in l} x) \bmod n = \left(\prod_{x \in l} (x \bmod n)\right) \bmod n$$

List.sum_int_mod theorem

(l : List ℤ) (n : ℤ) : l.sum % n = (l.map (· % n)).sum % n

Full source

lemma sum_int_mod (l : List ℤ) (n : ℤ) : l.sum % n = (l.map (· % n)).sum % n := by
  induction l <;> simp [Int.add_emod, *]

Modular Arithmetic Property for List Sum of Integers

Informal description

For any list $l$ of integers and any integer $n$, the sum of the elements of $l$ modulo $n$ is equal to the sum of the elements of $l$ where each element is taken modulo $n$, all modulo $n$. In symbols: $$\left(\sum_{x \in l} x\right) \bmod n = \left(\sum_{x \in l} (x \bmod n)\right) \bmod n$$

List.prod_int_mod theorem

(l : List ℤ) (n : ℤ) : l.prod % n = (l.map (· % n)).prod % n

Full source

lemma prod_int_mod (l : List ℤ) (n : ℤ) : l.prod % n = (l.map (· % n)).prod % n := by
  induction l <;> simp [Int.mul_emod, *]

Modular Arithmetic Property for List Product of Integers

Informal description

For any list $l$ of integers and any integer $n$, the product of the elements of $l$ modulo $n$ is equal to the product of the elements of $l$ where each element is taken modulo $n$, all modulo $n$. In symbols: $$\left(\prod_{x \in l} x\right) \bmod n = \left(\prod_{x \in l} (x \bmod n)\right) \bmod n$$

map_list_prod theorem

{F : Type*} [FunLike F M N] [MonoidHomClass F M N] (f : F) (l : List M) : f l.prod = (l.map f).prod

Full source

@[to_additive]
theorem map_list_prod {F : Type*} [FunLike F M N] [MonoidHomClass F M N] (f : F) (l : List M) :
    f l.prod = (l.map f).prod :=
  (l.prod_hom f).symm

Homomorphism Property for List Products: $f(\prod x) = \prod f(x)$

Informal description

Let $M$ and $N$ be monoids, and let $f \colon M \to N$ be a monoid homomorphism. For any list $l$ of elements of $M$, the image under $f$ of the product of $l$ is equal to the product of the list obtained by applying $f$ to each element of $l$. That is, \[ f\left(\prod_{x \in l} x\right) = \prod_{x \in l} f(x). \]

MonoidHom.map_list_prod theorem

(f : M →* N) (l : List M) : f l.prod = (l.map f).prod

Full source

@[to_additive]
protected theorem map_list_prod (f : M →* N) (l : List M) : f l.prod = (l.map f).prod :=
  map_list_prod f l

Homomorphism Property for List Products: $f(\prod x) = \prod f(x)$

Informal description

Let $M$ and $N$ be monoids, and let $f \colon M \to N$ be a monoid homomorphism. For any list $l$ of elements of $M$, the image under $f$ of the product of the elements in $l$ is equal to the product of the list obtained by applying $f$ to each element of $l$. That is, \[ f\left(\prod_{x \in l} x\right) = \prod_{x \in l} f(x). \]

List.take_sum_flatten theorem

(L : List (List α)) (i : ℕ) : L.flatten.take ((L.map length).take i).sum = (L.take i).flatten

Full source

/-- In a flatten, taking the first elements up to an index which is the sum of the lengths of the
first `i` sublists, is the same as taking the flatten of the first `i` sublists. -/
lemma take_sum_flatten (L : List (List α)) (i : ℕ) :
    L.flatten.take ((L.map length).take i).sum = (L.take i).flatten := by
  induction L generalizing i
  · simp
  · cases i <;> simp [take_append, *]

Take-Sum-Flatten Equality for Lists of Lists

Informal description

For any list of lists $L$ and any natural number $i$, taking the first $k$ elements from the flattened list $L$, where $k$ is the sum of the lengths of the first $i$ sublists in $L$, is equal to the flattened list of the first $i$ sublists of $L$. In other words: \[ \text{take}\left(\sum_{j < i} \text{length}(L_j), \text{flatten}(L)\right) = \text{flatten}(\text{take}(i, L)) \] where $L_j$ denotes the $j$-th sublist of $L$.

List.drop_sum_flatten theorem

(L : List (List α)) (i : ℕ) : L.flatten.drop ((L.map length).take i).sum = (L.drop i).flatten

Full source

/-- In a flatten, dropping all the elements up to an index which is the sum of the lengths of the
first `i` sublists, is the same as taking the join after dropping the first `i` sublists. -/
lemma drop_sum_flatten (L : List (List α)) (i : ℕ) :
    L.flatten.drop ((L.map length).take i).sum = (L.drop i).flatten := by
  induction L generalizing i
  · simp
  · cases i <;> simp [take_append, *]

Drop-Sum-Flatten Equality for Lists of Lists

Informal description

For any list of lists $L$ and any natural number $i$, dropping the first $k$ elements from the flattened list $L$, where $k$ is the sum of the lengths of the first $i$ sublists in $L$, is equal to the flattened list obtained by dropping the first $i$ sublists of $L$. In other words: \[ \text{drop}\left(\sum_{j < i} \text{length}(L_j), \text{flatten}(L)\right) = \text{flatten}(\text{drop}(i, L)) \] where $L_j$ denotes the $j$-th sublist of $L$.

List.length_le_sum_of_one_le theorem

(L : List ℕ) (h : ∀ i ∈ L, 1 ≤ i) : L.length ≤ L.sum

Full source

/-- If all elements in a list are bounded below by `1`, then the length of the list is bounded
by the sum of the elements. -/
theorem length_le_sum_of_one_le (L : List ℕ) (h : ∀ i ∈ L, 1 ≤ i) : L.length ≤ L.sum := by
  induction L with
  | nil => simp
  | cons j L IH =>
    rw [sum_cons, length, add_comm]
    exact Nat.add_le_add (h _ mem_cons_self) (IH fun i hi => h i (mem_cons.2 (Or.inr hi)))

Length Bounded by Sum for Lists of Natural Numbers Bounded Below by One

Informal description

For any list $L$ of natural numbers, if every element $i$ in $L$ satisfies $1 \leq i$, then the length of $L$ is less than or equal to the sum of its elements, i.e., $\text{length}(L) \leq \sum_{i \in L} i$.