land_assoc

Mathlib.Data.Nat.Bitwise

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

English

Bitwise AND is associative: (n &&& m) &&& k = n &&& (m &&& k).

Русский

Побитовая операция AND ассоциативна: (n &&& m) &&& k = n &&& (m &&& k).

LaTeX

$$$ (n \land m) \land k = n \land (m \land k) $$$

Lean4

theorem land_assoc (n m k : ℕ) : (n &&& m) &&& k = n &&& (m &&& k) := by bitwise_assoc_tac

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

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

Разделы

Аффилиация

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