English
If E/F is Galois and the automorphism group Aut(E/F) is finite, then E is finite-dimensional over F.
Русский
Если E/F Галуа и группа автоморфизмов Aut(E/F) конечна, тогда E конечномодульное над F (финитная размерность).
LaTeX
$$FiniteDimensional F E$$
Lean4
/-- A galois extension with finite galois group is finite dimensional.
The dimension is then equal to the order of the galois group via `IsGalois.card_aut_eq_finrank`. -/
theorem finiteDimensional_of_finite [IsGalois F E] [Finite (E ≃ₐ[F] E)] : FiniteDimensional F E :=
by
by_contra H
obtain ⟨K, h₁, h₂⟩ := exists_lt_finrank_of_infinite_dimensional H (Nat.card (E ≃ₐ[F] E))
let K' := normalClosure F K E
have : IsGalois F K' := ⟨⟩
have := Nat.card_le_card_of_surjective _ (AlgEquiv.restrictNormalHom_surjective (F := F) (K₁ := K') (E := E))
rw [IsGalois.card_aut_eq_finrank] at this
exact (this.trans_lt h₂).not_ge (finrank_le_of_le_right K.le_normalClosure)
