Set_of_Non_Zero_Natural_Numbers_is_Primitive_Recursive

Proved

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

computabilityprimitive-recursive-functionsproofwiki

Let $\N^*$ be defined as $\N^* = \N \setminus \left\{{0}\right\}$ . The subset $\N^* \subset \N$ is primitive recursive.

Preamble

import Mathlib.Computability.Primrec

Formal statement

theorem Set_of_Non_Zero_Natural_Numbers_is_Primitive_Recursive : Nat.Primrec (fun n => if n = 0 then 0 else 1) := by sorry

Source