nsmul_pow_two_powHalf — Mathlib

English

For every n, 2^n times powHalf(n) equals 1 in the Surreal numbers.

Русский

Для каждого n, 2^n умноженное на powHalf(n) равно 1 в сюрреальных числах.

LaTeX

$$2^n * powHalf(n) = 1$$

Lean4

@[simp]
theorem nsmul_pow_two_powHalf (n : ℕ) : 2 ^ n * powHalf n = 1 := by
  induction n with
  | zero => simp only [pow_zero, powHalf_zero, mul_one]
  | succ n hn =>
    rw [← hn, ← double_powHalf_succ_eq_powHalf n, ← mul_assoc (2 ^ n) 2 (powHalf (n + 1)), pow_succ',
      mul_comm 2 (2 ^ n)]

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