coe_algEquivOfAssociated

Mathlib.RingTheory.AdjoinRoot

URI: https://scilib.ai/kg/mathlib#AdjoinRoot.coe_algEquivOfAssociated

English

If ϕ: AdjoinRoot f →ₐ[R] S, then aeval (ϕ(root f)) f = 0.

Русский

Если ϕ — алгеброморф, то aeval (ϕ(root f)) f = 0.

LaTeX

$$$\\mathrm{aeval}(\\ϕ(\\mathrm{root} f)) f = 0$$$

Lean4

theorem coe_algEquivOfAssociated (f g : R[X]) (hfg) : ⇑(algEquivOfAssociated f g hfg) = algHomOfDvd f g hfg.symm.dvd :=
  rfl

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

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

Разделы

Аффилиация

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