coe_inv — Mathlib

English

The inverse in the completion respects the embedding of the base field: for any x in K, (x : hat K)^{-1} equals ((x^{-1}) : hat K).

Русский

Обратное в дополнении согласуется с вложением: (x : hat K)^{-1} = ((x^{-1} : K) : hat K).

LaTeX

$$$ (x : \hat K)^{-1} = ((x^{-1} : K) : \hat K) $$$

Lean4

@[norm_cast]
theorem coe_inv (x : K) : (x : hat K)⁻¹ = ((x⁻¹ : K) : hat K) :=
  by
  by_cases h : x = 0
  · rw [h, inv_zero]
    dsimp [Inv.inv]
    norm_cast
    simp
  · conv_lhs => dsimp [Inv.inv]
    rw [if_neg]
    · exact hatInv_extends h
    · exact fun H => h (isDenseEmbedding_coe.injective H)

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