English
If the valuation is rank one, the induced normed field structure on L is nontrivial; in particular there exists x ≠ 0 with ‖x‖ ≠ 1.
Русский
Если ранговая оценка равна единице, полученная нордифицированная структура поля на L не тривиальна; существует x ≠ 0 такое, что ‖x‖ ≠ 1.
LaTeX
$$$\exists x\in L\setminus\{0\},\|x\| \neq 1$$$
Lean4
/-- The nontrivially normed field structure determined by a rank one valuation.
-/
def toNontriviallyNormedField : NontriviallyNormedField L :=
{ val.toNormedField with
non_trivial := by
obtain ⟨x, hx⟩ := Valuation.RankOne.nontrivial val.v
rcases Valuation.val_le_one_or_val_inv_le_one val.v x with h | h
· use x⁻¹
simp only [toNormedField.one_lt_norm_iff, map_inv₀, one_lt_inv₀ (zero_lt_iff.mpr hx.1), lt_of_le_of_ne h hx.2]
· use x
simp only [map_inv₀, inv_le_one₀ <| zero_lt_iff.mpr hx.1] at h
simp only [toNormedField.one_lt_norm_iff, lt_of_le_of_ne h hx.2.symm] }
