Signum_Function_is_Primitive_Recursive

Proved

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

computabilityprimitive-recursive-functionsproofwiki

Let $\operatorname{sgn}: \N \to \N$ be defined as the signum function. Then $\operatorname{sgn}$ is primitive recursive. $\overline {\operatorname{sgn}}$ is primitive recursive.

Preamble

import Mathlib.Computability.Primrec

Formal statement

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

Source

https://proofwiki.org/wiki/Signum_Function_is_Primitive_Recursive

View graph