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

Merge pull request #39 from GTBarkley/sayantan

Browse source 
Renamed a file
This commit is contained in:
Sayantan Santra 2023-06-13 16:12:38 -05:00 committed by GitHub
commit 6bf4ae5d46
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
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
· intro fieldD
let h : Field D := IsField.toField fieldD
exact dim_field_eq_zero
exact dim_field_eq_zero