English
The tower-top version: for any R, K, L, M with IsIntegral x over R and tower relations, if Splits holds after composition with the algebra map, then Splits holds after restriction.
Русский
Верификация верха башни: для любых R, K, L, M с интегрированностью x над R и т. д., если выполнено разложение после композиции отображения, то выполняется разложение после ограничения.
LaTeX
$$$\\forall f: K\\to+*L,\\; Splits(f\\circ algebraMap, \\minpoly R x) \\Rightarrow Splits(f, \\minpoly K x)$$$
Lean4
/-- The `RingHom` version of `IsIntegral.minpoly_splits_tower_top`. -/
theorem minpoly_splits_tower_top' (int : IsIntegral R x) {f : K →+* L}
(h : Splits (f.comp <| algebraMap R K) (minpoly R x)) : Splits f (minpoly K x) :=
splits_of_splits_of_dvd _ ((minpoly.monic int).map _).ne_zero ((splits_map_iff _ _).mpr h)
(minpoly.dvd_map_of_isScalarTower R _ x)
