coeff_degree_eq_zero_iff

Mathlib.RingTheory.MvPolynomial.MonomialOrder

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

English

The coefficient at the degree of f vanishes if and only if f = 0.

Русский

Коэффициент при степени f равен нулю тогда и только тогда, когда f = 0.

LaTeX

$$$f_{m.degree f} = 0 \iff f = 0$$$

Lean4

@[simp]
theorem coeff_degree_eq_zero_iff {f : MvPolynomial σ R} : f.coeff (m.degree f) = 0 ↔ f = 0 :=
  m.leadingCoeff_eq_zero_iff

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

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

Разделы

Аффилиация

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