adicAbv_coe_eq_one_iff — Mathlib

English

The v-adic absolute value equals 1 on algebraf maps iff r ∉ v.asIdeal.

Русский

Адическая абсолютная величина равна 1 на образах алгебраических отображений тогда, когда r ∉ v.asIdeal.

LaTeX

$$v.adicAbv hb (algebraMap R K r) = 1 ↔ r ∉ v.asIdeal$$

Lean4

theorem adicAbv_coe_eq_one_iff {b : NNReal} (hb : 1 < b) (r : R) :
    v.adicAbv hb (algebraMap R K r) = 1 ↔ r ∉ v.asIdeal :=
  by
  rw [← not_iff_not, not_not, ← v.adicAbv_coe_lt_one_iff (K := K) hb, ne_iff_lt_iff_le]
  exact adicAbv_coe_le_one v hb r

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