From 431d25f92f73f49b69d08db7838f140f936292f3 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sat, 10 Feb 2024 22:19:50 +0100 Subject: [PATCH] Update Impartial.lean --- Mathlib/SetTheory/Game/Impartial.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/SetTheory/Game/Impartial.lean b/Mathlib/SetTheory/Game/Impartial.lean index af1907e2b0280..3447c4acaf185 100644 --- a/Mathlib/SetTheory/Game/Impartial.lean +++ b/Mathlib/SetTheory/Game/Impartial.lean @@ -13,7 +13,7 @@ import Mathlib.Tactic.NthRewrite We will define an impartial game, one in which left and right can make exactly the same moves. Our definition differs slightly by saying that the game is always equivalent to its negative, -no matter what moves are played. This allows for games such as poker-nim to be classifed as +no matter what moves are played. This allows for games such as poker-nim to be classified as impartial. -/