lean_workbook_plus_36698

Proved

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

Since n has exactly 8 natural divisors, $n$ is one of the forms $p^7, pq^3, pqr$ where $p,q,r$ are some primes.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_36698 (n : ℕ) (hn : n > 0) (h : Finset.card (Nat.divisors n) = 8) : ∃ (p q r : ℕ), p.Prime ∧ q.Prime ∧ r.Prime ∧ n = p^7 ∨ n = p*q^3 ∨ n = p*q*r   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph