SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-10-16 19:43:55 -05:00
Code Issues Projects Releases Packages Wiki Activity

function relating the offbrand notions of chain

Browse source
This commit is contained in:
GTBarkley 2023-06-11 06:49:28 +00:00
parent 8b28694f0e
commit e65513322c
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
comm_alg/grant.lean
View file

@ -18,6 +18,14 @@ import Mathlib.Order.Height
variable {α : Type _} [Preorder α] (s : Set α) 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 -- 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 -- 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 lemma twoHeights : s ≠ ∅ → (some (Set.chainHeight s) : WithBot (WithTop ℕ)) = krullDim s := by