bit_false

Mathlib.Data.Nat.Bitwise

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

English

bit false is the doubling function: bit false = (2 * ·).

Русский

bit false — это операция удвоения: bit false = (2 * ·).

LaTeX

$$$$ \\mathrm{bit}\\ false = (2 * \\cdot) $$$$

Lean4

@[simp]
theorem bit_false : bit false = (2 * ·) :=
  rfl

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

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

Разделы

Аффилиация

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