coeff_root

Mathlib.RingTheory.IsAdjoinRoot

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

English

If 1 < natDegree f, then h.coeff h.root = Pi.single 1 1.

Русский

Если 1 < natDegree f, тогда h.coeff h.root = Pi.single 1 1.

LaTeX

$$$ h.coeff\\, h.root = \\Pi.single\\ 1\\ 1 $$$

Lean4

theorem coeff_root (hdeg : 1 < natDegree f) : h.coeff h.root = Pi.single 1 1 := by rw [← h.coeff_root_pow hdeg, pow_one]

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

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

Разделы

Аффилиация

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