prod_Ico_div_bot — Mathlib

English

Let m < n and f: ℕ → M. Then (∏ i ∈ Ico m n, f(i)) / f(m) = ∏ i ∈ Ico (m+1) n, f(i).

Русский

Пусть m < n и f: ℕ → M. Тогда (∏_{i=m}^{n-1} f(i)) / f(m) = ∏_{i=m+1}^{n-1} f(i).

LaTeX

$$$$ \\frac{\\prod_{i \\in \\mathrm{Ico}(m,n)} f(i)}{f(m)} = \\prod_{i \\in \\mathrm{Ico}(m+1,n)} f(i). $$$$

Lean4

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

Похожие утверждения