closure_coe_completion_v_mul_v_lt

English

If r,s ∈ K with r ≠ 0, s ≠ 0, then closure of { x ∈ K | v(x)·v(r) < v(s) } equals { x ∈ hat K | extensionValuation(x)·v(r) < v(s) }.

Русский

Если r, s ∈ K и r ≠ 0, s ≠ 0, то замыкание { x | v(x)·v(r) < v(s) } в hat K даёт { x | extensionValuation(x)·v(r) < v(s) }.

LaTeX

$$$\forall r,s\in K\ (r \neq 0 \land s \neq 0)\; closure( { x ∈ K \mid v(x) \cdot v(r) < v(s) } ) = { x ∈ \hat{K} \mid extensionValuation(x) \cdot v(r) < v(s) }$$$

Lean4

theorem closure_coe_completion_v_mul_v_lt {r s : K} (hr : r ≠ 0) (hs : s ≠ 0) :
    closure ((↑) '' {x : K | v x * v r < v s}) = {x : hat K | extensionValuation x * v r < v s} :=
  by
  have hrs : v s / v r ≠ 0 := by simp [hr, hs]
  convert closure_coe_completion_v_lt (γ := .mk0 _ hrs) using 3
  all_goals simp [← lt_div_iff₀, zero_lt_iff, hr]

Похожие утверждения