English
Same as above: the product over the List.ofFn equals the product over its index set.
Русский
То же самое: произведение List.ofFn равна произведению по его индексу.
LaTeX
$$$\\mathrm{List.ofFn}\\ f .prod = \\prod_{i} f(i)$$$
Lean4
/-- To prove a property of a finite product, it suffices to prove that the property is
multiplicative and holds on the factors. -/
@[to_additive /-- To prove a property of a finite sum, it suffices to prove that the property is
additive and holds on the summands. -/
]
theorem finprod_induction {f : α → M} (p : M → Prop) (hp₀ : p 1) (hp₁ : ∀ x y, p x → p y → p (x * y))
(hp₂ : ∀ i, p (f i)) : p (∏ᶠ i, f i) := by
rw [finprod]
split_ifs
exacts [Finset.prod_induction _ _ hp₁ hp₀ fun i _ => hp₂ _, hp₀]
