leadingCoeff_eq

Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree

URI: https://scilib.ai/kg/mathlib#Polynomial.IsMonicOfDegree.leadingCoeff_eq

English

If p is monic of degree n, then the leading coefficient of p is 1.

Русский

Если p мономичен степени n, то его ведущий коэффициент равен 1.

LaTeX

$$$IsMonicOfDegree(p, n) \\Rightarrow p.leadingCoeff = 1$$$

Lean4

theorem leadingCoeff_eq {p : R[X]} {n : ℕ} (hp : IsMonicOfDegree p n) : p.leadingCoeff = 1 :=
  Monic.def.mp hp.monic

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

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

Разделы

Аффилиация

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