notMem_adicCompletionIntegers — Mathlib

English

The complement membership in adic completion integers corresponds to strict inequality 1 < valuation.

Русский

Принадлежность/не принадлежность к целочисленному подкольрцу завершения по адической норме соответствует строгому неравенству 1 < valuation.

LaTeX

$$notMem_adicCompletionIntegers$$

Lean4

theorem notMem_adicCompletionIntegers {x : v.adicCompletion K} : x ∉ v.adicCompletionIntegers K ↔ 1 < Valued.v x :=
  by
  rw [not_congr <| mem_adicCompletionIntegers R K v]
  exact not_le

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