lean_workbook_plus_63668

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

In $\mathbb{F}_p[x]$ , is it true that $x+p-1\mid x^2+p-1$ ?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_63668 (p : ℕ) (hp : p.Prime) (F : Type*) [Field F]
  [CharP F p] (x : F) : (x + p - 1) ∣ (x^2 + p - 1)   :=  by sorry

Source