English
For a multiset s, s.prod equals the Finset product ∏ m ∈ s.toFinset, m^{count m s}.
Русский
Для мультисета s произведение равно произведению по его элементам и счётчикам: s.toFinset, m^{count m s}.
LaTeX
$$$\displaystyle s.prod = \prod m \in s.toFinset, m^{\mathrm{count}(m,s)}$$$
Lean4
/-- 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. -/
@[to_additive /-- For any sum along `{0, ..., n - 1}` of a commutative-monoid-valued function, we
can verify that it's equal to a different function just by checking differences of adjacent terms
up to `n`.
This is a discrete analogue of the fundamental theorem of calculus. -/
]
theorem prod_range_induction (f s : ℕ → M) (base : s 0 = 1) (n : ℕ) (step : ∀ k < n, s (k + 1) = s k * f k) :
∏ k ∈ Finset.range n, f k = s n := by
induction n with
| zero => rw [Finset.prod_range_zero, base]
| succ k hk =>
rw [Finset.prod_range_succ, step _ (Nat.lt_succ_self _), hk]
exact fun _ hl ↦ step _ (Nat.lt_succ_of_lt hl)
