English
In a tower of field extensions A / K / F, if A is finite over F and A is nontrivial, then K is finite over F.
Русский
В цикле расширений полей A / K / F, если A конечно по F и A не тождественно нулю, то K конечно по F.
LaTeX
$$$(\\text{A} \\neq 0) \\land (\\text{A is finite over } F) \\Rightarrow (K \\\\text{ is finite over } F)$$$
Lean4
/-- In a tower of field extensions `A / K / F`, if `A / F` is finite, so is `K / F`.
(In fact, it suffices that `A` is a nontrivial ring.)
Note this cannot be an instance as Lean cannot infer `A`.
-/
theorem left [Nontrivial A] : Module.Finite F K :=
let ⟨x, hx⟩ := exists_ne (0 : A)
Module.Finite.of_injective (LinearMap.ringLmapEquivSelf K ℕ A |>.symm x |>.restrictScalars F)
(smul_left_injective K hx)
