shiftLeft'_add — Mathlib

English

For any Bool b, Nat m,n,k, we have shiftLeft'(b,m,n+k) = shiftLeft'(b, shiftLeft'(b,m,n), k).

Русский

Для любого b∈{true,false}, m,n,k∈Nat выполняется shiftLeft'(b,m,n+k) = shiftLeft'(b, shiftLeft'(b,m,n), k).

LaTeX

$$$$ \forall (b : \mathrm{Bool}) (m\, n\, k : \mathbb{N}),\; \text{shiftLeft}'(b,m,(n+k)) = \text{shiftLeft}'(b,\text{shiftLeft}'(b,m,n),k). $$$$

Lean4

theorem shiftLeft'_add (b m n) : ∀ k, shiftLeft' b m (n + k) = shiftLeft' b (shiftLeft' b m n) k
  | 0 => rfl
  | k + 1 => congr_arg (bit b) (shiftLeft'_add b m n k)

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