English
Let v be a valuation on a field F with valuation ring O. For any x in O, if the image of x under the algebra map O → F has valuation 1, then x is a unit in O.
Русский
Пусть v — нормирование на поле F с кольцом целых O. Для любого x ∈ O, если значение v(алгебраMap(O, F)(x)) равно 1, то x является единицей в O.
LaTeX
$$$v(\mathrm{algebraMap}(O,F)(x)) = 1 \Rightarrow x \in O^{\times}$$$
Lean4
/-- This is the special case of `Valuation.Integers.isUnit_of_one` when the valuation is defined
over a field. Let `v` be a valuation on some field `F` and `O` be its integers. For every element
`x` in `O`, `x` is a unit in `O` if and only if the image of `x` in `F` has valuation 1.
-/
theorem isUnit_of_one' (hv : Integers v O) {x : O} (hvx : v (algebraMap O F x) = 1) : IsUnit x :=
by
refine isUnit_of_one hv (IsUnit.mk0 _ ?_) hvx
simp only [← v.ne_zero_iff, hvx, ne_eq, one_ne_zero, not_false_eq_true]
