modByMonicHom_root

Mathlib.RingTheory.IsAdjoinRoot

URI: https://scilib.ai/kg/mathlib#IsAdjoinRootMonic.modByMonicHom_root

English

If 1 < natDegree f, then h.modByMonicHom h.root = X.

Русский

Если 1 < natDegree f, то h.modByMonicHom h.root = X.

LaTeX

$$$ h.modByMonicHom h.root = X $$$

Lean4

@[simp]
theorem modByMonicHom_root (hdeg : 1 < natDegree f) : h.modByMonicHom h.root = X := by
  simpa using modByMonicHom_root_pow h hdeg

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

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

Разделы

Аффилиация

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