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

Renamed a file

Browse source
This commit is contained in:
Sayantan Santra 2023-06-13 14:11:13 -07:00
parent 1dff00ff39
commit db18750677
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/sayantan.lean → CommAlg/sayantan(dim_eq_zero_iff_field).lean
View file

@ -79,4 +79,4 @@ lemma dim_eq_zero_iff_field {D: Type _} [CommRing D] [IsDomain D] : krullDim D =
· exact isField.dim_zero · exact isField.dim_zero
· intro fieldD · intro fieldD
let h : Field D := IsField.toField fieldD let h : Field D := IsField.toField fieldD
exact dim_field_eq_zero exact dim_field_eq_zero