testBit_land — Mathlib

English

For all integers m, n and natural k, testBit (land m n) k equals (testBit m k) and (testBit n k).

Русский

Для любых целых m, n и натурального k: k-й бит результата land m n равен логической конъюнкции k-й битов m и n.

LaTeX

$$$$\forall m,n\in\mathbb{Z},\; \forall k\in\mathbb{N},\; \mathrm{testBit}(\mathrm{land}\, m\, n)\ k = (\mathrm{testBit}\, m\ k)\land(\mathrm{testBit}\, n\ k).$$$$

Lean4

@[simp]
theorem testBit_land (m n k) : testBit (land m n) k = (testBit m k && testBit n k) := by
  rw [← bitwise_and, testBit_bitwise]

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