English
If f and g are nonzero and appropriate IsSplittingField hypotheses hold, then f·g is IsSplittingField over the appropriate base.
Русский
Если f и g ненулевые и выполнены предположения об IsSplittingField, то произведение f и g является IsSplittingField над базовым полем.
LaTeX
$$mul$$
Lean4
theorem mul (f g : F[X]) (hf : f ≠ 0) (hg : g ≠ 0) [IsSplittingField F K f]
[IsSplittingField K L (g.map <| algebraMap F K)] : IsSplittingField F L (f * g) :=
⟨(IsScalarTower.algebraMap_eq F K L).symm ▸
splits_mul _ (splits_comp_of_splits _ _ (splits K f))
((splits_map_iff _ _).1 (splits L <| g.map <| algebraMap F K)),
by
classical
rw [rootSet, aroots_mul (mul_ne_zero hf hg), Multiset.toFinset_add, Finset.coe_union,
Algebra.adjoin_union_eq_adjoin_adjoin, aroots_def, aroots_def, IsScalarTower.algebraMap_eq F K L, ← map_map,
roots_map (algebraMap K L) ((splits_id_iff_splits <| algebraMap F K).2 <| splits K f), Multiset.toFinset_map,
Finset.coe_image, Algebra.adjoin_algebraMap, ← rootSet, adjoin_rootSet, Algebra.map_top,
IsScalarTower.adjoin_range_toAlgHom, ← map_map, ← rootSet, adjoin_rootSet, Subalgebra.restrictScalars_top]⟩
