SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-12-26 23:48:36 -06:00
Code Issues Projects Releases Packages Wiki Activity

Added a comment

Browse source
This commit is contained in:
Sayantan Santra 2023-06-13 14:16:53 -07:00
parent 6bf4ae5d46
commit 5f241e80f1
Signed by: SinTan1729
GPG key ID: EB3E68BFBA25C85F
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
CommAlg/krull.lean
View file

@ -88,7 +88,7 @@ lemma dim_eq_bot_iff : krullDim R = ⊥ ↔ Subsingleton R := by
. rw [h.forall_iff] . rw [h.forall_iff]
trivial trivial
lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry lemma dim_eq_zero_iff_field [IsDomain R] : krullDim R = 0 ↔ IsField R := by sorry -- It's been done in another file
#check Ring.DimensionLEOne #check Ring.DimensionLEOne
lemma dim_le_one_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry lemma dim_le_one_iff : krullDim R ≤ 1 ↔ Ring.DimensionLEOne R := sorry