land_bit — Mathlib

English

The bitwise AND operation equals the bit at position with conjunction: land (bit a m) (bit b n) = bit (a ∧ b) (land m n).

Русский

Побитовое И выполняется как конъюнкция на позиции: land (bit a m) (bit b n) = bit (a ∧ b) (land m n).

LaTeX

$$$$ \operatorname{land\_{bit}}(a,m,b,n) = \operatorname{bit}(a \land b)(\operatorname{land} m n). $$$$

Lean4

@[simp]
theorem land_bit (a m b n) : land (bit a m) (bit b n) = bit (a && b) (land m n) := by rw [← bitwise_and, bitwise_bit]

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