mapRingEquiv — Mathlib

English

The canonical mapRingEquiv maps a ring isomorphism e: K ≃+* L to a ring isomorphism between their rings of integers 𝓞K and 𝓞L by restricting e.

Русский

Каноническая mapRingEquiv переводит кольцо изоморфизм e: K ≃+* L в изоморфизм между кольцами целых 𝓞K и 𝓞L путём ограничения e.

LaTeX

$$$\\mathrm{mapRingEquiv}(e): \\mathcal{O}_K \\cong+* \\mathcal{O}_L$$$

Lean4

/-- The ring isomorphism `(𝓞 K) ≃+* (𝓞 L)` given by restricting
  a ring isomorphism `e : K ≃+* L` to `𝓞 K`. -/
def mapRingEquiv {K L : Type*} [Field K] [Field L] (e : K ≃+* L) : (𝓞 K) ≃+* (𝓞 L) :=
  RingEquiv.ofRingHom (mapRingHom e) (mapRingHom e.symm) (RingHom.ext fun x => ext (EquivLike.right_inv e x.1))
    (RingHom.ext fun x => ext (EquivLike.left_inv e x.1))

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