finArrow

Mathlib.Computability.Primrec

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

English

The type Fin n → α is primitive codable.

Русский

Тип Fin n → α примитивно-кодируем.

LaTeX

$$$\mathrm{Primcodable}(\mathrm{Fin}(n) \to \alpha)$$$

Lean4

instance finArrow {n} : Primcodable (Fin n → α) :=
  ofEquiv _ (Equiv.vectorEquivFin _ _).symm

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

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

Разделы

Аффилиация

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