From ae8bf07ee7b82901b157fb81d018120f8f52c804 Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Wed, 14 Jun 2023 11:23:29 -0700 Subject: [PATCH] Make the lemma names a little more descriptive --- CommAlg/krull.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/CommAlg/krull.lean b/CommAlg/krull.lean index 1e720c0..ec94d36 100644 --- a/CommAlg/krull.lean +++ b/CommAlg/krull.lean @@ -135,7 +135,7 @@ lemma dim_field_eq_zero {K : Type _} [Field K] : krullDim K = 0 := by unfold krullDim simp [field_prime_height_zero] -lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by +lemma domain_dim_zero.isField {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) : IsField D := by by_contra x rw [Ring.not_isField_iff_exists_prime] at x obtain ⟨P, ⟨h1, primeP⟩⟩ := x @@ -156,9 +156,9 @@ lemma isField.dim_zero {D: Type _} [CommRing D] [IsDomain D] (h: krullDim D = 0) aesop contradiction -lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by +lemma domain_dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = 0 ↔ IsField D := by constructor - · exact isField.dim_zero + · exact domain_dim_zero.isField · intro fieldD let h : Field D := IsField.toField fieldD exact dim_field_eq_zero