English
If E / L / F is a tower of extensions and E is separable over F, then E is separable over L (tower_top). Conversely, if E is separable over F, then K is separable over F (tower_bot) with suitable tower conditions.
Русский
Если E над L над F — каскад расширений и E разделимо над F, то E разделимо над L (tower_top). Аналогично при tower_bot.
LaTeX
$$IsSeparable F E → IsSeparable L E$$
Lean4
/-- If `E / K / F` is a scalar tower and `algebraMap K E x` is separable over `F`, then `x` is
also separable over `F`. -/
theorem tower_bot {x : K} (h : IsSeparable F (algebraMap K E x)) : IsSeparable F x :=
have ⟨_q, hq⟩ := minpoly.dvd F x ((aeval_algebraMap_eq_zero_iff _ _ _).mp (minpoly.aeval F ((algebraMap K E) x)))
(Eq.mp (congrArg Separable hq) h).of_mul_left
