tprod_eq_finprod — Mathlib

English

If mulSupport f is finite, then the tprod equals the finite product over mulSupport.

Русский

Если поддержка умножения f конечна, то tprod равен произведению по этой поддержке.

LaTeX

$$∏'[L] b, f b = ∏ᶠ b, f b$$

Lean4

@[to_additive]
theorem tprod_eq_finprod [L.LeAtTop] (hf : (mulSupport f).Finite) : ∏'[L] b, f b = ∏ᶠ b, f b := by
  simp [tprod_def, multipliable_of_finite_mulSupport hf, hf, show L.HasSupport by infer_instance]

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