shiftLeft_eq_mul_pow — Mathlib

English

For all integers m and natural n, the left shift equals multiplication by 2^n: m <<< n = m * 2^n.

Русский

Для любых m ∈ ℤ и n ∈ ℕ: m <<< n = m · 2^n.

LaTeX

$$$$ \forall m\in\mathbb{Z},\; \forall n\in\mathbb{N},\; m <<< n = m \cdot (2^{n}). $$$$

Lean4

theorem shiftLeft_eq_mul_pow : ∀ (m : ℤ) (n : ℕ), m <<< (n : ℤ) = m * (2 ^ n : ℕ)
  | (m : ℕ), _ => congr_arg ((↑) : ℕ → ℤ) (by simp [Nat.shiftLeft_eq])
  | -[_+1], _ => @congr_arg ℕ ℤ _ _ (fun i => -i) (Nat.shiftLeft'_tt_eq_mul_pow _ _)

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