seq_ne_zero — Mathlib

English

All terms of the constructed sequence are nonzero when viewed as elements of the number field: each seq n is a nonzero algebraic integer lifted to K.

Русский

Все члены последовательности не равны нулю; каждая последовательность seq n является ненулевым алгебраическим целым из K.

LaTeX

$$$\forall n:\; (seq\; K\; w_1\; h_B\; n) \neq 0$$$

Lean4

/-- The terms of the sequence are nonzero. -/
theorem seq_ne_zero (n : ℕ) : algebraMap (𝓞 K) K (seq K w₁ hB n) ≠ 0 :=
  RingOfIntegers.coe_ne_zero_iff.mpr (seq K w₁ hB n).prop

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