Theorems · Theorem · number theory

NumberField.Embeddings.coeff_bdd_of_norm_le

∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {A : Type u_2} [inst_2 : NormedField A] [IsAlgClosed A]
  [NormedAlgebra ℚ A] {B : ℝ} {x : K},
  (∀ (φ : K →+* A), ‖φ x‖ ≤ B) →
    ∀ (i : ℕ),
      ‖(minpoly ℚ x).coeff i‖ ≤ max B 1 ^ Module.finrank ℚ K * ↑((Module.finrank ℚ K).choose (Module.finrank ℚ K / 2))

Defined in

Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings

Cited by

3 results in Mathlib

Foundations

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

Assumes

FieldNumberFieldNormedFieldIsAlgClosedNormedAlgebra