not_limZero_const_of_nonzero — Mathlib

English

For any nonzero rational q, the constant sequence with value q under the padic norm is not limZero.

Русский

Для любого ненулевого рационального числа q константная последовательность по p-адической норме не является limZero.

LaTeX

$$∀ q∈ℚ, q ≠ 0 → ¬LimZero (const (padicNorm p) q)$$

Lean4

theorem not_limZero_const_of_nonzero {q : ℚ} (hq : q ≠ 0) : ¬LimZero (const (padicNorm p) q) := fun h' ↦
  hq <| const_limZero.1 h'

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