shiftLeft'_false — Mathlib

English

shiftLeft' false m n equals m shifted left by n bits, i.e., m <<< n.

Русский

shiftLeft' false m n равняется m, сдвинутому влево на n разрядов, то есть m <<< n.

LaTeX

$$$\mathrm{shiftLeft'}(\mathrm{false}, m, n) = m \\text{ <<< } n$$$

Lean4

@[simp]
theorem shiftLeft'_false : ∀ n, shiftLeft' false m n = m <<< n
  | 0 => rfl
  | n + 1 =>
    by
    have : 2 * (m * 2 ^ n) = 2 ^ (n + 1) * m := by rw [Nat.mul_comm, Nat.mul_assoc, ← Nat.pow_succ]; simp
    simp [shiftLeft_eq, shiftLeft', bit_val, shiftLeft'_false, this]

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