From 02cb30cef94a16a664fdeec7ebcbbcc03b0419f5 Mon Sep 17 00:00:00 2001 From: David Renshaw Date: Sat, 9 Sep 2023 23:05:43 -0400 Subject: [PATCH] [ZeroesOnesAndTwos] remove unneeded GCD import --- MathPuzzles/ZeroesOnesAndTwos.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/MathPuzzles/ZeroesOnesAndTwos.lean b/MathPuzzles/ZeroesOnesAndTwos.lean index 0ebecb3d..8aa01f3e 100644 --- a/MathPuzzles/ZeroesOnesAndTwos.lean +++ b/MathPuzzles/ZeroesOnesAndTwos.lean @@ -8,7 +8,6 @@ import Mathlib.Data.Nat.Basic import Mathlib.Data.Nat.ModEq import Mathlib.Data.Nat.Parity import Mathlib.Data.Nat.Digits -import Mathlib.Data.Nat.GCD.Basic /-! (From Mathematical Puzzles: A Connoisseur's Collection by Peter Winkler.)