English
If x is irrational and p is a nonzero polynomial with integer coefficients with x as a root, then the degree of p is greater than 1.
Русский
Если x иррационально и p — не ноль многочлен с целыми коэффициентами, удовлетворяющий p(x)=0, то степень p больше единицы.
LaTeX
$$$x \in \mathbb{R},\; p \in \mathbb{Z}[X],\; p \neq 0,\; \operatorname{aeval}(x,p)=0 \Rightarrow 1 < \operatorname{natDegree}(p)$$$
Lean4
theorem one_lt_natDegree_of_irrational_root (hx : Irrational x) (p_nonzero : p ≠ 0) (x_is_root : aeval x p = 0) :
1 < p.natDegree := by
by_contra rid
rcases exists_eq_X_add_C_of_natDegree_le_one (not_lt.1 rid) with ⟨a, b, rfl⟩
clear rid
have : (a : ℝ) * x = -b := by simpa [eq_neg_iff_add_eq_zero] using x_is_root
rcases em (a = 0) with (rfl | ha)
· obtain rfl : b = 0 := by simpa
simp at p_nonzero
· rw [mul_comm, ← eq_div_iff_mul_eq, eq_comm] at this
· refine hx ⟨-b / a, ?_⟩
assumption_mod_cast
· assumption_mod_cast
