isUnit_iff_valuation_eq_one — Mathlib

English

For every x in O, x is a unit in O if and only if the image of x under the algebra map O → F has valuation 1.

Русский

Для любого x ∈ O выполняется: x — единица в O тогда и только тогда, когда v(алгебраMap(O, F)(x)) = 1.

LaTeX

$$$x \in O^{\times} \;\Leftrightarrow\; v(\mathrm{algebraMap}(O,F)(x)) = 1$$$

Lean4

theorem isUnit_iff_valuation_eq_one (hv : Integers v O) {x : O} : IsUnit x ↔ v (algebraMap O F x) = 1 :=
  ⟨hv.one_of_isUnit, hv.isUnit_of_one'⟩

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