seq — Mathlib

English

There exists a unit u in the ring of integers 𝓞_K such that, for every infinite place w different from w1, the logarithm of w applied to u is strictly negative: log w(u) < 0.

Русский

Существует единица u в кольце целых чисел 𝓞_K такая, что для любого бесконечного места w, не равного w1, выполняется log w(u) < 0.

LaTeX

$$$\exists u \in (\mathcal{O}_K)^{\times},\; \forall w \neq w_1:\; \log w(u) < 0$$$

Lean4

/-- 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`. -/
def seq : ℕ → { x : 𝓞 K // x ≠ 0 }
  | 0 => ⟨1, by simp⟩
  | n + 1 => ⟨(seq_next K w₁ hB (seq n).prop).choose, (seq_next K w₁ hB (seq n).prop).choose_spec.1⟩

Похожие утверждения