coeff_degree

Mathlib.RingTheory.MvPolynomial.MonomialOrder

URI: https://scilib.ai/kg/mathlib#MonomialOrder.Monic.coeff_degree

English

If f is monic, the coefficient of the degree m.degree f in f equals 1.

Русский

Если f моничен, коэффициент при степени m.degree f в f равен 1.

LaTeX

$$$f$ мононич → $f.coeff( m.degree f) = 1$$$

Lean4

theorem coeff_degree {f : MvPolynomial σ R} (hf : m.Monic f) : f.coeff (m.degree f) = 1 :=
  hf

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

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

Разделы

Аффилиация

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