Monic

Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

Lean4

/-- A multivariate polynomial is `Monic` with respect to a monomial order
if its leading coefficient (for that monomial order) is 1. -/
def Monic (f : MvPolynomial σ R) : Prop :=
  m.leadingCoeff f = 1

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

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

Разделы

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

Аффилиация

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