coe_equivAdjoin — Mathlib

English

Let hx be as above. The underlying map of the isomorphism between Adjoin_R({x}) and Minpoly.toAdjoin R x is exactly the natural map sending the root to x.

Русский

Пусть hx как выше. Подлежащий отображению изоморфизма между Adjoin_R({x}) и Minpoly.toAdjoin R x является естественное отображение, отправляющее корень в x.

LaTeX

$$$Adjoin_R\\bigl(\\{x\\}\\bigr) \\cong_R Minpoly.toAdjoin R x\\; \\text{(underlying map sends the root to } x\\text{)}$$$

Lean4

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

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