algEquivOfEq_toAlgHom

Mathlib.RingTheory.AdjoinRoot

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

English

The underlying map of algEquivOfEq f g hfg is algHomOfDvd f g hfg.symm.dvd.

Русский

Основанное отображение algEquivOfEq f g hfg равно algHomOfDvd f g hfg.symm.dvd.

LaTeX

$$coe_algEquivOfEq f g hfg = algHomOfDvd f g hfg.symm.dvd$$

Lean4

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

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

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

Разделы

Аффилиация

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