English
Let i be a field homomorphism K → L, and let s: ι → K[X] be a finite family of polynomials. If every s(j) is nonzero for j in a finite set t, then the product ∏_{x ∈ t} s(x) splits over i if and only if every s(j) splits over i.
Русский
Пусть i: K → L – гомоморфизм полей, и пусть s: ι → K[X] образует конечную семейство многочленов. При условии, что для всех j ∈ t polynom s(j) ≠ 0, произведение ∏_{x ∈ t} s(x) распадается над i тогда и только тогда, когда каждый s(j) распадается над i.
LaTeX
$$$\\forall i\\, \\forall s:\\ ι \\to K[X], \\forall t: \\mathrm{Finset}\\ ι,\\; (\\forall j \\in t, s(j) \\neq 0) \\Rightarrow \\left(\\prod_{x \\in t} s(x)\\right)\\text{ Splits over } i \\iff \\forall j \\in t,\\ (s(j)).\\text{Splits over } i.$$$
Lean4
theorem splits_prod_iff {ι : Type u} {s : ι → K[X]} {t : Finset ι} :
(∀ j ∈ t, s j ≠ 0) → ((∏ x ∈ t, s x).Splits i ↔ ∀ j ∈ t, (s j).Splits i) := by
classical
refine
Finset.induction_on t (fun _ => ⟨fun _ _ h => by simp only [Finset.notMem_empty] at h, fun _ => splits_one i⟩)
fun a t hat ih ht => ?_
rw [Finset.forall_mem_insert] at ht ⊢
rw [Finset.prod_insert hat, splits_mul_iff i ht.1 (Finset.prod_ne_zero_iff.2 ht.2), ih ht.2]
