degree_one

Mathlib.RingTheory.MvPolynomial.MonomialOrder

URI: https://scilib.ai/kg/mathlib#MonomialOrder.degree_one

← MathLib Explorer

English

The leading coefficient of a monomial m is precisely the coefficient c.

Русский

Старший коэффициент монома равен его коэффициенту c.

LaTeX

$$$m.leadingCoeff(\\text{monomial } d c) = c$$$

Lean4

@[simp]
theorem degree_one : m.degree (1 : MvPolynomial σ R) = 0 :=
  by
  nontriviality R
  classical rw [MvPolynomial.one_def, degree_monomial]
  simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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