Theorems · Theorem · group theory

Finset.prod_range_induction

∀ {M : Type u_4} [inst : CommMonoid M] (f s : ℕ → M),
  s 0 = 1 → ∀ (n : ℕ), (∀ k < n, s (k + 1) = s k * f k) → ∏ k ∈ Finset.range n, f k = s n

For any product along {0, ..., n - 1} of a commutative-monoid-valued function, we can verify that it's equal to a different function just by checking ratios of adjacent terms up to n. This is a multiplicative discrete analogue of the fundamental theorem of calculus.

Defined in

Mathlib.Algebra.BigOperators.Group.Finset.Basic

Cited by

4 results in Mathlib

Foundations

Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoid