decidable

Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

English

If a polynomial f is monic with respect to m, then its leading coefficient is 1.

Русский

Если полином f моничен по порядку m, то его старшая коэффициент равен 1.

LaTeX

$$$\\text{hf}: m.Monic f \\Rightarrow m.leadingCoeff f = 1$$$

Lean4

instance decidable [DecidableEq R] (f : MvPolynomial σ R) : Decidable (m.Monic f) := by unfold Monic; infer_instance

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

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

Разделы

Аффилиация

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