From db1875067783ee57b4013b8c5ce54d335a9c63ac Mon Sep 17 00:00:00 2001 From: SinTan1729 Date: Tue, 13 Jun 2023 14:11:13 -0700 Subject: [PATCH] Renamed a file --- CommAlg/{sayantan.lean => sayantan(dim_eq_zero_iff_field).lean} | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) rename CommAlg/{sayantan.lean => sayantan(dim_eq_zero_iff_field).lean} (99%) 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