English
For fixed N, the set of number fields K with a complex place and |discr K| ≤ N is finite.
Русский
Для фиксированного N множество полей K с комплексным местом и |дискр K| ≤ N конечно.
LaTeX
$$$$\\{K : {\\mathbb{Q} \\text{-field} \\mid |\\operatorname{discr} K| \\le N, \\; \\text{Complex place exists} \\} \\}.\\text{Finite}$$$$
Lean4
/-- **Hermite Theorem**. Let `N` be an integer. There are only finitely many number fields
(in some fixed extension of `ℚ`) of discriminant bounded by `N`. -/
theorem _root_.NumberField.finite_of_discr_bdd :
{K : { F : IntermediateField ℚ A // FiniteDimensional ℚ F } |
haveI : NumberField K := @NumberField.mk _ _ inferInstance K.prop
|discr K| ≤ N}.Finite :=
by
refine
Set.Finite.subset (Set.Finite.union (finite_of_discr_bdd_of_isReal A N) (finite_of_discr_bdd_of_isComplex A N)) ?_
rintro ⟨K, hK₀⟩ hK₁
have : CharZero K := SubsemiringClass.instCharZero K
haveI : NumberField K := @NumberField.mk _ _ inferInstance hK₀
obtain ⟨w₀⟩ := (inferInstance : Nonempty (InfinitePlace K))
by_cases hw₀ : IsReal w₀
· apply Set.mem_union_left
exact ⟨⟨w₀, hw₀⟩, hK₁⟩
· apply Set.mem_union_right
exact ⟨⟨w₀, not_isReal_iff_isComplex.mp hw₀⟩, hK₁⟩
