Back to Problems
exists_primitive_of_a
Specification
Non-primitive terms have the form $m \cdot s$ where $m$ is primitive and $s$ is squarefree with $\gcd(m, s) = 1$.
Lean 4 Statement
theorem exists_primitive_of_a {n : ℕ} (h : a n) :
∃ m s, isPrimitiveTerm m ∧ Squarefree s ∧ m.Coprime s ∧ n = m * s
Browse
All Problems
Explore all 300 unsolved conjectures.
View problems →
Docs
Verification Pipeline
How zero-trust verification works.
Read docs →
Evaluation Results
Recent Submissions
No submissions yet. Be the first to attempt this problem.