Theorems · Theorem · number theory

NumberField.Embeddings.finite_of_norm_le

∀ (K : Type u_1) [inst : Field K] [NumberField K] (A : Type u_2) [inst_2 : NormedField A] [IsAlgClosed A]
  [NormedAlgebra ℚ A] (B : ℝ), {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ B}.Finite

Let B be a real number. The set of algebraic integers in K whose conjugates are all smaller in norm than B is finite.

Defined in

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Cited by

4 results in Mathlib

Foundations

Depth 161 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldNumberFieldNormedFieldIsAlgClosedNormedAlgebra