English
If q1 and q2 are nonzero and p1 splits over q1.SplittingField and p2 splits over q2.SplittingField, then p1*p2 splits over (q1*q2).SplittingField.
Русский
Если q1 и q2 ненулевые, а p1 распадается над q1.SplittingField и p2 — над q2.SplittingField, то произведение p1 p2 распадается над SplittingField( q1 q2 ).
LaTeX
$$$\\text{Splits}(\\alpha, p1) \\land \\text{Splits}(\\alpha, p2) \\implies (p1 p2).Splits(\\text{algebraMap} F (q1 q2).SplittingField)$$$
Lean4
theorem mul_splits_in_splittingField_of_mul {p₁ q₁ p₂ q₂ : F[X]} (hq₁ : q₁ ≠ 0) (hq₂ : q₂ ≠ 0)
(h₁ : p₁.Splits (algebraMap F q₁.SplittingField)) (h₂ : p₂.Splits (algebraMap F q₂.SplittingField)) :
(p₁ * p₂).Splits (algebraMap F (q₁ * q₂).SplittingField) :=
by
apply splits_mul
· rw [←
(SplittingField.lift q₁
(splits_of_splits_of_dvd (algebraMap F (q₁ * q₂).SplittingField) (mul_ne_zero hq₁ hq₂)
(SplittingField.splits _) (dvd_mul_right q₁ q₂))).comp_algebraMap]
exact splits_comp_of_splits _ _ h₁
· rw [←
(SplittingField.lift q₂
(splits_of_splits_of_dvd (algebraMap F (q₁ * q₂).SplittingField) (mul_ne_zero hq₁ hq₂)
(SplittingField.splits _) (dvd_mul_left q₂ q₁))).comp_algebraMap]
exact splits_comp_of_splits _ _ h₂
