fin

Mathlib.Computability.Primrec

URI: https://scilib.ai/kg/mathlib#Primcodable.fin

English

For each n, Fin n is a primitive codable type.

Русский

Для каждого n тип Fin n является примитивно-кодируемым.

LaTeX

$$$\text{Primcodable}(\mathrm{Fin}(n))$$$

Lean4

instance fin {n} : Primcodable (Fin n) :=
  @ofEquiv _ _ (subtype <| nat_lt.comp .id (const n)) Fin.equivSubtype

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

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

Разделы

Аффилиация

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