lean_workbook_plus_64978

Proved

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

Prove that for an arbitrary prime number $p$ , $f(x)\equiv 0\pmod{p}$ has a solution, where $f(x)=x^6-11x^4+36x^2-36$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_64978 (p : ℕ) (hp : p.Prime) : ∃ x : ℕ, (x^6 - 11 * x^4 + 36 * x^2 - 36) % p = 0   :=  by sorry

Source