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