Prime_Number_has_4_Integral_Divisors

Proved

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

prime-numbersproofwiki

An integer p is prime iff it has exactly four integral divisors: 1, -1, p, -p.

Preamble

import Mathlib.Data.Int.GCD
import Mathlib.RingTheory.Int.Basic

Formal statement

theorem Prime_Number_has_4_Integral_Divisors (p : ℤ) (hp : Prime p) : {d : ℤ | d ∣ p} = {1, -1, p, -p} := by sorry

Source