X_pow_add_C_ne_one — Mathlib

English

For every n > 0 and every a in R, the polynomial X^n + C(a) is not equal to the constant polynomial 1.

Русский

Для любого n > 0 и любого a в R многочлен X^n + C(a) не равен константному полиному 1.

LaTeX

$$$0 < n \rightarrow (X^n + C a) \neq 1$$$

Lean4

theorem X_pow_add_C_ne_one {n : ℕ} (hn : 0 < n) (a : R) : (X : R[X]) ^ n + C a ≠ 1 := fun h =>
  hn.ne' <| by simpa only [natDegree_X_pow_add_C, natDegree_one] using congr_arg natDegree h

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