bodd_bit

Mathlib.Data.Int.Bitwise

URI: https://scilib.ai/kg/mathlib#Int.bodd_bit

English

The parity of bit b n equals the boolean b: bodd (bit b n) = b.

Русский

Парность числа bit b n равна булевому значению b: bodd (bit b n) = b.

LaTeX

$$$$ \operatorname{bodd}(\operatorname{bit}(b,n)) = b. $$$$

Lean4

@[simp]
theorem bodd_bit (b n) : bodd (bit b n) = b := by
  rw [bit_val]
  cases b <;> cases bodd n <;> simp [(show bodd 2 = false by rfl)]

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

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

Разделы

Аффилиация

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