Prove2Me

lean_workbook_plus_56991

Proved

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

Suppose yy is a positive integer. If pp is a prime and p∣y2p|y^2 , then p∣yp|y .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_56991 (p y : ℕ) (hp : p.Prime) (h : p ∣ y^2) : p ∣ y   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph