English
If there exists a nonzero x with ∥x∥ ≠ 1, then the given normed field structure yields a nontrivially normed field.
Русский
Если существует ненулевой элемент x с ∥x∥ ≠ 1, то данная нормаобразующая структура поля даёт ненулевое нормированное поле.
LaTeX
$$$ (\exists x : 𝕜, x \neq 0 \land \|x\| \neq 1) \Rightarrow NontriviallyNormedField 𝕜 $$$
Lean4
/-- A normed field is nontrivially normed
provided that the norm of some nonzero element is not one. -/
def ofNormNeOne {𝕜 : Type*} [h' : NormedField 𝕜] (h : ∃ x : 𝕜, x ≠ 0 ∧ ‖x‖ ≠ 1) : NontriviallyNormedField 𝕜
where
toNormedField := h'
non_trivial := by
rcases h with ⟨x, hx, hx1⟩
rcases hx1.lt_or_gt with hlt | hlt
· use x⁻¹
rw [norm_inv]
exact (one_lt_inv₀ (norm_pos_iff.2 hx)).2 hlt
· exact ⟨x, hlt⟩
