Hermite's theorem on number fields

Stream: mathlib4

[Xavier Roblot]

Let A be an algebraic closure of ℚ and let N ≥ 1 be an integer. A theorem of Hermite states that
there are finitely many number fields in A such that |discr K| ≤ N where discr K denotes
the discriminant of K. I think we have all the tools necessary to add the proof of this result to
mathlib but I am not sure on the best way to state the result. So far, I have the following

import Mathlib.NumberTheory.NumberField.Discriminant

open NumberField

example {A : Type*} [Field A] [CharZero A] [IsAlgClosed A] (N : ℕ) :
    {K : { K : IntermediateField ℚ A // FiniteDimensional ℚ K } |
      haveI :  NumberField K := @NumberField.mk _ _ inferInstance K.prop
      |discr K| ≤ N }.Finite := sorry

Is there a better way to state this theorem?

[Kevin Buzzard]

You don't need A to be algebraically closed.

My guess is that this is fine. Other approaches: consider all number fields up to isomorphism and say that the quotient is finite, or claim the existence of a finite set of fields and say every field with small discriminant is isomorphic to one of these. But my guess is that in applications what you have will be the most useful.

[Xavier Roblot]

Kevin Buzzard said:

You don't need A to be algebraically closed.

Good point.

[Xavier Roblot]

One thing I am not sure about is wether it is better to use IntermediateField ℚ A or Subfield A...

[Kevin Buzzard]

DoesFiniteDimensional \Q A work in both cases? If so then it probably doesn't matter :-)

[Xavier Roblot]

Yes, the rest stays exactly the same.

[Kevin Buzzard]

Usually the logic is to write the thing which the user will find easiest to use, so probably Subfield?