English
A finite-dimensional extension is Liouville over the base field.
Русский
Конечнодименсиональное расширение является Liouville над базовым полем.
LaTeX
$$$\\mathrm{IsLiouville}\\ F\\ K$$$
Lean4
/-- We lift `isLiouville_of_finiteDimensional_galois` to non-Galois field extensions by using it for the
normal closure then obtaining it for `F`.
-/
instance isLiouville_of_finiteDimensional [FiniteDimensional F K] : IsLiouville F K :=
let map := IsAlgClosed.lift (M := AlgebraicClosure F) (R := F) (S := K)
let K' := map.fieldRange
have : FiniteDimensional F K' := LinearMap.finiteDimensional_range map.toLinearMap
let K'' := normalClosure F K' (AlgebraicClosure F)
let B : IntermediateField F K'' := IntermediateField.restrict (F := K') (IntermediateField.le_normalClosure ..)
have kequiv : K ≃ₐ[F] ↥B :=
(show K ≃ₐ[F] K' from AlgEquiv.ofInjectiveField map).trans (IntermediateField.restrict_algEquiv _)
IsLiouville.equiv kequiv.symm
