nat_bodd

Mathlib.Computability.Primrec

URI: https://scilib.ai/kg/mathlib#Primrec.nat_bodd

← MathLib Explorer

English

Parity (bodd) is primitive recursive.

Русский

Паритет (odd) является примитивно вычисимой функцией.

LaTeX

$$$Nat.bodd$ is primitive recursive.$$

Lean4

theorem nat_bodd : Primrec Nat.bodd :=
  (Primrec.beq.comp (nat_mod.comp .id (const 2)) (const 1)).of_eq fun n => by
    cases H : n.bodd <;> simp [Nat.mod_two_of_bodd, H]

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru