zsmul_pow_two_powHalf

Mathlib.SetTheory.Surreal.Dyadic

URI: https://scilib.ai/kg/mathlib#Surreal.zsmul_pow_two_powHalf

← MathLib Explorer

English

For all m ∈ ℤ, n, k ∈ ℕ, (m · 2^n) · powHalf(n+k) = m · powHalf(k).

Русский

Для всех m ∈ ℤ, n, k ∈ ℕ выполняется (m · 2^n) · powHalf(n+k) = m · powHalf(k).

LaTeX

$$$$ (m \cdot 2^n) \cdot powHalf(n+k) = m \cdot powHalf(k) $$$$

Lean4

theorem zsmul_pow_two_powHalf (m : ℤ) (n k : ℕ) : (m * 2 ^ n) * powHalf (n + k) = m * powHalf k :=
  by
  rw [mul_assoc]
  congr
  exact nsmul_pow_two_powHalf' n k

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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