English
Let E/F be a finite-dimensional extension. If |Aut(E/F)| = [E:F], then E/F is Galois.
Русский
Пусть E/F — конечномерное расширение. Если |Aut(E/F)| = [E:F], то E/F — галуа.
LaTeX
$$$[E:F] < \infty \;\wedge\; |\mathrm{Aut}_F(E)| = [E:F] \;\Rightarrow\; E/F \text{ is Galois}$$$
Lean4
/-- Let $E / F$ be a finite extension of fields. If $|\text{Aut}(E/F)| = [E : F]$, then
$E$ is Galois over $F$. -/
@[stacks 09I1 "'if' part"]
theorem of_card_aut_eq_finrank [FiniteDimensional F E] (h : Nat.card (E ≃ₐ[F] E) = finrank F E) : IsGalois F E :=
by
apply of_fixedField_eq_bot
have p : 0 < finrank (IntermediateField.fixedField (⊤ : Subgroup (E ≃ₐ[F] E))) E := finrank_pos
classical
rw [← IntermediateField.finrank_eq_one_iff, ← mul_left_inj' (ne_of_lt p).symm, finrank_mul_finrank, ← h, one_mul,
IntermediateField.finrank_fixedField_eq_card]
apply Nat.card_congr
exact { toFun := fun g => ⟨g, Subgroup.mem_top g⟩, invFun := (↑) }
