ofNatCode_eq

Mathlib.Computability.PartrecCode

URI: https://scilib.ai/kg/mathlib#Nat.Partrec.Code.ofNatCode_eq

English

ofNat Code equals ofNatCode: decoding from Nat to Code matches the existing decoder.

Русский

ofNat Code равняется ofNatCode: расшифровка из Nat в Code совпадает с существующим декодером.

LaTeX

$$$\\mathrm{ofNatCode} = \\mathrm{ofNat} \\text{Code}$$$

Lean4

theorem ofNatCode_eq : ofNat Code = ofNatCode :=
  rfl

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

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

Разделы

Аффилиация

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