finprod_eq_prod — Mathlib

English

If (mulSupport f).Finite, then the finprod equals the ordinary finite product over hf.toFinset.

Русский

Если mulSupport f конечна, то финпроизводство равно обычному конечному произведению по hf.toFinset.

LaTeX

$$$$ \prod^{\mathrm{fin}}_{i: \alpha} f(i) = \prod_{i \in hf.toFinset} f(i). $$$$

Lean4

@[to_additive]
theorem finprod_eq_prod (f : α → M) (hf : (mulSupport f).Finite) : ∏ᶠ i : α, f i = ∏ i ∈ hf.toFinset, f i := by
  classical rw [finprod_def, dif_pos hf]

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