coeff_ne_zero_of_eq_degree

Mathlib.Algebra.Polynomial.Degree.Definitions

URI: https://scilib.ai/kg/mathlib#Polynomial.coeff_ne_zero_of_eq_degree

English

If deg p = n, then coeff p n ≠ 0.

Русский

Если deg p = n, то коэффициент p на n не равен нулю.

LaTeX

$$coeff(p, n) ≠ 0 \\text{ given } degree(p) = n$$

Lean4

theorem coeff_ne_zero_of_eq_degree (hn : degree p = n) : coeff p n ≠ 0 := fun h => mem_support_iff.mp (mem_of_max hn) h

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

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

Разделы

Аффилиация

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