Theorems · Theorem · number theory

NumberField.Units.dirichletUnitTheorem.seq_decreasing

∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (w₁ : NumberField.InfinitePlace K) {B : ℕ}
  (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B)
  {n m : ℕ},
  n < m →
    ∀ (w : NumberField.InfinitePlace K),
      w ≠ w₁ →
        w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(NumberField.Units.dirichletUnitTheorem.seq K w₁ hB m)) <
          w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(NumberField.Units.dirichletUnitTheorem.seq K w₁ hB n))

The sequence is strictly decreasing at infinite places distinct from w₁.

Defined in

Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldNumberField