testBit_land

Mathlib.Data.Nat.Bitwise

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

English

testBit distributes over bitwise AND: testBit (m &&& n) k = (testBit m k) ∧ (testBit n k).

Русский

testBit распределяется через побитовое AND: testBit (m &&& n) k = testBit m k ∧ testBit n k.

LaTeX

$$$$ \\text{testBit}(m\\,\\&\\&\\&\\,n)\\,k = (\\text{testBit}\\,m\\,k) \\land (\\text{testBit}\\,n\\,k) $$$$

Lean4

theorem testBit_land : ∀ m n k, testBit (m &&& n) k = (testBit m k && testBit n k) :=
  testBit_bitwise rfl

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

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

Разделы

Аффилиация

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