diff --git a/Mathlib/Algebra/Field/Subfield/Basic.lean b/Mathlib/Algebra/Field/Subfield/Basic.lean
index 0f34ab90c7b2b1..97ff49468e4585 100644
--- a/Mathlib/Algebra/Field/Subfield/Basic.lean
+++ b/Mathlib/Algebra/Field/Subfield/Basic.lean
@@ -433,6 +433,12 @@ theorem coe_sSup_of_directedOn {S : Set (Subfield K)} (Sne : S.Nonempty)
 
 end Subfield
 
+variable (L) in
+/-- A field is finitely generated if it is the closure of a finite subset. -/
+@[mk_iff fg_iff]
+protected class Field.FG : Prop where
+  finitely_generated : ∃ S : Finset L, Subfield.closure (S : Set L) = ⊤
+
 namespace RingHom
 
 variable {s : Subfield K}
diff --git a/Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean b/Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
index 037a6c723713d1..517d2987696954 100644
--- a/Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
+++ b/Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
@@ -124,6 +124,11 @@ lemma essFiniteType_iff {K : IntermediateField F E} :
       adjoin_map, ← Set.range_comp, Function.comp_def, ← AlgHom.fieldRange_eq_map] using this
   exact ⟨fun ⟨s, _, hs⟩ ↦ ⟨s, hs⟩, fun ⟨s, hs⟩ ↦ ⟨s, hs ▸ subset_adjoin _ _, hs⟩⟩
 
+/-- A field is finitely generated if and only if it is essentially of finite type over its prime
+subfield. -/
+theorem _root_.Field.fg_iff_essFiniteType : Field.FG F ↔ Algebra.EssFiniteType (⊥ : Subfield F) F :=
+  Field.fg_iff_fg_top_bot.trans fg_top_iff
+
 end FG
 
 section AdjoinSimple
diff --git a/Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean b/Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
index da6341a6aafb9a..3529d1cd78a178 100644
--- a/Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
+++ b/Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
@@ -673,6 +673,13 @@ theorem fg_iSup {ι : Sort*} [Finite ι] {S : ι → IntermediateField F E} (h :
   simp_rw [← hs, ← adjoin_iUnion]
   exact fg_adjoin_of_finite (Set.finite_iUnion fun _ ↦ Finset.finite_toSet _)
 
+/-- A field is finitely generated if and only if it is finitely generated over its prime
+subfield. -/
+theorem _root_.Field.fg_iff_fg_top_bot :
+    Field.FG F ↔ (⊤ : IntermediateField (⊥ : Subfield F) F).FG := by
+  simp [Field.fg_iff, fg_def, Set.exists_finite_iff_finset,
+    ← toSubfield_inj, Subfield.algebraMap_ofSubfield, Subfield.closure_union]
+
 theorem induction_on_adjoin_finset (S : Finset E) (P : IntermediateField F E → Prop) (base : P ⊥)
     (ih : ∀ (K : IntermediateField F E), ∀ x ∈ S, P K → P (K⟮x⟯.restrictScalars F)) :
     P (adjoin F S) := by