coeff_mul_of_degree_add

Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

← MathLib Explorer

English

For all f, deg f = 0 iff totalDegree f = 0.

Русский

Для всякого f: deg f = 0 ⇔ totalDegree f = 0.

LaTeX

$$$m.degree f = 0 \iff f.totalDegree = 0$$$

Lean4

/-- Multiplicativity of leading coefficients -/
theorem coeff_mul_of_degree_add {f g : MvPolynomial σ R} :
    (f * g).coeff (m.degree f + m.degree g) = m.leadingCoeff f * m.leadingCoeff g :=
  coeff_mul_of_add_of_degree_le (le_of_eq rfl) (le_of_eq rfl)

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

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

Разделы

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

Аффилиация

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