lor_assoc

Mathlib.Data.Nat.Bitwise

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

← MathLib Explorer

English

Bitwise OR is associative: (n ||| m) ||| k = n ||| (m ||| k).

Русский

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

LaTeX

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

Lean4

theorem lor_assoc (n m k : ℕ) : (n ||| m) ||| k = n ||| (m ||| k) := by
  bitwise_assoc_tac
    -- These lemmas match `mul_inv_cancel_right` and `mul_inv_cancel_left`.

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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