English
Multiplication by a nonzero element a on the right defines a dilation-equivalence of a normed division ring.
Русский
Умножение справа на непустой элемент a образует дилатацию-эквивалентность в нормированном кольце деления.
LaTeX
$$$a \neq 0 \Rightarrow \text{Right-multiplication by } a \text{ defines a dilation-equivalence on } \alpha.$$
Lean4
instance instCompletableTopField : CompletableTopField F
where
t0 := (inferInstanceAs <| T0Space _).t0
nice f hc
hn := by
obtain ⟨δ, δ_pos, hδ⟩ := (disjoint_nhds_zero ..).mp <| disjoint_iff.mpr hn
have f_bdd : f.IsBoundedUnder (· ≤ ·) (‖·⁻¹‖) :=
⟨δ⁻¹, hδ.mono fun y hy ↦ le_inv_of_le_inv₀ δ_pos (by simpa using hy)⟩
have h₀ : ∀ᶠ y in f, y ≠ 0 := hδ.mono fun y hy ↦ by simpa using δ_pos.trans_le hy
have : ∀ᶠ p in f ×ˢ f, p.1⁻¹ - p.2⁻¹ = p.1⁻¹ * (p.2 - p.1) * p.2⁻¹ :=
h₀.prod_mk h₀ |>.mono fun ⟨x, y⟩ ⟨hx, hy⟩ ↦ by simp [mul_sub, sub_mul, hx, hy]
rw [cauchy_iff_tendsto_swapped] at hc
rw [cauchy_map_iff_tendsto, tendsto_congr' this]
refine ⟨hc.1, .zero_mul_isBoundedUnder_le ?_ <| tendsto_snd.isBoundedUnder_comp f_bdd⟩
exact isBoundedUnder_le_mul_tendsto_zero (tendsto_fst.isBoundedUnder_comp f_bdd) hc.2
