equivFin

Mathlib.Data.BitVec

URI: https://scilib.ai/kg/mathlib#BitVec.equivFin

← MathLib Explorer

English

There is a ring isomorphism between BitVec m and Fin (2^m).

Русский

Существует кольцевое изоморфизм между BitVec m и Fin(2^m).

LaTeX

$$$\text{BitVec}(m) \cong_{\mathrm{Ring}} \mathrm{Fin}(2^m)$$$

Lean4

/-- The ring `BitVec m` is isomorphic to `Fin (2 ^ m)`. -/
@[simps]
def equivFin {m : ℕ} : BitVec m ≃+* Fin (2 ^ m)
    where
  toFun a := a.toFin
  invFun a := ofFin a
  map_mul' := toFin_mul
  map_add' := toFin_add

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

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

Разделы

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

Аффилиация

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