From 463fce4a6ffb370946684e5146993ae41bc8588a Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Sun, 11 Feb 2024 00:59:07 +0000 Subject: [PATCH] doc: fix typo (#10409) Fix minor typo. --- 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. -/