toBitVec_natCast

Mathlib.Data.UInt

URI: https://scilib.ai/kg/mathlib#USize.toBitVec_natCast

English

The bit-vector representation of the natural cast to USize is just the natural number itself.

Русский

Битовый вектор преобразования натурального числа в USize равен самому числу.

LaTeX

$$$\forall n\in\mathbb{N},\; (n:\mathrm{USize}).\operatorname{toBitVec} = n$$$

Lean4

@[simp, int_toBitVec]
protected theorem toBitVec_natCast (n : ℕ) : (n : USize).toBitVec = n :=
  rfl

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

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

Разделы

Аффилиация

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