encodeCode_eq

Mathlib.Computability.PartrecCode

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

English

The canonical encoding and encodeCode agree: encode equals encodeCode.

Русский

Каноническое кодирование и encodeCode совпадают: encode = encodeCode.

LaTeX

$$$\\mathrm{encode} = \\mathrm{encodeCode}$$$

Lean4

theorem encodeCode_eq : encode = encodeCode :=
  rfl

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

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

Разделы

Аффилиация

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