English
Let s_j be a family of polynomials s_j ∈ K[X] indexed by a type ι, and t a finite set of ι. If every s_j splits via i, then their product ∏_{x ∈ t} s_x splits via i.
Русский
Пусть имеется family полиномов s_j ∈ K[X], индексируемых по ι, и конечное множество t ⊂ ι. Если для каждого j ∈ t полином s_j раскладывается через i, тогда произведение ∏_{x∈t} s_x раскладывается через i.
LaTeX
$$$\Big( \forall j \in t,\ s_j \text{ splits via } i \Big) \Rightarrow \Big( \prod_{x \in t} s_x \text{ splits via } i \Big)$$$
Lean4
theorem splits_prod {ι : Type u} {s : ι → K[X]} {t : Finset ι} : (∀ j ∈ t, (s j).Splits i) → (∏ x ∈ t, s x).Splits i :=
by
classical
refine Finset.induction_on t (fun _ => splits_one i) fun a t hat ih ht => ?_
rw [Finset.forall_mem_insert] at ht; rw [Finset.prod_insert hat]
exact splits_mul i ht.1 (ih ht.2)
