From 42c1c14edf2e2d26495b4bafdda5115be88e24c9 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 12 Sep 2024 07:13:35 +0200
Subject: [PATCH] Delete diffOpGrothendieck.lean

---
 Nevanlinna/diffOpGrothendieck.lean | 9 ---------
 1 file changed, 9 deletions(-)
 delete mode 100644 Nevanlinna/diffOpGrothendieck.lean

diff --git a/Nevanlinna/diffOpGrothendieck.lean b/Nevanlinna/diffOpGrothendieck.lean
deleted file mode 100644
index c76f80c..0000000
--- a/Nevanlinna/diffOpGrothendieck.lean
+++ /dev/null
@@ -1,9 +0,0 @@
-import Mathlib.Analysis.Calculus.ContDiff.Basic
-import Mathlib.Analysis.InnerProductSpace.PiL2
-
-/-
-
-Here we would like to define differential operators, following EGA 4-1, §20.
-This is work to be done in the future.
-
--/
\ No newline at end of file