identical_zero — Mathlib

English

Any game with no left or right moves is identical to 0.

Русский

Любая игра без левых и правых ходов идентична нулю.

LaTeX

$$$ x \equiv 0 \quad\text{whenever } IsEmpty(x.LeftMoves) \text{ and } IsEmpty(x.RightMoves) $$$

Lean4

/-- Any game without left or right moves is identical to 0. -/
theorem identical_zero (x : PGame) [IsEmpty x.LeftMoves] [IsEmpty x.RightMoves] : x ≡ 0 :=
  x.identical_zero_iff.mpr ⟨by infer_instance, by infer_instance⟩

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