toFin_nsmul

Mathlib.Data.BitVec

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

← MathLib Explorer

English

Further variant of injectivity for toNat.

Русский

Дальнейшее вариативное утверждение инъективности toNat.

LaTeX

$$$\forall x,y : BitVec w,\; toNat(x) = toNat(y) \Rightarrow x = y$$$

Lean4

theorem toFin_nsmul (n : ℕ) (x : BitVec w) : toFin (n • x) = n • x.toFin :=
  toFin_mul _ _ |>.trans <| by
    open scoped Fin.CommRing in simp only [natCast_eq_ofNat, toFin_ofNat, Fin.ofNat_eq_cast, nsmul_eq_mul]

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

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

Разделы

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

Аффилиация

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