Equality_Relation_is_Primitive_Recursive

Proved

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

computabilityprimitive-recursive-functionsproofwiki

The relation $\operatorname{eq} \subseteq \N^2$ , defined as $\map {\operatorname {eq} } {n, m} \iff n = m$ is primitive recursive.

Preamble

import Mathlib.Computability.Primrec

Formal statement

theorem Equality_Relation_is_Primitive_Recursive : PrimrecRel (fun (a b : ℕ) => a = b) := by sorry

Source