coe_algEquivOfEq

Mathlib.RingTheory.AdjoinRoot

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

English

For associated f g, the underlying map of algEquivOfAssociated is the same as algHomOfDvd under hfg.

Русский

Для ассоциированных f и g основанное отображение algEquivOfAssociated то же, что и algHomOfDvd при hfg.

LaTeX

$$coe_algEquivOfAssociated f g hfg = algHomOfDvd f g hfg$$

Lean4

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

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

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

Разделы

Аффилиация

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