multipliable_prod — Mathlib

English

If for every i in a finite set s, f i is Multipliable, then the finite product ∏ i∈s f i is Multipliable.

Русский

Если для каждого i в конечном множестве s функция f i выполнима в смысле множимости, то конечно произведение по i∈s f i тоже выполнимо.

LaTeX

$$Multipliable (fun b => ∏ i ∈ s, f i b) L$$

Lean4

@[to_additive]
theorem multipliable_prod {f : γ → β → α} {s : Finset γ} (hf : ∀ i ∈ s, Multipliable (f i) L) :
    Multipliable (fun b ↦ ∏ i ∈ s, f i b) L :=
  (hasProd_prod fun i hi ↦ (hf i hi).hasProd).multipliable

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