English
Let R be a commutative ring and {f_i} be polynomials indexed by a finite set s. If the f_i are pairwise coprime and each f_i is separable, then the product over i∈s of f_i is separable.
Русский
Пусть R — коммутативное кольцо и {f_i} — многочлены, индексируемые по конечному множеству s. Если они попарно взаимно просты и каждый из них сепарабелен, то произведение по i∈s f_i сепарабельно.
LaTeX
$$$ \left( \forall i \in s, \forall j \in s, i \neq j \Rightarrow \gcd(f_i,f_j)=1 \right) \land \left( \forall i \in s, \ (f_i) \text{ Separable} \right) \Rightarrow \left( \prod_{i \in s} f_i \right) \text{ Separable}$$$
Lean4
theorem separable_prod' {ι : Sort _} {f : ι → R[X]} {s : Finset ι} :
(∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → (∏ x ∈ s, f x).Separable := by
classical
exact
Finset.induction_on s (fun _ _ => separable_one) fun a s has ih h1 h2 =>
by
simp_rw [Finset.forall_mem_insert, forall_and] at h1 h2; rw [prod_insert has]
exact
h2.1.mul (ih h1.2.2 h2.2)
(IsCoprime.prod_right fun i his => h1.1.2 i his <| Ne.symm <| ne_of_mem_of_not_mem his has)
