mapRingEquiv_symm_apply — Mathlib

English

For a ring isomorphism e: K ≃+* L and x ∈ 𝓞 L, the image under the inverse mapRingEquiv(e) equals applying e.symm to x viewed in L.

Русский

Для изоморфизма e: K ≃+* L и x ∈ 𝓞 L образ через обратную mapRingEquiv(e) равен применению e.symm к x, взятому в L.

LaTeX

$$$((mapRingEquiv e).symm x : K) = e^{-1}(x)$$$

Lean4

@[simp]
theorem mapRingEquiv_symm_apply {K L : Type*} [Field K] [Field L] (e : K ≃+* L) (x : 𝓞 L) :
    ((mapRingEquiv e).symm x : K) = e.symm (x : L) :=
  rfl

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