English
Let x,y,r,s ∈ K with y ≠ 0, r ≠ 0, s ≠ 0. If v(x − y) < min((v(s)/v(r)) · (v(y))², v(y)), then v(x⁻¹ − y⁻¹) · v(r) < v(s).
Русский
Пусть x,y,r,s ∈ K такие, что y ≠ 0, r ≠ 0, s ≠ 0. Если v(x − y) < min((v(s)/v(r)) · (v(y))², v(y)), тогда v(x⁻¹ − y⁻¹) · v(r) < v(s).
LaTeX
$$$\forall x,y,r,s \in K\;\big(y \neq 0 \wedge r \neq 0 \wedge s \neq 0\big) \,\Rightarrow\; v(x-y) < \min\Big( (v(s)/v(r)) \cdot (v(y) \cdot v(y)), v(y) \Big) \Rightarrow v(x^{-1}-y^{-1}) \cdot v(r) < v(s)$$$
Lean4
theorem inversion_estimate' {x y r s : K} (y_ne : y ≠ 0) (hr : r ≠ 0) (hs : s ≠ 0)
(h : v (x - y) < min ((v s / v r) * (v y * v y)) (v y)) : v (x⁻¹ - y⁻¹) * v r < v s :=
by
have hr' : 0 < v r := by simp [zero_lt_iff, hr]
let γ : Γ₀ˣ := .mk0 (v s / v r) (by simp [hs, hr])
calc
v (x⁻¹ - y⁻¹) * v r < γ * v r := by gcongr; exact Valuation.inversion_estimate v y_ne h
_ = v s := div_mul_cancel₀ _ (by simpa)
