hatInv_extends — Mathlib

English

If x is a nonzero element of the base field K, then the inverse in the completion hat K agrees with the embedding of the inverse in K: hatInv(x) = x^{-1} as an element of hat K.

Русский

Если x ≠ 0 в K, то обратное в дополнении hat K совпадает с вложением x^{-1} в hat K: hatInv(x) = x^{-1}.

LaTeX

$$$\hatInv (x : \hat K) = (x^{-1} : \hat K) \quad (x \neq 0)$$$

Lean4

theorem hatInv_extends {x : K} (h : x ≠ 0) : hatInv (x : hat K) = ↑(x⁻¹ : K) :=
  isDenseInducing_coe.extend_eq_at ((continuous_coe K).continuousAt.comp (continuousAt_inv₀ h))

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