bitIndices_two_pow_mul — Mathlib

English

For all k,n, bitIndices(2^k * n) = (bitIndices n).map (+k).

Русский

Для всех k,n: bitIndices(2^k * n) = (bitIndices n).map (+k).

LaTeX

$$$ bitIndices(2^k * n) = (bitIndices\ n).map (+k) $$$

Lean4

@[simp]
theorem bitIndices_two_pow_mul (k n : ℕ) : bitIndices (2 ^ k * n) = (bitIndices n).map (· + k) := by
  induction k with
  | zero => simp
  | succ k
    ih =>
    rw [add_comm, pow_add, pow_one, mul_assoc, bitIndices_two_mul, ih, List.map_map, comp_add_right]
    simp [add_comm (a := 1)]

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