Divisor_Relation_is_Primitive_Recursive

Proved

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

computabilitydivisibilityprimitive-recursive-functionsproofwiki

The divisor relation $m \divides n$ in $\N^2$ is primitive recursive.

Preamble

import Mathlib.Computability.Primrec

Formal statement

theorem Divisor_Relation_is_Primitive_Recursive : PrimrecRel (fun (m n : ℕ) => m ∣ n) := by sorry

Source