From e65513322c59ffc53029c17124a6ab692ca82bb3 Mon Sep 17 00:00:00 2001
From: GTBarkley <barkleygrant@gmail.com>
Date: Sun, 11 Jun 2023 06:49:28 +0000
Subject: [PATCH] function relating the offbrand notions of chain

---
 comm_alg/grant.lean | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/comm_alg/grant.lean b/comm_alg/grant.lean
index 2814919..de3e50f 100644
--- a/comm_alg/grant.lean
+++ b/comm_alg/grant.lean
@@ -18,6 +18,14 @@ import Mathlib.Order.Height
 
 variable {α : Type _} [Preorder α] (s : Set α)
 
+def finFun_to_list {n : ℕ} : (Fin n → α) → List α := by sorry
+
+def series_to_chain : StrictSeries s → s.subchain
+| ⟨length, toFun, strictMono⟩ => 
+    ⟨ finFun_to_list (fun x => toFun x),
+      sorry⟩
+
+
 -- there should be a coercion from WithTop ℕ to WithBot (WithTop ℕ) but it doesn't seem to work
 -- it looks like this might be because someone changed the instance from CoeCT to Coe during the port
 lemma twoHeights : s ≠ ∅ → (some (Set.chainHeight s) : WithBot (WithTop ℕ)) = krullDim s := by