leadingCoeff_eq_one

Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

English

Same principle: if f is monic then leadingCoeff f = 1.

Русский

Та же идея: если f моничен, то leadingCoeff f = 1.

LaTeX

$$$\\ \\; m.leadingCoeff f = 1$ при $m.Monic f$$$

Lean4

@[simp]
theorem leadingCoeff_eq_one {f : MvPolynomial σ R} (hf : m.Monic f) : m.leadingCoeff f = 1 :=
  hf

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

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

Разделы

Аффилиация

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