periodic_prod — Mathlib

English

If each function indexed by elements of a finite set ι is c-periodic, then the finite product over the index set is c-periodic.

Русский

Если каждая функция f_i (для i в ι) периодична с периодом c, то произведение по i∈s f_i периодично с периодом c.

LaTeX

$$$\\forall s:\\,\\text{Finset}(ι), (\\forall i∈s, Periodic(f_i,c)) ⇒ Periodic(\\prod_{i∈s} f_i, c)$$$

Lean4

@[to_additive]
theorem _root_.Finset.periodic_prod [Add α] [CommMonoid β] {ι : Type*} {f : ι → α → β} (s : Finset ι)
    (hs : ∀ i ∈ s, Periodic (f i) c) : Periodic (∏ i ∈ s, f i) c :=
  s.prod_map_toList f ▸ (s.toList.map f).periodic_prod (by simpa [-Periodic])

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