Mathlib.Algebra.BigOperators.Group.List.Defs

List.prod definition

{α} [Mul α] [One α] : List α → α

Full source

/-- Product of a list.

`List.prod [a, b, c] = a * (b * (c * 1))` -/
@[to_additive existing]
def prod {α} [Mul α] [One α] : List α → α :=
  foldr (· * ·) 1

Product of a list of elements in a multiplicative monoid

Informal description

Given a type $\alpha$ equipped with a multiplication operation and a multiplicative identity, the function `List.prod` takes a list of elements in $\alpha$ and returns their product, computed by multiplying the elements from right to left with the identity element as the initial value. Specifically, for a list $[a_1, a_2, \dots, a_n]$, the product is $a_1 \cdot (a_2 \cdot (\dots \cdot (a_n \cdot 1) \dots))$.

List.alternatingSum definition

{G : Type*} [Zero G] [Add G] [Neg G] : List G → G

Full source

/-- The alternating sum of a list. -/
def alternatingSum {G : Type*} [Zero G] [Add G] [Neg G] : List G → G
  | [] => 0
  | g :: [] => g
  | g :: h :: t => g + -h + alternatingSum t

Alternating sum of a list

Informal description

The alternating sum of a list $[g_1, g_2, g_3, \ldots]$ is defined recursively as: - $0$ for the empty list, - $g_1$ for a single-element list $[g_1]$, - $g_1 - g_2 + g_3 - g_4 + \cdots$ for longer lists, where the signs alternate between addition and subtraction.

List.alternatingProd definition

{G : Type*} [One G] [Mul G] [Inv G] : List G → G

Full source

/-- The alternating product of a list. -/
@[to_additive existing]
def alternatingProd {G : Type*} [One G] [Mul G] [Inv G] : List G → G
  | [] => 1
  | g :: [] => g
  | g :: h :: t => g * h⁻¹ * alternatingProd t

Alternating product of a list

Informal description

The alternating product of a list is defined recursively as follows: - The alternating product of the empty list is $1$. - The alternating product of a single-element list $[g]$ is $g$. - For a list with at least two elements $g :: h :: t$, the alternating product is $g \cdot h^{-1} \cdot \text{alternatingProd}(t)$.

List.prod_nil theorem

: ([] : List M).prod = 1

Full source

@[to_additive existing, simp]
theorem prod_nil : ([] : List M).prod = 1 :=
  rfl

Product of Empty List is One

Informal description

The product of an empty list of elements in a multiplicative monoid is equal to the multiplicative identity $1$.

List.prod_cons theorem

{a} {l : List M} : (a :: l).prod = a * l.prod

Full source

@[to_additive existing, simp]
theorem prod_cons {a} {l : List M} : (a :: l).prod = a * l.prod := rfl

Product of Cons List Equals Head Times Tail Product

Informal description

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

List.prod_induction theorem

(p : M → Prop) (hom : ∀ a b, p a → p b → p (a * b)) (unit : p 1) (base : ∀ x ∈ l, p x) : p l.prod

Full source

@[to_additive]
lemma prod_induction
    (p : M → Prop) (hom : ∀ a b, p a → p b → p (a * b)) (unit : p 1) (base : ∀ x ∈ l, p x) :
    p l.prod := by
  induction l with
  | nil => simpa
  | cons a l ih =>
    rw [List.prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at base
    exact hom _ _ (base.1) (ih base.2)

Induction Principle for List Products in a Multiplicative Monoid

Informal description

Let $M$ be a multiplicative monoid and $l$ be a list of elements in $M$. For any predicate $p$ on $M$, if $p$ is multiplicative (i.e., $p(a)$ and $p(b)$ imply $p(a \cdot b)$ for all $a, b \in M$), $p$ holds for the identity element $1$, and $p$ holds for every element in $l$, then $p$ holds for the product of the list $l$.

List.prod_singleton theorem

: [a].prod = a

Full source

@[to_additive]
theorem prod_singleton : [a].prod = a :=
  mul_one a

Product of Singleton List Equals Its Element

Informal description

For any element $a$ in a multiplicative monoid $M$, the product of the singleton list $[a]$ is equal to $a$, i.e., $\text{prod}([a]) = a$.

List.prod_one_cons theorem

: (1 :: l).prod = l.prod

Full source

@[to_additive]
theorem prod_one_cons : (1 :: l).prod = l.prod := by
  rw [prod, foldr, one_mul]

Product of List with Prepended Identity Equals Product of Original List

Informal description

For any list $l$ of elements in a multiplicative monoid $M$, the product of the list obtained by prepending the multiplicative identity $1$ to $l$ is equal to the product of $l$, i.e., $\text{prod}(1 :: l) = \text{prod}(l)$.

List.prod_map_one theorem

{l : List ι} : (l.map fun _ => (1 : M)).prod = 1

Full source

@[to_additive]
theorem prod_map_one {l : List ι} :
    (l.map fun _ => (1 : M)).prod = 1 := by
  induction l with
  | nil => rfl
  | cons hd tl ih => rw [map_cons, prod_one_cons, ih]

Product of List Mapped to Identity is Identity

Informal description

For any list $l$ of elements of type $\iota$, the product of the list obtained by mapping each element of $l$ to the multiplicative identity $1$ in a monoid $M$ is equal to $1$, i.e., $\prod (\text{map} (\lambda \_. 1) l) = 1$.

List.prod_eq_foldr theorem

{l : List M} : l.prod = foldr (· * ·) 1 l

Full source

@[to_additive]
theorem prod_eq_foldr {l : List M} : l.prod = foldr (· * ·) 1 l := rfl

Product of List Equals Right 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 right-fold of the list using the multiplication operation with the identity element $1$ as the initial value, i.e., $\prod l = \text{foldr} (\cdot) 1 l$.

List.prod_replicate theorem

(n : ℕ) (a : M) : (replicate n a).prod = a ^ n

Full source

@[to_additive (attr := simp)]
theorem prod_replicate (n : ℕ) (a : M) : (replicate n a).prod = a ^ n := by
  induction n with
  | zero => rw [pow_zero, replicate_zero, prod_nil]
  | succ n ih => rw [replicate_succ, prod_cons, ih, pow_succ']

Product of Replicated List Equals Power: $\prod (\text{replicate}\ n\ a) = a^n$

Informal description

For any natural number $n$ and any element $a$ in a monoid $M$, the product of a list consisting of $n$ copies of $a$ is equal to $a$ raised to the power of $n$, i.e., $\prod (\text{replicate}\ n\ a) = a^n$.

List.prod_eq_pow_card theorem

(l : List M) (m : M) (h : ∀ x ∈ l, x = m) : l.prod = m ^ l.length

Full source

@[to_additive sum_eq_card_nsmul]
theorem prod_eq_pow_card (l : List M) (m : M) (h : ∀ x ∈ l, x = m) : l.prod = m ^ l.length := by
  rw [← prod_replicate, ← List.eq_replicate_iff.mpr ⟨rfl, h⟩]

Product of Uniform List Equals Element to the Power of Length: $\prod l = m^{|l|}$

Informal description

For any list $l$ of elements in a monoid $M$ and any element $m \in M$, if every element $x$ in $l$ is equal to $m$, then the product of the elements in $l$ is equal to $m$ raised to the power of the length of $l$, i.e., $\prod l = m^{|l|}$.

List.prod_hom_rel theorem

 (l : List ι) {r : M → N → Prop} {f : ι → M} {g : ι → N} (h₁ : r 1 1) (h₂ : ∀ ⦃i a b⦄, r a b → r (f i * a) (g i * b)) :
  r (l.map f).prod (l.map g).prod

Full source

@[to_additive]
theorem prod_hom_rel (l : List ι) {r : M → N → Prop} {f : ι → M} {g : ι → N} (h₁ : r 1 1)
    (h₂ : ∀ ⦃i a b⦄, r a b → r (f i * a) (g i * b)) : r (l.map f).prod (l.map g).prod :=
  List.recOn l h₁ fun a l hl => by simp only [map_cons, prod_cons, h₂ hl]

Preservation of Relation Under List Product Homomorphism

Informal description

Let $M$ and $N$ be monoids, and let $r : M \to N \to \mathrm{Prop}$ be a relation between them. Given a list $l$ of elements of type $\iota$, and functions $f : \iota \to M$ and $g : \iota \to N$, if the relation $r$ holds for the identity elements ($r(1,1)$) and is preserved under multiplication (i.e., for any $i \in \iota$ and $a \in M$, $b \in N$, if $r(a,b)$ holds then $r(f(i) \cdot a, g(i) \cdot b)$ also holds), then the relation $r$ holds between the product of the list obtained by mapping $f$ over $l$ and the product of the list obtained by mapping $g$ over $l$. In symbols: \[ r(1,1) \land (\forall i\ a\ b, r(a,b) \to r(f(i) \cdot a, g(i) \cdot b)) \implies r\left(\prod (l.\mathrm{map}\ f), \prod (l.\mathrm{map}\ g)\right) \]