shiftLeft'_tt_eq_mul_pow — Mathlib

English

For all m, n, shiftLeft' true m n + 1 equals (m + 1) * 2^n.

Русский

Для любых m, n выражение shiftLeft' true m n + 1 равно (m + 1) * 2^n.

LaTeX

$$$ \\operatorname{shiftLeft}'(\\text{true})\\, m\\, n + 1 = (m + 1) \\cdot 2^n $$$

Lean4

theorem shiftLeft'_tt_eq_mul_pow (m) : ∀ n, shiftLeft' true m n + 1 = (m + 1) * 2 ^ n
  | 0 => by simp [shiftLeft', pow_zero]
  | k + 1 => by
    rw [shiftLeft', bit_val, Bool.toNat_true, add_assoc, ← Nat.mul_add_one, shiftLeft'_tt_eq_mul_pow m k, mul_left_comm,
      mul_comm 2, pow_succ]

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