testBit_ldiff

Mathlib.Data.Nat.Bitwise

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

English

testBit (ldiff m n) k = testBit m k ∧ ¬ testBit n k.

Русский

testBit(ldiff m n) k = testBit m k ∧ ¬ testBit n k.

LaTeX

$$$$ \\text{testBit}(\\mathrm{ldiff}\\, m\\, n)\\,k = (\\text{testBit} \\ m\\ k) \\land \\lnot (\\text{testBit} \\ n\\ k) $$$$

Lean4

@[simp]
theorem testBit_ldiff : ∀ m n k, testBit (ldiff m n) k = (testBit m k && not (testBit n k)) :=
  testBit_bitwise rfl

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

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

Разделы

Аффилиация

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