equivAdjoin_toAlgHom — Mathlib

English

Let R ⊆ S be commutative rings, x ∈ S integral over R. Then the R-algebra generated by x, Adjoin_R({x}), is canonically isomorphic to the R-algebra Minpoly.toAdjoin R x, via the natural isomorphism that sends the adjoined root to x.

Русский

Пусть R и S — коммутативные кольца, x ∈ S интегрален над R. Тогда R-алгебра, порождаемая x, Adjoin_R({x}), канонически изоморфна R-алгебре Minpoly.toAdjoin R x, причём образ корня при этом отображении соответствует x.

LaTeX

$$$Adjoin_R\\bigl(\\{x\\}\\bigr) \\cong_R Minpoly.toAdjoin R x$$$

Lean4

@[simp]
theorem equivAdjoin_toAlgHom (hx : IsIntegral R x) : equivAdjoin hx = Minpoly.toAdjoin R x :=
  rfl

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