bit_true

Mathlib.Data.Nat.Bitwise

URI: https://scilib.ai/kg/mathlib#Nat.bit_true

English

bit true is the doubling-plus-one function: bit true = (2 * · + 1).

Русский

bit true — это удвоение плюс единица: bit true = (2 * · + 1).

LaTeX

$$$$ \\mathrm{bit}\\ true = (2 * \\cdot + 1) $$$$

Lean4

@[simp]
theorem bit_true : bit true = (2 * · + 1) :=
  rfl

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

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

Разделы

Аффилиация

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