lean_workbook_plus_62819

Proved

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

Prove that if $n=p^2$ , then $d=p$ , which means $d - 1 \mid n - 1$ (i.e. $p - 1 \mid p^2 - 1$ ).

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_62819 (n : ℕ) (p : ℕ) (hp : p.Prime) (h : n = p^2) (d : ℕ) (hd : d = p) : d - 1 ∣ n - 1   :=  by sorry

Source