lean_workbook_plus_76831
ProvedNote that and are the roots of at , where . So those 2 linear polynomials are the factors of . Also, and the and also divide . Thus, all the factors of are also factors of , so itself must divide .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_76831 (x : ℤ) (y : ℤ) (z : ℤ) : (x^2 + x + 1) ∣ (x^7 + x^2 + 1) := by sorry
Source