toGame_natCast — Mathlib

English

Natural numbers embed into games via toGame with preservation of the natural numbers.

Русский

Естественные числа встраиваются в игры через toGame с сохранением чисел внутри.

LaTeX

$$toGame_natCast : \forall n:\mathbb{N}, toGame(n) = n$$

Lean4

@[simp] -- used to be a norm_cast lemma

theorem toGame_natCast : ∀ n : ℕ, toGame n = n
  | 0 => Quot.sound (zeroToPGameRelabelling).equiv
  | n + 1 => by
    have : toGame 1 = 1 := Quot.sound oneToPGameRelabelling.equiv
    rw [Nat.cast_add, ← nadd_nat, toGame_nadd, toGame_natCast, Nat.cast_one, this]
    rfl

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