The complete divisor set of a semiprime

Proved

WorkbookSource.plus_7645

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Find the divisors of the number $n$ when $n=pq$ and $p, q$ are distinct primes.

Source: InternLM Lean-Workbook, record lean_workbook_plus_7645 (Apache-2.0). The complete source proposition and its explicit variable declarations are preserved.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.plus_7645 (n : ℕ) (p q : ℕ) (hp : p.Prime) (hq : q.Prime) (hpq : p ≠ q) (hn : n = p*q) : {d | d ∣ n} = {1, p, q, p*q}   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_plus_7645; Apache-2.0

View graph