double_powHalf_succ_eq_powHalf — Mathlib

English

In Surreal numbers, 2 * powHalf(n+1) = powHalf(n) holds for every n (via quotient equivalence).

Русский

В сюрреальных числах выполняется 2 · powHalf(n+1) = powHalf(n) для каждого n (по эквивалентности частного).

LaTeX

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

Lean4

@[simp]
theorem double_powHalf_succ_eq_powHalf (n : ℕ) : 2 * powHalf (n + 1) = powHalf n := by rw [two_mul];
  exact Quotient.sound (PGame.add_powHalf_succ_self_eq_powHalf n)

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