mapEquiv — Mathlib

English

If e: R ≃+* S is a ring isomorphism, then the induced map on polynomial rings yields an isomorphism R[X] ≃+* S[X].

Русский

Если e: R ≃+* S — изоморфизм колец, то индуцированное отображение между кольцевыми полиномами задаёт изоморфизм R[X] ≃+* S[X].

LaTeX

$$$\\text{mapEquiv}(e):\\ R[X] \\cong S[X]$$$

Lean4

/-- If `R` and `S` are isomorphic, then so are their polynomial rings. -/
@[simps!]
def mapEquiv (e : R ≃+* S) : R[X] ≃+* S[X] :=
  RingEquiv.ofHomInv (mapRingHom (e : R →+* S)) (mapRingHom (e.symm : S →+* R)) (by ext; simp) (by ext; simp)

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