hatInv — Mathlib

English

The inversion on a field extends to its completion hat K by the uniform-dense embedding; hatInv is defined as the extension of x ↦ x⁻¹ from K to hat K.

Русский

Обратимость на поле распространяется на его окрестность hat K; hatInv — продолжение отображения x ↦ x⁻¹ на hat K.

LaTeX

$$$\hatInv : \hat K \to \hat K \\ hatInv = \mathrm{isDenseInducing\_coe}.extend(\lambda x: (x^{-1}) ).$$$

Lean4

/-- extension of inversion to the completion of a field. -/
def hatInv : hat K → hat K :=
  isDenseInducing_coe.extend fun x : K => (↑x⁻¹ : hat K)

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