mapRingEquiv_apply — Mathlib

English

For a ring isomorphism e: K ≃+* L and x ∈ 𝓞 K, the image under mapRingEquiv e coincides with applying e to x considered as an element of K.

Русский

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

LaTeX

$$$(mapRingEquiv\, e\, x : L) = e(x)$$$

Lean4

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

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