nsmul_pow_two_powHalf' — Mathlib

English

For all n, k in natural numbers, 2^n · powHalf(n+k) = powHalf(k).

Русский

Пусть n, k ∈ натуральные. Тогда 2^n · powHalf(n+k) = powHalf(k).

LaTeX

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

Lean4

@[simp]
theorem nsmul_pow_two_powHalf' (n k : ℕ) : 2 ^ n * powHalf (n + k) = powHalf k := by
  induction k with
  | zero => simp only [add_zero, Surreal.nsmul_pow_two_powHalf, Surreal.powHalf_zero]
  | succ k
    hk =>
    rw [← double_powHalf_succ_eq_powHalf (n + k), ← double_powHalf_succ_eq_powHalf k, ← mul_assoc, mul_comm (2 ^ n) 2,
      mul_assoc] at hk
    rw [← zsmul_eq_zsmul_iff' two_ne_zero]
    simpa only [zsmul_eq_mul, Int.cast_ofNat]

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