Mathlib.Algebra.BigOperators.Intervals

Finset.mul_prod_Ico_eq_prod_Icc theorem

(h : a ≤ b) : f b * ∏ x ∈ Ico a b, f x = ∏ x ∈ Icc a b, f x

Full source

@[to_additive]
lemma mul_prod_Ico_eq_prod_Icc (h : a ≤ b) : f b * ∏ x ∈ Ico a b, f x = ∏ x ∈ Icc a b, f x := by
  rw [Icc_eq_cons_Ico h, prod_cons]

Product over Closed Interval as Product over Closed-Open Interval: $f(b) \cdot \prod_{[a, b)} f = \prod_{[a, b]} f$

Informal description

Let $\alpha$ be a type with a locally finite order and a partial order, and let $f : \alpha \to M$ be a function to a commutative monoid $M$. For any elements $a, b \in \alpha$ with $a \leq b$, the product of $f(b)$ with the product of $f$ over the closed-open interval $[a, b)$ equals the product of $f$ over the closed interval $[a, b]$. In symbols: $$ f(b) \cdot \prod_{x \in [a, b)} f(x) = \prod_{x \in [a, b]} f(x). $$

Finset.prod_Ico_mul_eq_prod_Icc theorem

(h : a ≤ b) : (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Icc a b, f x

Full source

@[to_additive]
lemma prod_Ico_mul_eq_prod_Icc (h : a ≤ b) : (∏ x ∈ Ico a b, f x) * f b = ∏ x ∈ Icc a b, f x := by
  rw [mul_comm, mul_prod_Ico_eq_prod_Icc h]

Product identity: $\prod_{[a, b)} f \cdot f(b) = \prod_{[a, b]} f$

Informal description

Let $\alpha$ be a type with a locally finite order and a partial order, and let $f : \alpha \to M$ be a function to a commutative monoid $M$. For any elements $a, b \in \alpha$ with $a \leq b$, the product of $f$ over the closed-open interval $[a, b)$ multiplied by $f(b)$ equals the product of $f$ over the closed interval $[a, b]$. In symbols: $$ \left(\prod_{x \in [a, b)} f(x)\right) \cdot f(b) = \prod_{x \in [a, b]} f(x). $$

Finset.mul_prod_Ioc_eq_prod_Icc theorem

(h : a ≤ b) : f a * ∏ x ∈ Ioc a b, f x = ∏ x ∈ Icc a b, f x

Full source

@[to_additive]
lemma mul_prod_Ioc_eq_prod_Icc (h : a ≤ b) : f a * ∏ x ∈ Ioc a b, f x = ∏ x ∈ Icc a b, f x := by
  rw [Icc_eq_cons_Ioc h, prod_cons]

Product identity: $f(a) \cdot \prod_{x \in (a, b]} f(x) = \prod_{x \in [a, b]} f(x)$

Informal description

Let $\alpha$ be a locally finite order and $a, b \in \alpha$ with $a \leq b$. For any function $f : \alpha \to M$ where $M$ is a commutative monoid, the product of $f(a)$ with the product of $f(x)$ over all $x$ in the open-closed interval $(a, b]$ equals the product of $f(x)$ over all $x$ in the closed interval $[a, b]$. In symbols: $$ f(a) \cdot \prod_{x \in (a, b]} f(x) = \prod_{x \in [a, b]} f(x) $$

Finset.prod_Ioc_mul_eq_prod_Icc theorem

(h : a ≤ b) : (∏ x ∈ Ioc a b, f x) * f a = ∏ x ∈ Icc a b, f x

Full source

@[to_additive]
lemma prod_Ioc_mul_eq_prod_Icc (h : a ≤ b) : (∏ x ∈ Ioc a b, f x) * f a = ∏ x ∈ Icc a b, f x := by
  rw [mul_comm, mul_prod_Ioc_eq_prod_Icc h]

Product Identity: $\left(\prod_{x \in (a, b]} f(x)\right) \cdot f(a) = \prod_{x \in [a, b]} f(x)$

Informal description

Let $\alpha$ be a locally finite order and $a, b \in \alpha$ with $a \leq b$. For any function $f : \alpha \to M$ where $M$ is a commutative monoid, the product of $f(x)$ over all $x$ in the open-closed interval $(a, b]$ multiplied by $f(a)$ equals the product of $f(x)$ over all $x$ in the closed interval $[a, b]$. In symbols: $$ \left(\prod_{x \in (a, b]} f(x)\right) \cdot f(a) = \prod_{x \in [a, b]} f(x) $$

Finset.mul_prod_Ioi_eq_prod_Ici theorem

(a : α) : f a * ∏ x ∈ Ioi a, f x = ∏ x ∈ Ici a, f x

Full source

@[to_additive]
lemma mul_prod_Ioi_eq_prod_Ici (a : α) : f a * ∏ x ∈ Ioi a, f x = ∏ x ∈ Ici a, f x := by
  rw [Ici_eq_cons_Ioi, prod_cons]

Product Identity: $f(a) \cdot \prod_{x > a} f(x) = \prod_{x \geq a} f(x)$

Informal description

For any element $a$ in a locally finite order with finite intervals bounded below, and any function $f$ defined on the order, the product of $f(a)$ with the product of $f(x)$ over all $x$ in the open interval $(a, \infty)$ is equal to the product of $f(x)$ over all $x$ in the closed interval $[a, \infty)$. In symbols: $f(a) \cdot \prod_{x \in (a, \infty)} f(x) = \prod_{x \in [a, \infty)} f(x)$.

Finset.prod_Ioi_mul_eq_prod_Ici theorem

(a : α) : (∏ x ∈ Ioi a, f x) * f a = ∏ x ∈ Ici a, f x

Full source

@[to_additive]
lemma prod_Ioi_mul_eq_prod_Ici (a : α) : (∏ x ∈ Ioi a, f x) * f a = ∏ x ∈ Ici a, f x := by
  rw [mul_comm, mul_prod_Ioi_eq_prod_Ici]

Product Identity: $\left(\prod_{x > a} f(x)\right) \cdot f(a) = \prod_{x \geq a} f(x)$

Informal description

For any element $a$ in a locally finite order with finite intervals bounded below, and any function $f$ defined on the order, the product of $f(x)$ over all $x$ in the open interval $(a, \infty)$ multiplied by $f(a)$ is equal to the product of $f(x)$ over all $x$ in the closed interval $[a, \infty)$. In symbols: $\left(\prod_{x > a} f(x)\right) \cdot f(a) = \prod_{x \geq a} f(x)$.

Finset.mul_prod_Iio_eq_prod_Iic theorem

(a : α) : f a * ∏ x ∈ Iio a, f x = ∏ x ∈ Iic a, f x

Full source

@[to_additive]
lemma mul_prod_Iio_eq_prod_Iic (a : α) : f a * ∏ x ∈ Iio a, f x = ∏ x ∈ Iic a, f x := by
  rw [Iic_eq_cons_Iio, prod_cons]

Product identity: $f(a) \cdot \prod_{x < a} f(x) = \prod_{x \leq a} f(x)$

Informal description

Let $\alpha$ be a type with a partial order and a locally finite order with finite lower-bounded intervals. For any element $a \in \alpha$ and any function $f : \alpha \to M$ where $M$ is a commutative monoid, the product of $f(a)$ with the product of $f(x)$ over all $x < a$ equals the product of $f(x)$ over all $x \leq a$. In symbols: \[ f(a) \cdot \prod_{x \in Iio(a)} f(x) = \prod_{x \in Iic(a)} f(x). \]

Finset.prod_Iio_mul_eq_prod_Iic theorem

(a : α) : (∏ x ∈ Iio a, f x) * f a = ∏ x ∈ Iic a, f x

Full source

@[to_additive]
lemma prod_Iio_mul_eq_prod_Iic (a : α) : (∏ x ∈ Iio a, f x) * f a = ∏ x ∈ Iic a, f x := by
  rw [mul_comm, mul_prod_Iio_eq_prod_Iic]

Product identity: $\left(\prod_{x < a} f(x)\right) \cdot f(a) = \prod_{x \leq a} f(x)$

Informal description

Let $\alpha$ be a partially ordered type with a locally finite order where all lower-bounded intervals are finite, and let $M$ be a commutative monoid. For any function $f : \alpha \to M$ and any element $a \in \alpha$, the product of $f(x)$ over all $x < a$ multiplied by $f(a)$ equals the product of $f(x)$ over all $x \leq a$. In symbols: \[ \left(\prod_{x < a} f(x)\right) \cdot f(a) = \prod_{x \leq a} f(x). \]

Finset.prod_prod_Ioi_mul_eq_prod_prod_off_diag theorem

(f : α → α → M) : ∏ i, ∏ j ∈ Ioi i, f j i * f i j = ∏ i, ∏ j ∈ { i }ᶜ, f j i

Full source

@[to_additive]
lemma prod_prod_Ioi_mul_eq_prod_prod_off_diag (f : α → α → M) :
    ∏ i, ∏ j ∈ Ioi i, f j i * f i j = ∏ i, ∏ j ∈ {i}ᶜ, f j i := by
  simp_rw [← Ioi_disjUnion_Iio, prod_disjUnion, prod_mul_distrib]
  congr 1
  rw [prod_sigma', prod_sigma']
  refine prod_nbij' (fun i ↦ ⟨i.2, i.1⟩) (fun i ↦ ⟨i.2, i.1⟩) ?_ ?_ ?_ ?_ ?_ <;> simp

Double product identity for off-diagonal terms: $\prod_i \prod_{j>i} f(j,i)f(i,j) = \prod_i \prod_{j \neq i} f(j,i)$

Informal description

Let $\alpha$ be a finite type with a linear order and $M$ a commutative monoid. For any function $f : \alpha \times \alpha \to M$, the double product over all pairs $(i,j)$ with $j > i$ of $f(j,i) \cdot f(i,j)$ equals the double product over all pairs $(i,j)$ with $j \neq i$ of $f(j,i)$. In symbols: \[ \prod_{i \in \alpha} \prod_{j \in \text{Ioi}(i)} f(j,i) \cdot f(i,j) = \prod_{i \in \alpha} \prod_{j \in \{i\}^c} f(j,i). \]

Finset.prod_Ico_add' theorem

 [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (f : α → M)
  (a b c : α) : (∏ x ∈ Ico a b, f (x + c)) = ∏ x ∈ Ico (a + c) (b + c), f x

Full source

@[to_additive]
theorem prod_Ico_add' [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α]
    [ExistsAddOfLE α] [LocallyFiniteOrder α]
    (f : α → M) (a b c : α) : (∏ x ∈ Ico a b, f (x + c)) = ∏ x ∈ Ico (a + c) (b + c), f x := by
  rw [← map_add_right_Ico, prod_map]
  rfl

Shifted Interval Product Identity: $\prod_{[a,b)} f(x + c) = \prod_{[a+c,b+c)} f(x)$

Informal description

Let $\alpha$ be an additive commutative monoid with a partial order, which is also an ordered cancellative additive monoid where one-sided subtraction exists and has a locally finite order. For any function $f : \alpha \to M$ (where $M$ is a commutative monoid) and any elements $a, b, c \in \alpha$, the product of $f(x + c)$ over the interval $[a, b)$ equals the product of $f(x)$ over the interval $[a + c, b + c)$. That is: \[ \prod_{x \in [a, b)} f(x + c) = \prod_{x \in [a + c, b + c)} f(x). \]

Finset.prod_Ico_add theorem

 [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] (f : α → M)
  (a b c : α) : (∏ x ∈ Ico a b, f (c + x)) = ∏ x ∈ Ico (a + c) (b + c), f x

Full source

@[to_additive]
theorem prod_Ico_add [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α]
    [ExistsAddOfLE α] [LocallyFiniteOrder α]
    (f : α → M) (a b c : α) : (∏ x ∈ Ico a b, f (c + x)) = ∏ x ∈ Ico (a + c) (b + c), f x := by
  convert prod_Ico_add' f a b c using 2
  rw [add_comm]

Shifted Interval Product Identity: $\prod_{[a,b)} f(c + x) = \prod_{[a+c,b+c)} f(x)$

Informal description

Let $\alpha$ be an additive commutative monoid with a partial order, which is also an ordered cancellative additive monoid where one-sided subtraction exists and has a locally finite order. For any function $f : \alpha \to M$ (where $M$ is a commutative monoid) and any elements $a, b, c \in \alpha$, the product of $f(c + x)$ over the interval $[a, b)$ equals the product of $f(x)$ over the interval $[a + c, b + c)$. That is: \[ \prod_{x \in [a, b)} f(c + x) = \prod_{x \in [a + c, b + c)} f(x). \]

Finset.prod_Ico_add_right_sub_eq theorem

 [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [LocallyFiniteOrder α] [Sub α]
  [OrderedSub α] (a b c : α) : ∏ x ∈ Ico (a + c) (b + c), f (x - c) = ∏ x ∈ Ico a b, f x

Full source

@[to_additive (attr := simp)]
theorem prod_Ico_add_right_sub_eq [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α]
    [ExistsAddOfLE α] [LocallyFiniteOrder α] [Sub α] [OrderedSub α] (a b c : α) :
    ∏ x ∈ Ico (a + c) (b + c), f (x - c) = ∏ x ∈ Ico a b, f x := by
  simp only [← map_add_right_Ico, prod_map, addRightEmbedding_apply, add_tsub_cancel_right]

Shifted Interval Product Equality: $\prod_{[a+c, b+c)} f(x - c) = \prod_{[a, b)} f(x)$

Informal description

Let $\alpha$ be an additive commutative monoid with a partial order, which is also an ordered cancellative additive monoid where one-sided subtraction exists and has a locally finite order. Suppose $\alpha$ is equipped with a subtraction operation satisfying the ordered subtraction property. Then for any function $f : \alpha \to M$ (where $M$ is a commutative monoid) and any elements $a, b, c \in \alpha$, the product of $f(x - c)$ over the interval $[a + c, b + c)$ equals the product of $f(x)$ over the interval $[a, b)$. That is: $$ \prod_{x \in [a + c, b + c)} f(x - c) = \prod_{x \in [a, b)} f(x). $$

Finset.prod_Ico_succ_top theorem

{a b : ℕ} (hab : a ≤ b) (f : ℕ → M) : (∏ k ∈ Ico a (b + 1), f k) = (∏ k ∈ Ico a b, f k) * f b

Full source

@[to_additive]
theorem prod_Ico_succ_top {a b : ℕ} (hab : a ≤ b) (f : ℕ → M) :
    (∏ k ∈ Ico a (b + 1), f k) = (∏ k ∈ Ico a b, f k) * f b := by
  rw [Nat.Ico_succ_right_eq_insert_Ico hab, prod_insert right_not_mem_Ico, mul_comm]

Product over $[a, b+1)$ as product over $[a, b)$ times $f(b)$

Informal description

Let $M$ be a commutative monoid and $f : \mathbb{N} \to M$ be a function. For any natural numbers $a \leq b$, the product of $f$ over the interval $[a, b+1)$ is equal to the product over $[a, b)$ multiplied by $f(b)$. That is: $$ \prod_{k \in [a, b+1)} f(k) = \left( \prod_{k \in [a, b)} f(k) \right) \cdot f(b). $$

Finset.prod_eq_prod_Ico_succ_bot theorem

{a b : ℕ} (hab : a < b) (f : ℕ → M) : ∏ k ∈ Ico a b, f k = f a * ∏ k ∈ Ico (a + 1) b, f k

Full source

@[to_additive]
theorem prod_eq_prod_Ico_succ_bot {a b : ℕ} (hab : a < b) (f : ℕ → M) :
    ∏ k ∈ Ico a b, f k = f a * ∏ k ∈ Ico (a + 1) b, f k := by
  have ha : a ∉ Ico (a + 1) b := by simp
  rw [← prod_insert ha, Nat.Ico_insert_succ_left hab]

Product Decomposition for Closed-Open Interval: $[a, b) = \{a\} \cdot [a+1, b)$

Informal description

Let $M$ be a commutative monoid and $f \colon \mathbb{N} \to M$ be a function. For any natural numbers $a < b$, the product of $f$ over the interval $[a, b)$ equals $f(a)$ multiplied by the product of $f$ over the interval $[a+1, b)$. That is: $$ \prod_{k \in [a, b)} f(k) = f(a) \cdot \prod_{k \in [a+1, b)} f(k). $$

Finset.prod_Ico_consecutive theorem

 (f : ℕ → M) {m n k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) : ((∏ i ∈ Ico m n, f i) * ∏ i ∈ Ico n k, f i) = ∏ i ∈ Ico m k, f i

Full source

@[to_additive]
theorem prod_Ico_consecutive (f : ℕ → M) {m n k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) :
    ((∏ i ∈ Ico m n, f i) * ∏ i ∈ Ico n k, f i) = ∏ i ∈ Ico m k, f i :=
  Ico_union_Ico_eq_Ico hmn hnk ▸ Eq.symm (prod_union (Ico_disjoint_Ico_consecutive m n k))

Product Splitting over Consecutive Intervals: $[m, n) \cdot [n, k) = [m, k)$

Informal description

Let $M$ be a commutative monoid and $f : \mathbb{N} \to M$ be a function. For any natural numbers $m, n, k$ such that $m \leq n \leq k$, the product of $f$ over the interval $[m, n)$ multiplied by the product of $f$ over the interval $[n, k)$ is equal to the product of $f$ over the interval $[m, k)$. In symbols: $$ \left( \prod_{i \in [m, n)} f(i) \right) \cdot \left( \prod_{i \in [n, k)} f(i) \right) = \prod_{i \in [m, k)} f(i). $$

Finset.prod_Ioc_consecutive theorem

 (f : ℕ → M) {m n k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) : ((∏ i ∈ Ioc m n, f i) * ∏ i ∈ Ioc n k, f i) = ∏ i ∈ Ioc m k, f i

Full source

@[to_additive]
theorem prod_Ioc_consecutive (f : ℕ → M) {m n k : ℕ} (hmn : m ≤ n) (hnk : n ≤ k) :
    ((∏ i ∈ Ioc m n, f i) * ∏ i ∈ Ioc n k, f i) = ∏ i ∈ Ioc m k, f i := by
  rw [← Ioc_union_Ioc_eq_Ioc hmn hnk, prod_union]
  apply disjoint_left.2 fun x hx h'x => _
  intros x hx h'x
  exact lt_irrefl _ ((mem_Ioc.1 h'x).1.trans_le (mem_Ioc.1 hx).2)

Product Splitting over Consecutive Open-Closed Intervals: $(m, n] \cdot (n, k] = (m, k]$

Informal description

Let $M$ be a commutative monoid and $f \colon \mathbb{N} \to M$ be a function. For any natural numbers $m, n, k$ such that $m \leq n \leq k$, the product of $f$ over the open-closed interval $(m, n]$ multiplied by the product of $f$ over the open-closed interval $(n, k]$ is equal to the product of $f$ over the open-closed interval $(m, k]$. In symbols: $$ \left( \prod_{i \in (m, n]} f(i) \right) \cdot \left( \prod_{i \in (n, k]} f(i) \right) = \prod_{i \in (m, k]} f(i). $$

Finset.prod_Ioc_succ_top theorem

{a b : ℕ} (hab : a ≤ b) (f : ℕ → M) : (∏ k ∈ Ioc a (b + 1), f k) = (∏ k ∈ Ioc a b, f k) * f (b + 1)

Full source

@[to_additive]
theorem prod_Ioc_succ_top {a b : ℕ} (hab : a ≤ b) (f : ℕ → M) :
    (∏ k ∈ Ioc a (b + 1), f k) = (∏ k ∈ Ioc a b, f k) * f (b + 1) := by
  rw [← prod_Ioc_consecutive _ hab (Nat.le_succ b), Nat.Ioc_succ_singleton, prod_singleton]

Product over $(a, b+1]$ as product over $(a, b]$ times $f(b+1)$

Informal description

Let $M$ be a commutative monoid and $f \colon \mathbb{N} \to M$ be a function. For any natural numbers $a, b$ such that $a \leq b$, the product of $f$ over the open-closed interval $(a, b+1]$ is equal to the product over $(a, b]$ multiplied by $f(b+1)$. That is: $$ \prod_{k \in (a, b+1]} f(k) = \left( \prod_{k \in (a, b]} f(k) \right) \cdot f(b+1). $$

Finset.prod_Icc_succ_top theorem

{a b : ℕ} (hab : a ≤ b + 1) (f : ℕ → M) : (∏ k ∈ Icc a (b + 1), f k) = (∏ k ∈ Icc a b, f k) * f (b + 1)

Full source

@[to_additive]
theorem prod_Icc_succ_top {a b : ℕ} (hab : a ≤ b + 1) (f : ℕ → M) :
    (∏ k ∈ Icc a (b + 1), f k) = (∏ k ∈ Icc a b, f k) * f (b + 1) := by
  rw [← Nat.Ico_succ_right, prod_Ico_succ_top hab, Nat.Ico_succ_right]

Product over $[a, b+1]$ as product over $[a, b]$ times $f(b+1)$

Informal description

Let $M$ be a commutative monoid and $f : \mathbb{N} \to M$ be a function. For any natural numbers $a, b$ such that $a \leq b + 1$, the product of $f$ over the closed interval $[a, b+1]$ is equal to the product over $[a, b]$ multiplied by $f(b+1)$. That is: $$ \prod_{k \in [a, b+1]} f(k) = \left( \prod_{k \in [a, b]} f(k) \right) \cdot f(b+1). $$

Finset.prod_range_mul_prod_Ico theorem

 (f : ℕ → M) {m n : ℕ} (h : m ≤ n) : ((∏ k ∈ range m, f k) * ∏ k ∈ Ico m n, f k) = ∏ k ∈ range n, f k

Full source

@[to_additive]
theorem prod_range_mul_prod_Ico (f : ℕ → M) {m n : ℕ} (h : m ≤ n) :
    ((∏ k ∈ range m, f k) * ∏ k ∈ Ico m n, f k) = ∏ k ∈ range n, f k :=
  Nat.Ico_zero_eq_range ▸ Nat.Ico_zero_eq_range ▸ prod_Ico_consecutive f m.zero_le h

Product Splitting: $\text{range}(m) \cdot [m, n) = \text{range}(n)$

Informal description

Let $M$ be a commutative monoid and $f : \mathbb{N} \to M$ be a function. For any natural numbers $m, n$ such that $m \leq n$, the product of $f$ over the range $\{0, \dots, m-1\}$ multiplied by the product of $f$ over the interval $[m, n)$ equals the product of $f$ over the range $\{0, \dots, n-1\}$. In symbols: $$ \left( \prod_{k \in \{0, \dots, m-1\}} f(k) \right) \cdot \left( \prod_{k \in [m, n)} f(k) \right) = \prod_{k \in \{0, \dots, n-1\}} f(k). $$

Finset.prod_range_eq_mul_Ico theorem

(f : ℕ → M) {n : ℕ} (hn : 0 < n) : ∏ x ∈ Finset.range n, f x = f 0 * ∏ x ∈ Ico 1 n, f x

Full source

@[to_additive]
theorem prod_range_eq_mul_Ico (f : ℕ → M) {n : ℕ} (hn : 0 < n) :
    ∏ x ∈ Finset.range n, f x = f 0 * ∏ x ∈ Ico 1 n, f x :=
  Finset.range_eq_Ico ▸ Finset.prod_eq_prod_Ico_succ_bot hn f

Product Decomposition: $\text{range}(n) = \{0\} \cdot [1, n)$

Informal description

Let $M$ be a commutative monoid and $f \colon \mathbb{N} \to M$ be a function. For any positive natural number $n$, the product of $f$ over the range $\{0, \dots, n-1\}$ equals $f(0)$ multiplied by the product of $f$ over the interval $[1, n)$. That is: $$ \prod_{k=0}^{n-1} f(k) = f(0) \cdot \prod_{k \in [1, n)} f(k). $$

Finset.prod_Ico_eq_mul_inv theorem

 {δ : Type*} [CommGroup δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) :
  ∏ k ∈ Ico m n, f k = (∏ k ∈ range n, f k) * (∏ k ∈ range m, f k)⁻¹

Full source

@[to_additive]
theorem prod_Ico_eq_mul_inv {δ : Type*} [CommGroup δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) :
    ∏ k ∈ Ico m n, f k = (∏ k ∈ range n, f k) * (∏ k ∈ range m, f k)⁻¹ :=
  eq_mul_inv_iff_mul_eq.2 <| by (rw [mul_comm]; exact prod_range_mul_prod_Ico f h)

Product over Interval as Product over Range Multiplied by Inverse

Informal description

Let $\delta$ be a commutative group and $f : \mathbb{N} \to \delta$ be a function. For any natural numbers $m, n$ such that $m \leq n$, the product of $f$ over the interval $[m, n)$ equals the product of $f$ over the range $\{0, \dots, n-1\}$ multiplied by the inverse of the product of $f$ over the range $\{0, \dots, m-1\}$. In symbols: $$ \prod_{k \in [m, n)} f(k) = \left( \prod_{k \in \{0, \dots, n-1\}} f(k) \right) \cdot \left( \prod_{k \in \{0, \dots, m-1\}} f(k) \right)^{-1}. $$

Finset.prod_Ico_eq_div theorem

 {δ : Type*} [CommGroup δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) :
  ∏ k ∈ Ico m n, f k = (∏ k ∈ range n, f k) / ∏ k ∈ range m, f k

Full source

@[to_additive]
theorem prod_Ico_eq_div {δ : Type*} [CommGroup δ] (f : ℕ → δ) {m n : ℕ} (h : m ≤ n) :
    ∏ k ∈ Ico m n, f k = (∏ k ∈ range n, f k) / ∏ k ∈ range m, f k := by
  simpa only [div_eq_mul_inv] using prod_Ico_eq_mul_inv f h

Product over Interval as Quotient of Range Products

Informal description

Let $\delta$ be a commutative group and $f : \mathbb{N} \to \delta$ be a function. For any natural numbers $m, n$ with $m \leq n$, the product of $f$ over the interval $[m, n)$ equals the quotient of the product of $f$ over $\{0, \dots, n-1\}$ divided by the product of $f$ over $\{0, \dots, m-1\}$. In symbols: $$ \prod_{k \in [m, n)} f(k) = \frac{\prod_{k \in \{0, \dots, n-1\}} f(k)}{\prod_{k \in \{0, \dots, m-1\}} f(k)}. $$

Finset.prod_range_div_prod_range theorem

 {α : Type*} [CommGroup α] {f : ℕ → α} {n m : ℕ} (hnm : n ≤ m) :
  ((∏ k ∈ range m, f k) / ∏ k ∈ range n, f k) = ∏ k ∈ range m with n ≤ k, f k

Full source

@[to_additive]
theorem prod_range_div_prod_range {α : Type*} [CommGroup α] {f : ℕ → α} {n m : ℕ} (hnm : n ≤ m) :
    ((∏ k ∈ range m, f k) / ∏ k ∈ range n, f k) = ∏ k ∈ range m with n ≤ k, f k := by
  rw [← prod_Ico_eq_div f hnm]
  congr
  apply Finset.ext
  simp only [mem_Ico, mem_filter, mem_range, *]
  tauto

Quotient of Range Products Equals Product over Filtered Range

Informal description

Let $\alpha$ be a commutative group and $f : \mathbb{N} \to \alpha$ be a function. For any natural numbers $n, m$ with $n \leq m$, the quotient of the product of $f$ over $\{0, \dots, m-1\}$ divided by the product of $f$ over $\{0, \dots, n-1\}$ equals the product of $f$ over the subset $\{k \in \{0, \dots, m-1\} \mid n \leq k\}$. In symbols: $$ \frac{\prod_{k \in \{0, \dots, m-1\}} f(k)}{\prod_{k \in \{0, \dots, n-1\}} f(k)} = \prod_{\substack{k \in \{0, \dots, m-1\} \\ n \leq k}} f(k). $$

Finset.sum_Ico_Ico_comm theorem

 {M : Type*} [AddCommMonoid M] (a b : ℕ) (f : ℕ → ℕ → M) :
  (∑ i ∈ Finset.Ico a b, ∑ j ∈ Finset.Ico i b, f i j) = ∑ j ∈ Finset.Ico a b, ∑ i ∈ Finset.Ico a (j + 1), f i j

Full source

/-- The two ways of summing over `(i, j)` in the range `a ≤ i ≤ j < b` are equal. -/
theorem sum_Ico_Ico_comm {M : Type*} [AddCommMonoid M] (a b : ℕ) (f : ℕ → ℕ → M) :
    (∑ i ∈ Finset.Ico a b, ∑ j ∈ Finset.Ico i b, f i j) =
      ∑ j ∈ Finset.Ico a b, ∑ i ∈ Finset.Ico a (j + 1), f i j := by
  rw [Finset.sum_sigma', Finset.sum_sigma']
  refine sum_nbij' (fun x ↦ ⟨x.2, x.1⟩) (fun x ↦ ⟨x.2, x.1⟩) ?_ ?_ (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl) <;>
  simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma] <;>
  rintro a b ⟨⟨h₁, h₂⟩, ⟨h₃, h₄⟩⟩ <;>
  omega

Commutativity of Double Summation over Half-Open Interval

Informal description

Let $M$ be an additive commutative monoid, and let $a, b$ be natural numbers with $a \leq b$. For any function $f : \mathbb{N} \times \mathbb{N} \to M$, the double sum over pairs $(i, j)$ where $i$ ranges from $a$ to $b-1$ and $j$ ranges from $i$ to $b-1$ is equal to the double sum where $j$ ranges from $a$ to $b-1$ and $i$ ranges from $a$ to $j$. That is, $$ \sum_{i=a}^{b-1} \sum_{j=i}^{b-1} f(i,j) = \sum_{j=a}^{b-1} \sum_{i=a}^{j} f(i,j). $$

Finset.sum_Ico_Ico_comm' theorem

 {M : Type*} [AddCommMonoid M] (a b : ℕ) (f : ℕ → ℕ → M) :
  (∑ i ∈ Finset.Ico a b, ∑ j ∈ Finset.Ico (i + 1) b, f i j) = ∑ j ∈ Finset.Ico a b, ∑ i ∈ Finset.Ico a j, f i j

Full source

/-- The two ways of summing over `(i, j)` in the range `a ≤ i < j < b` are equal. -/
theorem sum_Ico_Ico_comm' {M : Type*} [AddCommMonoid M] (a b : ℕ) (f : ℕ → ℕ → M) :
    (∑ i ∈ Finset.Ico a b, ∑ j ∈ Finset.Ico (i + 1) b, f i j) =
      ∑ j ∈ Finset.Ico a b, ∑ i ∈ Finset.Ico a j, f i j := by
  rw [Finset.sum_sigma', Finset.sum_sigma']
  refine sum_nbij' (fun x ↦ ⟨x.2, x.1⟩) (fun x ↦ ⟨x.2, x.1⟩) ?_ ?_ (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
    (fun _ _ ↦ rfl) <;>
  simp only [Finset.mem_Ico, Sigma.forall, Finset.mem_sigma] <;>
  rintro a b ⟨⟨h₁, h₂⟩, ⟨h₃, h₄⟩⟩ <;>
  omega

Commutativity of Double Summation over Strictly Ordered Pairs in Half-Open Interval

Informal description

Let $M$ be an additive commutative monoid, and let $a, b$ be natural numbers with $a \leq b$. For any function $f : \mathbb{N} \times \mathbb{N} \to M$, the double sum over pairs $(i, j)$ where $i$ ranges from $a$ to $b-1$ and $j$ ranges from $i+1$ to $b-1$ is equal to the double sum where $j$ ranges from $a$ to $b-1$ and $i$ ranges from $a$ to $j-1$. That is, $$ \sum_{i=a}^{b-1} \sum_{j=i+1}^{b-1} f(i,j) = \sum_{j=a}^{b-1} \sum_{i=a}^{j-1} f(i,j). $$

Finset.prod_Ico_eq_prod_range theorem

(f : ℕ → M) (m n : ℕ) : ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k)

Full source

@[to_additive]
theorem prod_Ico_eq_prod_range (f : ℕ → M) (m n : ℕ) :
    ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k) := by
  by_cases h : m ≤ n
  · rw [← Nat.Ico_zero_eq_range, prod_Ico_add, zero_add, tsub_add_cancel_of_le h]
  · replace h : n ≤ m := le_of_not_ge h
    rw [Ico_eq_empty_of_le h, tsub_eq_zero_iff_le.mpr h, range_zero, prod_empty, prod_empty]

Product over half-open interval equals product over shifted range: $\prod_{[m,n)} f(k) = \prod_{k=0}^{n-m-1} f(m+k)$

Informal description

Let $M$ be a commutative monoid and $f : \mathbb{N} \to M$ a function. For any natural numbers $m \leq n$, the product of $f(k)$ over the half-open interval $[m, n)$ is equal to the product of $f(m + k)$ over the range $\{0, 1, \dots, (n - m) - 1\}$. That is, \[ \prod_{k \in [m, n)} f(k) = \prod_{k=0}^{n - m - 1} f(m + k). \]

Finset.prod_Ico_reflect theorem

 (f : ℕ → M) (k : ℕ) {m n : ℕ} (h : m ≤ n + 1) : (∏ j ∈ Ico k m, f (n - j)) = ∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j

Full source

theorem prod_Ico_reflect (f : ℕ → M) (k : ℕ) {m n : ℕ} (h : m ≤ n + 1) :
    (∏ j ∈ Ico k m, f (n - j)) = ∏ j ∈ Ico (n + 1 - m) (n + 1 - k), f j := by
  have : ∀ i < m, i ≤ n := by
    intro i hi
    exact (add_le_add_iff_right 1).1 (le_trans (Nat.lt_iff_add_one_le.1 hi) h)
  rcases lt_or_le k m with hkm | hkm
  · rw [← Nat.Ico_image_const_sub_eq_Ico (this _ hkm)]
    refine (prod_image ?_).symm
    simp only [mem_Ico]
    rintro i ⟨_, im⟩ j ⟨_, jm⟩ Hij
    rw [← tsub_tsub_cancel_of_le (this _ im), Hij, tsub_tsub_cancel_of_le (this _ jm)]
  · have : n + 1 - k ≤ n + 1 - m := by
      rw [tsub_le_tsub_iff_left h]
      exact hkm
    simp only [hkm, Ico_eq_empty_of_le, prod_empty, tsub_le_iff_right, Ico_eq_empty_of_le
      this]

Reflection Property of Products over Half-Open Intervals in Natural Numbers

Informal description

Let $M$ be a commutative monoid and $f : \mathbb{N} \to M$ a function. For any natural numbers $k, m, n$ with $m \leq n + 1$, the product of $f(n - j)$ over $j$ in the interval $[k, m)$ is equal to the product of $f(j)$ over $j$ in the interval $[n + 1 - m, n + 1 - k)$. That is, $$ \prod_{j \in [k, m)} f(n - j) = \prod_{j \in [n + 1 - m, n + 1 - k)} f(j). $$

Finset.sum_Ico_reflect theorem

 {δ : Type*} [AddCommMonoid δ] (f : ℕ → δ) (k : ℕ) {m n : ℕ} (h : m ≤ n + 1) :
  (∑ j ∈ Ico k m, f (n - j)) = ∑ j ∈ Ico (n + 1 - m) (n + 1 - k), f j

Full source

theorem sum_Ico_reflect {δ : Type*} [AddCommMonoid δ] (f : ℕ → δ) (k : ℕ) {m n : ℕ}
    (h : m ≤ n + 1) : (∑ j ∈ Ico k m, f (n - j)) = ∑ j ∈ Ico (n + 1 - m) (n + 1 - k), f j :=
  @prod_Ico_reflect (Multiplicative δ) _ f k m n h

Reflection Property of Sums over Half-Open Intervals in Natural Numbers

Informal description

Let $\delta$ be an additive commutative monoid and $f : \mathbb{N} \to \delta$ a function. For any natural numbers $k, m, n$ with $m \leq n + 1$, the sum of $f(n - j)$ over $j$ in the interval $[k, m)$ is equal to the sum of $f(j)$ over $j$ in the interval $[n + 1 - m, n + 1 - k)$. That is, $$ \sum_{j \in [k, m)} f(n - j) = \sum_{j \in [n + 1 - m, n + 1 - k)} f(j). $$

Finset.prod_range_reflect theorem

(f : ℕ → M) (n : ℕ) : (∏ j ∈ range n, f (n - 1 - j)) = ∏ j ∈ range n, f j

Full source

theorem prod_range_reflect (f : ℕ → M) (n : ℕ) :
    (∏ j ∈ range n, f (n - 1 - j)) = ∏ j ∈ range n, f j := by
  cases n
  · simp
  · simp only [← Nat.Ico_zero_eq_range, Nat.succ_sub_succ_eq_sub, tsub_zero]
    rw [prod_Ico_reflect _ _ le_rfl]
    simp

Reflection Property of Products over Range: $\prod_{j=0}^{n-1} f(n-1-j) = \prod_{j=0}^{n-1} f(j)$

Informal description

Let $M$ be a commutative monoid and $f : \mathbb{N} \to M$ a function. For any natural number $n$, the product of $f(n - 1 - j)$ over $j$ in the range $\{0, 1, \dots, n-1\}$ is equal to the product of $f(j)$ over the same range. That is, \[ \prod_{j=0}^{n-1} f(n - 1 - j) = \prod_{j=0}^{n-1} f(j). \]

Finset.sum_range_reflect theorem

 {δ : Type*} [AddCommMonoid δ] (f : ℕ → δ) (n : ℕ) : (∑ j ∈ range n, f (n - 1 - j)) = ∑ j ∈ range n, f j

Full source

theorem sum_range_reflect {δ : Type*} [AddCommMonoid δ] (f : ℕ → δ) (n : ℕ) :
    (∑ j ∈ range n, f (n - 1 - j)) = ∑ j ∈ range n, f j :=
  @prod_range_reflect (Multiplicative δ) _ f n

Reflection Property of Sums over Range: $\sum_{j=0}^{n-1} f(n-1-j) = \sum_{j=0}^{n-1} f(j)$

Informal description

Let $\delta$ be an additive commutative monoid and $f : \mathbb{N} \to \delta$ a function. For any natural number $n$, the sum of $f(n - 1 - j)$ over $j$ in the range $\{0, 1, \dots, n-1\}$ is equal to the sum of $f(j)$ over the same range. That is, \[ \sum_{j=0}^{n-1} f(n - 1 - j) = \sum_{j=0}^{n-1} f(j). \]

Finset.prod_Ico_id_eq_factorial theorem

: ∀ n : ℕ, (∏ x ∈ Ico 1 (n + 1), x) = n !

Full source

@[simp]
theorem prod_Ico_id_eq_factorial : ∀ n : ℕ, (∏ x ∈ Ico 1 (n + 1), x) = n !
  | 0 => rfl
  | n + 1 => by
    rw [prod_Ico_succ_top <| Nat.succ_le_succ <| Nat.zero_le n, Nat.factorial_succ,
      prod_Ico_id_eq_factorial n, Nat.succ_eq_add_one, mul_comm]

Factorial as Product over Interval $[1, n+1)$

Informal description

For any natural number $n$, the product of all natural numbers in the closed-open interval $[1, n+1)$ is equal to the factorial of $n$, i.e., \[ \prod_{x \in [1, n+1)} x = n! \]

Finset.prod_range_add_one_eq_factorial theorem

: ∀ n : ℕ, (∏ x ∈ range n, (x + 1)) = n !

Full source

@[simp]
theorem prod_range_add_one_eq_factorial : ∀ n : ℕ, (∏ x ∈ range n, (x + 1)) = n !
  | 0 => rfl
  | n + 1 => by simp [factorial, Finset.range_succ, prod_range_add_one_eq_factorial n]

Factorial as Product of Successors: $\prod_{x=0}^{n-1} (x + 1) = n!$

Informal description

For any natural number $n$, the product of $(x + 1)$ for $x$ ranging from $0$ to $n-1$ equals the factorial of $n$, i.e., \[ \prod_{x=0}^{n-1} (x + 1) = n! \]

Finset.sum_range_id_mul_two theorem

(n : ℕ) : (∑ i ∈ range n, i) * 2 = n * (n - 1)

Full source

/-- Gauss' summation formula -/
theorem sum_range_id_mul_two (n : ℕ) : (∑ i ∈ range n, i) * 2 = n * (n - 1) :=
  calc
    (∑ i ∈ range n, i) * 2 = (∑ i ∈ range n, i) + ∑ i ∈ range n, (n - 1 - i) := by
      rw [sum_range_reflect (fun i => i) n, mul_two]
    _ = ∑ i ∈ range n, (i + (n - 1 - i)) := sum_add_distrib.symm
    _ = ∑ _ ∈ range n, (n - 1) :=
      sum_congr rfl fun _ hi => add_tsub_cancel_of_le <| Nat.le_sub_one_of_lt <| mem_range.1 hi
    _ = n * (n - 1) := by rw [sum_const, card_range, Nat.nsmul_eq_mul]

Twice Sum of First $n$ Natural Numbers Equals $n(n-1)$

Informal description

For any natural number $n$, twice the sum of the first $n$ natural numbers (from $0$ to $n-1$) equals $n$ times $(n - 1)$, i.e., \[ 2 \sum_{i=0}^{n-1} i = n(n - 1). \]

Finset.sum_range_id theorem

(n : ℕ) : ∑ i ∈ range n, i = n * (n - 1) / 2

Full source

/-- Gauss' summation formula -/
theorem sum_range_id (n : ℕ) : ∑ i ∈ range n, i = n * (n - 1) / 2 := by
  rw [← sum_range_id_mul_two n, Nat.mul_div_cancel _ zero_lt_two]

Sum of First $n$ Natural Numbers: $\sum_{i=0}^{n-1} i = \frac{n(n-1)}{2}$

Informal description

For any natural number $n$, the sum of the first $n$ natural numbers (from $0$ to $n-1$) equals $\frac{n(n - 1)}{2}$, i.e., \[ \sum_{i=0}^{n-1} i = \frac{n(n - 1)}{2}. \]

Finset.prod_range_diag_flip theorem

 (n : ℕ) (f : ℕ → ℕ → M) : (∏ m ∈ range n, ∏ k ∈ range (m + 1), f k (m - k)) = ∏ m ∈ range n, ∏ k ∈ range (n - m), f m k

Full source

@[to_additive]
lemma prod_range_diag_flip (n : ℕ) (f : ℕ → ℕ → M) :
    (∏ m ∈ range n, ∏ k ∈ range (m + 1), f k (m - k)) =
      ∏ m ∈ range n, ∏ k ∈ range (n - m), f m k := by
  rw [prod_sigma', prod_sigma']
  refine prod_nbij' (fun a ↦ ⟨a.2, a.1 - a.2⟩) (fun a ↦ ⟨a.1 + a.2, a.1⟩) ?_ ?_ ?_ ?_ ?_ <;>
    simp +contextual only [mem_sigma, mem_range, lt_tsub_iff_left,
      Nat.lt_succ_iff, le_add_iff_nonneg_right, Nat.zero_le, and_true, and_imp, imp_self,
      implies_true, Sigma.forall, forall_const, add_tsub_cancel_of_le, Sigma.mk.inj_iff,
      add_tsub_cancel_left, heq_eq_eq]
  exact fun a b han hba ↦ lt_of_le_of_lt hba han

Double Product Diagonal Flip Identity: $\prod_{m=0}^{n-1} \prod_{k=0}^m f(k, m - k) = \prod_{m=0}^{n-1} \prod_{k=0}^{n-m-1} f(m, k)$

Informal description

For any natural number $n$ and any function $f : \mathbb{N} \to \mathbb{N} \to M$ where $M$ is a commutative monoid, the following equality holds: \[ \prod_{m=0}^{n-1} \prod_{k=0}^m f(k, m - k) = \prod_{m=0}^{n-1} \prod_{k=0}^{n-m-1} f(m, k). \]

Finset.prod_range_succ_div_prod theorem

: ((∏ i ∈ range (n + 1), f i) / ∏ i ∈ range n, f i) = f n

Full source

@[to_additive]
theorem prod_range_succ_div_prod : ((∏ i ∈ range (n + 1), f i) / ∏ i ∈ range n, f i) = f n :=
  div_eq_iff_eq_mul'.mpr <| prod_range_succ f n

Ratio of Consecutive Product Ranges Equals Last Term: $\frac{\prod_{i=0}^n f(i)}{\prod_{i=0}^{n-1} f(i)} = f(n)$

Informal description

For any function $f$ defined on natural numbers and any natural number $n$, the ratio of the product of $f(i)$ over $i \in \{0, \ldots, n\}$ to the product of $f(i)$ over $i \in \{0, \ldots, n-1\}$ is equal to $f(n)$. That is, \[ \frac{\prod_{i=0}^n f(i)}{\prod_{i=0}^{n-1} f(i)} = f(n). \]

Finset.prod_range_succ_div_top theorem

: (∏ i ∈ range (n + 1), f i) / f n = ∏ i ∈ range n, f i

Full source

@[to_additive]
theorem prod_range_succ_div_top : (∏ i ∈ range (n + 1), f i) / f n = ∏ i ∈ range n, f i :=
  div_eq_iff_eq_mul.mpr <| prod_range_succ f n

Ratio of Product Range to Last Term Equals Previous Product: $\frac{\prod_{i=0}^n f(i)}{f(n)} = \prod_{i=0}^{n-1} f(i)$

Informal description

For any function $f$ defined on natural numbers and any natural number $n$, the ratio of the product of $f(i)$ over $i \in \{0, \ldots, n\}$ to $f(n)$ is equal to the product of $f(i)$ over $i \in \{0, \ldots, n-1\}$. That is, \[ \frac{\prod_{i=0}^n f(i)}{f(n)} = \prod_{i=0}^{n-1} f(i). \]

Finset.prod_Ico_div_bot theorem

(hmn : m < n) : (∏ i ∈ Ico m n, f i) / f m = ∏ i ∈ Ico (m + 1) n, f i

Full source

@[to_additive]
theorem prod_Ico_div_bot (hmn : m < n) : (∏ i ∈ Ico m n, f i) / f m = ∏ i ∈ Ico (m + 1) n, f i :=
  div_eq_iff_eq_mul'.mpr <| prod_eq_prod_Ico_succ_bot hmn _

Telescoping Product Identity for $[m, n)$: $\frac{\prod_{[m,n)} f(i)}{f(m)} = \prod_{[m+1,n)} f(i)$

Informal description

Let $M$ be a commutative group and $f : \mathbb{N} \to M$ be a function. For any natural numbers $m < n$, the ratio of the product of $f(i)$ over the interval $[m, n)$ to $f(m)$ equals the product of $f(i)$ over the interval $[m+1, n)$. That is: \[ \frac{\prod_{i \in [m, n)} f(i)}{f(m)} = \prod_{i \in [m+1, n)} f(i). \]

Finset.prod_Ico_succ_div_top theorem

(hmn : m ≤ n) : (∏ i ∈ Ico m (n + 1), f i) / f n = ∏ i ∈ Ico m n, f i

Full source

@[to_additive]
theorem prod_Ico_succ_div_top (hmn : m ≤ n) :
    (∏ i ∈ Ico m (n + 1), f i) / f n = ∏ i ∈ Ico m n, f i :=
  div_eq_iff_eq_mul.mpr <| prod_Ico_succ_top hmn _

Ratio of Product over $[m, n+1)$ to $f(n)$ Equals Product over $[m, n)$

Informal description

Let $M$ be a commutative group and $f : \mathbb{N} \to M$ be a function. For any natural numbers $m \leq n$, the ratio of the product of $f(i)$ over the interval $[m, n+1)$ to $f(n)$ is equal to the product of $f(i)$ over the interval $[m, n)$. That is: \[ \frac{\prod_{i \in [m, n+1)} f(i)}{f(n)} = \prod_{i \in [m, n)} f(i). \]

Finset.prod_Ico_div theorem

(hmn : m ≤ n) : ∏ i ∈ Ico m n, f (i + 1) / f i = f n / f m

Full source

@[to_additive]
theorem prod_Ico_div (hmn : m ≤ n) : ∏ i ∈ Ico m n, f (i + 1) / f i = f n / f m := by
  rw [prod_Ico_eq_div _ hmn, prod_range_div, prod_range_div, div_div_div_cancel_right]

Telescoping Product Identity for Intervals: $\prod_{i \in [m, n)} \frac{f(i+1)}{f(i)} = \frac{f(n)}{f(m)}$

Informal description

Let $M$ be a commutative group and $f : \mathbb{N} \to M$ be a function. For any natural numbers $m \leq n$, the product of the ratios $\frac{f(i+1)}{f(i)}$ over the interval $[m, n)$ equals the ratio $\frac{f(n)}{f(m)}$. That is: \[ \prod_{i \in [m, n)} \frac{f(i+1)}{f(i)} = \frac{f(n)}{f(m)}. \]