divX_eq_zero_iff — Mathlib

English

Let p be a polynomial over a semiring R. Then divX p = 0 if and only if p is a constant polynomial, i.e. p = C(p0) where p0 is the constant term of p.

Русский

Пусть p — полином над полем R. Тогда divX p = 0 тогда и только тогда, когда p является константным полиномом, то есть p = C(p0), где p0 — постоянный коэффициент p.

LaTeX

$$$ \\operatorname{divX}(p) = 0 \\iff p = C\\bigl(p_0\\bigr), \\quad p_0 = \\operatorname{coeff}_0(p). $$$

Lean4

theorem divX_eq_zero_iff : divX p = 0 ↔ p = C (p.coeff 0) :=
  ⟨fun h => by simpa [eq_comm, h] using divX_mul_X_add p, fun h => by rw [h, divX_C]⟩

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