From 01f628cf986c8bdc6d9a13592c888408278f1246 Mon Sep 17 00:00:00 2001
From: chelseaandmadrid <53058005+chelseaandmadrid@users.noreply.github.com>
Date: Thu, 15 Jun 2023 20:43:52 -0700
Subject: [PATCH] kind of finish \Delta of d times lemma
---
CommAlg/final_poly_type.lean | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/CommAlg/final_poly_type.lean b/CommAlg/final_poly_type.lean
index 96a3aca..4405e42 100644
--- a/CommAlg/final_poly_type.lean
+++ b/CommAlg/final_poly_type.lean
@@ -199,7 +199,9 @@ lemma foofoo (d : ℕ) : (f : ℤ → ℤ) → (PolyType f d) → (PolyType (Δ
have this1 : PolyType f (d + 1) := by tauto
have this2 : PolyType (Δ f (d + 1)) 0 := by
have this3 : PolyType (Δ f 1) d := by
- sorry
+ have this4 : d + 1 > 0 := by positivity
+ have this5 : (d + 1) > 0 → PolyType f (d + 1) → PolyType (Δ f 1) d := Δ_1 f (d + 1)
+ exact this5 this4 this1
clear hf
specialize hd (Δ f 1)
have this4 : PolyType (Δ (Δ f 1) d) 0 := by tauto