English
If every function in a finite list l of α → β is c-periodic, then the product of all functions in the list is c-periodic.
Русский
Если каждая функция из конечного списка l функций α → β имеет период c, то произведение всех функций из списка также имеет период c.
LaTeX
$$$\\forall l:\\ text{List}(α→β), (\\forall f ∈ l, Periodic(f,c)) \\Rightarrow Periodic(l.prod,c)$$$
Lean4
@[to_additive]
theorem _root_.List.periodic_prod [Add α] [MulOneClass β] (l : List (α → β)) (hl : ∀ f ∈ l, Periodic f c) :
Periodic l.prod c := by
induction l with
| nil => simp
| cons g l ih =>
rw [List.forall_mem_cons] at hl
simpa only [List.prod_cons] using hl.1.mul (ih hl.2)
