monic_one

Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

English

The constant one is monic with respect to any monomial order.

Русский

Единица как константный полином мононична для любого порядка мономов.

LaTeX

$$$m.Monic (C 1)$$$

Lean4

theorem monic_one : m.Monic (C 1 : MvPolynomial σ R) :=
  monic_monomial_one

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

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

Разделы

Аффилиация

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