comp_X_add_C_ne_zero_iff — Mathlib

English

Let p be a polynomial over a commutative ring and t an element of the ring. Then the polynomial obtained by shifting the variable by t, namely p(X + t), is nonzero if and only if p is nonzero.

Русский

Пусть p — полином над коммутативным кольцом и t ∈ R. Тогда полином p(X + t) не равен нулю тогда и только тогда, когда p не нулевой.

LaTeX

$$$ p(X+t) \neq 0 \iff p \neq 0 $$$

Lean4

theorem comp_X_add_C_ne_zero_iff : p.comp (X + C t) ≠ 0 ↔ p ≠ 0 :=
  comp_X_add_C_eq_zero_iff.not

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