prod_flip — Mathlib

English

The product of a sequence f(n−r) for r from 0 to n equals the product of f(k) for k from 0 to n.

Русский

Произведение f(n−r) по r от 0 до n равно произведению f(k) по k от 0 до n.

LaTeX

$$$\\prod_{r=0}^{n} f(n-r) = \\prod_{k=0}^{n} f(k)$$$

Lean4

@[to_additive]
theorem prod_flip {n : ℕ} (f : ℕ → M) : (∏ r ∈ range (n + 1), f (n - r)) = ∏ k ∈ range (n + 1), f k := by
  induction n with
  | zero => rw [prod_range_one, prod_range_one]
  | succ n ih =>
    rw [prod_range_succ', prod_range_succ _ (Nat.succ n)]
    simp [← ih]

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