Theorems · Definition · number theory

NumberField.Units.dirichletUnitTheorem.seq

(K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      NumberField.InfinitePlace K →
        {B : ℕ} →
          NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B →
            ℕ → { x // x ≠ 0 }

An infinite sequence of nonzero algebraic integers of K satisfying the following properties: • seq n is nonzero; • for w : InfinitePlace K, w ≠ w₁ → w (seq n + 1) < w (seq n); • ∣norm (seq n)∣ ≤ B.

Defined in

Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Cited by

6 results in Mathlib

Foundations

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

Assumes

FieldNumberField