adicAbv_coe_lt_one_iff — Mathlib

English

For hb > 1, v.adicAbv hb (algebraMap R K r) < 1 iff r ∈ v.asIdeal.

Русский

Для hb > 1, v.adicAbv hb (algebraMap R K r) < 1 тогда и только тогда, когда r ∈ v.asIdeal.

LaTeX

$$v.adicAbv hb (algebraMap R K r) < 1 ↔ r ∈ v.asIdeal$$

Lean4

theorem adicAbv_coe_lt_one_iff {b : NNReal} (hb : 1 < b) (r : R) :
    v.adicAbv hb (algebraMap R K r) < 1 ↔ r ∈ v.asIdeal := by
  simpa [adicAbv, adicAbvDef, toNNReal_lt_one_iff hb] using valuation_lt_one_iff_mem v r

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