exists_coe_eq_v — Mathlib

English

For any x ∈ hat K, there exists r ∈ K with extensionValuation(x) = v(r).

Русский

Для любого x ∈ hat K существует r ∈ K с extensionValuation(x) = v(r).

LaTeX

$$$\exists r \in K\; extensionValuation(x) = v(r)$$$

Lean4

theorem exists_coe_eq_v (x : hat K) : ∃ r : K, extensionValuation x = v r :=
  by
  rcases eq_or_ne x 0 with (rfl | h)
  · use 0
    exact extensionValuation_apply_coe 0
  · refine Completion.denseRange_coe.induction_on x ?_ (by simp)
    simpa [eq_comm] using valuation_isClosedMap.isClosed_range.preimage continuous_extensionValuation

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