bitIndices_two_pow

Mathlib.Data.Nat.BitIndices

URI: https://scilib.ai/kg/mathlib#Nat.bitIndices_two_pow

English

For all k, bitIndices(2^k) = [k].

Русский

Для любого k: bitIndices(2^k) = [k].

LaTeX

$$$ bitIndices(2^k) = [k] $$$

Lean4

@[simp]
theorem bitIndices_two_pow (k : ℕ) : bitIndices (2 ^ k) = [k] := by rw [← mul_one (a := 2 ^ k), bitIndices_two_pow_mul];
  simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru