diff --git a/CommAlg/sayantan.lean b/CommAlg/sayantan(dim_eq_zero_iff_field).lean similarity index 99% rename from CommAlg/sayantan.lean rename to CommAlg/sayantan(dim_eq_zero_iff_field).lean index 7656924..35f197f 100644 --- a/CommAlg/sayantan.lean +++ b/CommAlg/sayantan(dim_eq_zero_iff_field).lean @@ -79,4 +79,4 @@ lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D = · exact isField.dim_zero · intro fieldD let h : Field D := IsField.toField fieldD - exact dim_field_eq_zero \ No newline at end of file + exact dim_field_eq_zero