coeff_one

Mathlib.RingTheory.IsAdjoinRoot

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

English

For a nontrivial S, h.coeff 1 = Pi.single 0 1.

Русский

Для ненулевого S, h.coeff 1 = Pi.single 0 1.

LaTeX

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

Lean4

theorem coeff_one [Nontrivial S] : h.coeff 1 = Pi.single 0 1 := by rw [← h.coeff_root_pow h.deg_pos, pow_zero]

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

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

Разделы

Аффилиация

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