adjoinRootAlgEquiv_apply_mk

Mathlib.RingTheory.IsAdjoinRoot

URI: https://scilib.ai/kg/mathlib#IsAdjoinRoot.adjoinRootAlgEquiv_apply_mk

English

For any g in R[X], the canonical isomorphism sends AdjoinRoot.mk f g to h.map g.

Русский

Для произвольного g в R[X] канонический изоморфизм отправляет AdjoinRoot.mk f g в h.map g.

LaTeX

$$$h.adjoinRootAlgEquiv(\operatorname{AdjoinRoot.mk} f\, g) = h.map\, g$$$

Lean4

@[simp]
theorem adjoinRootAlgEquiv_apply_mk (g : R[X]) : h.adjoinRootAlgEquiv (AdjoinRoot.mk f g) = h.map g :=
  rfl

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

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

Разделы

Аффилиация

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