| .. |
|
final_poly_type.lean
|
removed a comment
|
2023-06-16 17:42:48 -04:00 |
|
grant.lean
|
proved dim_le_zero_iff
|
2023-06-14 20:28:19 +00:00 |
|
grant2.lean
|
proved principle ideal theorem mod sorries
|
2023-06-16 22:14:09 +00:00 |
|
grant3.lean
|
testing api for StrictSeries
|
2023-07-11 04:41:48 +00:00 |
|
hil_mine.lean
|
rearranged defs
|
2023-06-16 22:00:43 +00:00 |
|
hilbertpolynomial.lean
|
moved files into CommAlg
|
2023-06-14 17:38:40 +00:00 |
|
jayden(krull-dim-zero).lean
|
Is it too late to say sorry
|
2023-06-16 14:37:06 -07:00 |
|
krull.lean
|
removed sorried lemmas that are now proved elsewhe
|
2023-06-16 14:54:36 -07:00 |
|
Leo.lean
|
Finished last sorry on dim_le_dim_polynomial!!!
|
2023-06-15 18:05:33 -07:00 |
|
monalisa.lean
|
added graded morphism def
|
2023-06-15 04:19:56 +00:00 |
|
poly_type.lean
|
reduced imports poly_type
|
2023-06-14 16:28:25 -04:00 |
|
polynomial.lean
|
golfed imports
|
2023-06-16 09:54:07 -07:00 |
|
quotient.lean
|
Complete proof that dim (R/I) <= dim R
|
2023-06-16 14:53:24 -07:00 |
|
resources.lean
|
Merge branch 'main' of github.com:GTBarkley/comm_alg into main
|
2023-06-12 10:50:59 -07:00 |
|
sameer(artinian-rings).lean
|
Implemented FieldisArtinian lemma
|
2023-06-15 10:26:31 -07:00 |
|
sayantan(dim_eq_dim_polynomial_add_one).lean
|
Tried to avoid the finiteness condition on height P
|
2023-06-14 23:51:46 -07:00 |
|
sayantan(poly_over_field).lean
|
Add the whole proof back since I just noticed that I had replaced them by sorried statements
|
2023-06-16 11:37:19 -07:00 |
|
StrictSeries.lean
|
added eraseBot and API for it
|
2023-06-22 05:30:47 +00:00 |
