English
Let i be a field homomorphism from K to L. For polynomials f,g in K[X] with f ≠ 0 and g ≠ 0, the product f g splits over i if and only if f splits over i and g splits over i.
Русский
Пусть i – гомоморфизм полей K → L. Пусть f,g ∈ K[X] с f ≠ 0 и g ≠ 0. Произведение f g распадается над i тогда и только тогда, когда f распадается над i и g распадается над i.
LaTeX
$$$\\forall i\\, \\forall f,g : K[X],\\; f \\neq 0 \\land g \\neq 0 \\Rightarrow (f \\cdot g)\\text{ splits over } i \\Leftrightarrow (f \\text{ splits over } i) \\land (g \\text{ splits over } i).$$$
Lean4
theorem splits_mul_iff {f g : K[X]} (hf : f ≠ 0) (hg : g ≠ 0) : (f * g).Splits i ↔ f.Splits i ∧ g.Splits i :=
⟨splits_of_splits_mul i (mul_ne_zero hf hg), fun ⟨hfs, hgs⟩ => splits_mul i hfs hgs⟩
