From fa2abd3a886de3829656b2d7edf1f24c9e00bd67 Mon Sep 17 00:00:00 2001 From: Nehal Patel <1161604+habemus-papadum@users.noreply.github.com> Date: Wed, 4 Dec 2024 08:04:37 -0500 Subject: [PATCH] Fix Build Issue - Change spelling to use lowercase '03_Nonsingularity_Of_Curves' -> '03_Nonsingularity_of_Curves' --- PolyrithTutorial.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/PolyrithTutorial.lean b/PolyrithTutorial.lean index f36ca1f..13fc0e9 100644 --- a/PolyrithTutorial.lean +++ b/PolyrithTutorial.lean @@ -4,8 +4,8 @@ import PolyrithTutorial.«01_Basics_of_Polyrith».«04Polyrith» import PolyrithTutorial.«02_Using_Polyrith».«01Chebyshev» import PolyrithTutorial.«02_Using_Polyrith».«02IsometryPlane» import PolyrithTutorial.«02_Using_Polyrith».«03DoubleCover» -import PolyrithTutorial.«03_Nonsingularity_Of_Curves».«01PowersCaseSplits» -import PolyrithTutorial.«03_Nonsingularity_Of_Curves».«02ProjectiveCurves» +import PolyrithTutorial.«03_Nonsingularity_of_Curves».«01PowersCaseSplits» +import PolyrithTutorial.«03_Nonsingularity_of_Curves».«02ProjectiveCurves» import PolyrithTutorial.«04_Combining_Tactics».«01FieldSimp» import PolyrithTutorial.«04_Combining_Tactics».«02Sphere» import PolyrithTutorial.«04_Combining_Tactics».«03Binomial»