Divisor_Counting_Function_is_Primitive_Recursive
Provedcomputabilitydivisibilityprimitive-recursive-functionsproofwiki
The divisor counting () function is primitive recursive.
Preamble
import Mathlib.Computability.Primrec import Mathlib.NumberTheory.Divisors
Formal statement
theorem Divisor_Counting_Function_is_Primitive_Recursive : Nat.Primrec (fun n => Nat.divisors n |>.card) := by sorry
Source