English
If f splits after composing i with j, and every root of f.map (j∘i) lies in the range of j, then f splits after applying i.
Русский
Если f распадается после композиции i и j, и каждый корень f.map (j∘i) принадлежит диапазону j, тогда f распадается после применения i.
LaTeX
$$$\forall f:K[X],\, j: L\to+^F,\, i: K\to+^L,\ (Splits (j\.comp\ i)\ f) \land (\forall a\in (f.map (j\.comp\ i)).roots, a\in j.range) \Rightarrow Splits\ i\ f$$$
Lean4
theorem splits_of_comp (j : L →+* F) {f : K[X]} (h : Splits (j.comp i) f)
(roots_mem_range : ∀ a ∈ (f.map (j.comp i)).roots, a ∈ j.range) : Splits i f :=
by
choose lift lift_eq using roots_mem_range
rw [splits_iff_exists_multiset]
refine ⟨(f.map (j.comp i)).roots.pmap lift fun _ ↦ id, map_injective _ j.injective ?_⟩
conv_lhs => rw [Polynomial.map_map, eq_prod_roots_of_splits h]
simp_rw [Polynomial.map_mul, Polynomial.map_multiset_prod, Multiset.map_pmap, Polynomial.map_sub, map_C, map_X,
lift_eq, Multiset.pmap_eq_map]
rfl
