Prime_Exponent_Function_is_Primitive_Recursive

Proved

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

computabilityprimitive-recursive-functionsproofwiki

Let $n \in \N$ be a natural number. Let $\left({n, j}\right): \N^2 \to \N$ be defined as $\left({n, j}\right) = \left({n}\right)_j$ where $\left({n}\right)_j$ is the prime exponent function. Then $\left({n, j}\right)$ is primitive recursive.

Preamble

import Mathlib.Computability.Primrec
import Mathlib.Data.Nat.Factorization.Basic

Formal statement

theorem Prime_Exponent_Function_is_Primitive_Recursive : Primrec₂ (fun (n j : ℕ) => n.factorization j) := by sorry

Source

https://proofwiki.org/wiki/Prime_Exponent_Function_is_Primitive_Recursive

View graph