shiftl_succ_eq_bit0_shiftl

Mathlib.Data.Num.Bitwise

URI: https://scilib.ai/kg/mathlib#PosNum.shiftl_succ_eq_bit0_shiftl

← MathLib Explorer

English

For every p and n, p <<< (n+1) = bit0 (p <<< n).

Русский

Для любого p и n: p <<< (n+1) = bit0 (p <<< n).

LaTeX

$$theorem shiftl_succ_eq_bit0_shiftl : ∀ (p : PosNum) (n : Nat), p <<< n.succ = bit0 (p <<< n) | _, 0 => rfl | p, .succ n => shiftl_succ_eq_bit0_shiftl p.bit0 n$$

Lean4

theorem shiftl_succ_eq_bit0_shiftl : ∀ (p : PosNum) (n : Nat), p <<< n.succ = bit0 (p <<< n)
  | _, 0 => rfl
  | p, .succ n => shiftl_succ_eq_bit0_shiftl p.bit0 n

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

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

Разделы

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

Аффилиация

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