add sorry to compile

pink10000 · pink10000 · commit 8b558f4c434a · 2024-11-24T11:28:09.000-08:00
diff --git a/LeanCommAlg/Basic.lean b/LeanCommAlg/Basic.lean
@@ -29,5 +29,5 @@ theorem height_1_of_principal_of_prime [h : I.IsPrime] [h' : I.IsPrincipal] : he
   rw [height, Order.height]
   simp_all
   intro ltseries relseries
-
+  sorry
   -- Associated primes, Krull's principal ideal theorem,
