Set_Containing_Only_Zero_is_Primitive_Recursive
Provedcomputabilityprimitive-recursive-functionsproofwiki
The subset is primitive recursive.
Preamble
import Mathlib.Computability.Primrec
Formal statement
theorem Set_Containing_Only_Zero_is_Primitive_Recursive : Nat.Primrec (fun n => if n = 0 then 1 else 0) := by sorry
Source