English
The set of algebraic integers in K whose conjugates have norm at most B is finite.
Русский
Множество алгебрически целых чисел x∈K, чьи сопряжённые имеют норму не более B, конечное.
LaTeX
$${x ∈ K | IsIntegral ℤ x ∧ ∀ φ : K →+* A, ∥φ x∥ ≤ B}. Finite$$
Lean4
/-- Let `B` be a real number. The set of algebraic integers in `K` whose conjugates are all
smaller in norm than `B` is finite. -/
theorem finite_of_norm_le (B : ℝ) : {x : K | IsIntegral ℤ x ∧ ∀ φ : K →+* A, ‖φ x‖ ≤ B}.Finite := by
classical
let C := Nat.ceil (max B 1 ^ finrank ℚ K * (finrank ℚ K).choose (finrank ℚ K / 2))
have := bUnion_roots_finite (algebraMap ℤ K) (finrank ℚ K) (finite_Icc (-C : ℤ) C)
refine this.subset fun x hx => ?_; simp_rw [mem_iUnion]
have h_map_ℚ_minpoly := minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hx.1
refine ⟨_, ⟨?_, fun i => ?_⟩, mem_rootSet.2 ⟨minpoly.ne_zero hx.1, minpoly.aeval ℤ x⟩⟩
· rw [← (minpoly.monic hx.1).natDegree_map (algebraMap ℤ ℚ), ← h_map_ℚ_minpoly]
exact minpoly.natDegree_le x
rw [mem_Icc, ← abs_le, ← @Int.cast_le ℝ]
refine (Eq.trans_le ?_ <| coeff_bdd_of_norm_le hx.2 i).trans (Nat.le_ceil _)
rw [h_map_ℚ_minpoly, coeff_map, eq_intCast, Int.norm_cast_rat, Int.norm_eq_abs, Int.cast_abs]
