coe_toAdjoin_mk_X

Mathlib.RingTheory.AdjoinRoot

URI: https://scilib.ai/kg/mathlib#AdjoinRoot.Minpoly.coe_toAdjoin_mk_X

English

The evaluation sends the class of X to the element x in the target ring: Minpoly.toAdjoin R x (mk (minpoly R x) X) = x.

Русский

Оценка отправляет класс $X$ в элемент $x$: Minpoly.toAdjoin R x (mk (minpoly R x) X) = x.

LaTeX

$$$\text{Minpoly.toAdjoin } R\;x\;\bigl(\mathrm{mk}(\minpoly\;R\;x)\;X\bigr) = x$$$

Lean4

theorem coe_toAdjoin_mk_X : Minpoly.toAdjoin R x (mk (minpoly R x) X) = x := by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru