eq_C_of_degree_eq_zero — Mathlib

English

If the degree of f is zero, then f equals a scalar constant C(leadingCoeff f).

Русский

Если степень f равна нулю, то f = C(leadingCoeff f).

LaTeX

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

Lean4

theorem eq_C_of_degree_eq_zero {f : MvPolynomial σ R} (hf : m.degree f = 0) : f = C (m.leadingCoeff f) :=
  by
  ext d
  simp only [leadingCoeff, hf]
  classical
  by_cases hd : d = 0
  · simp [hd]
  · rw [coeff_C, if_neg (Ne.symm hd)]
    apply coeff_eq_zero_of_lt (m := m)
    rw [hf, map_zero, lt_iff_le_and_ne, ne_eq, eq_comm, EmbeddingLike.map_eq_zero_iff]
    exact ⟨bot_le, hd⟩

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