degree_eq_zero_iff — Mathlib

English

For any f, the degree of f is zero if and only if f equals C(leadingCoeff f).

Русский

Для любого f степень f равна нулю тогда и только тогда, когда f = C(leadingCoeff f).

LaTeX

$$$m.degree f = 0 \iff f = C\bigl(m.leadingCoeff f\bigr)$$$

Lean4

theorem degree_eq_zero_iff {f : MvPolynomial σ R} : m.degree f = 0 ↔ f = C (m.leadingCoeff f) :=
  ⟨MonomialOrder.eq_C_of_degree_eq_zero, fun h => by rw [h, MonomialOrder.degree_C]⟩

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