English
Let ι be an index set with Fintype and f_i ∈ R[X]. If the f_i are pairwise coprime in the sense of Function.onFun IsCoprime and each f_i is separable, then the product over i of f_i is separable.
Русский
Пусть ι — множество индексов, имеется конечноразмерное множество. Пусть f_i ∈ R[X]. Если f_i попарно взаимно просты (в смысле функции) и каждый f_i сепарабелен, то произведение по i∈ι f_i сепарабельно.
LaTeX
$$$ \text{Pairwise}( \operatorname{IsCoprime} \ on\ f) \land \forall i, (f(i))^Separable \Rightarrow \prod_i f(i) \Separable$$$
Lean4
theorem separable_prod {ι : Sort _} [Fintype ι] {f : ι → R[X]} (h1 : Pairwise (IsCoprime on f))
(h2 : ∀ x, (f x).Separable) : (∏ x, f x).Separable :=
separable_prod' (fun _x _hx _y _hy hxy => h1 hxy) fun x _hx => h2 x
