English
Reiterating the discrete topology result: in a normed division ring with discrete topology, for all x, ||x|| = 1 iff x ≠ 0.
Русский
Повторение результата про дискретную топологию: в нормированном делении кольца с дискретной топологией для любого x выполняется ||x|| = 1 тогда и только тогда, когда x ≠ 0.
LaTeX
$$$\\|x\\| = 1 \iff x \neq 0$$$
Lean4
theorem norm_eq_one_iff_ne_zero_of_discrete {x : 𝕜} : ‖x‖ = 1 ↔ x ≠ 0 :=
by
constructor <;> intro hx
· contrapose! hx
simp [hx]
· have : IsOpen {(0 : 𝕜)} := isOpen_discrete {0}
simp_rw [Metric.isOpen_singleton_iff, dist_eq_norm, sub_zero] at this
obtain ⟨ε, εpos, h'⟩ := this
wlog h : ‖x‖ < 1 generalizing 𝕜 with H
· push_neg at h
rcases h.eq_or_lt with h | h
· rw [h]
replace h := norm_inv x ▸ inv_lt_one_of_one_lt₀ h
rw [← inv_inj, inv_one, ← norm_inv]
exact H (by simpa) h' h
obtain ⟨k, hk⟩ : ∃ k : ℕ, ‖x‖ ^ k < ε := exists_pow_lt_of_lt_one εpos h
rw [← norm_pow] at hk
specialize h' _ hk
simp [hx] at h'
