Commit graph

Select branches

Hide pull requests

bobby

grant

jayden

main

monalisa

monalisa3

monalisa4

monula95-patch-1

sayantan

#1

#10

#100

#101

#102

#103

#104

#105

#106

#107

#108

#11

#12

#13

#14

#15

#16

#17

#18

#19

#2

#20

#21

#22

#23

#24

#25

#26

#27

#28

#29

#3

#30

#31

#32

#33

#34

#35

#36

#37

#38

#39

#4

#40

#41

#42

#43

#44

#45

#46

#47

#48

#49

#5

#50

#51

#52

#53

#54

#55

#56

#57

#58

#59

#6

#60

#61

#62

#63

#64

#65

#66

#67

#68

#69

#7

#70

#71

#72

#73

#74

#75

#76

#77

#78

#79

#8

#80

#81

#82

#83

#84

#85

#86

#87

#88

#89

#9

#90

#91

#92

#93

#94

#95

#96

#97

#98

#99

Mono Color

• 5da3b52dde Merge branch 'monalisa' of github.com:GTBarkley/comm_alg into monalisa chelseaandmadrid 2023-06-15 20:27:35 -0700
• 31210a9bf5 add foo and foofoo chelseaandmadrid 2023-06-15 20:27:29 -0700
• 54c76464bc
  
  Added some comments SinTan1729 2023-06-15 20:06:08 -0700
• 1cf31c2590
  Merge pull request #78 from SinTan1729/main Sayantan Santra 2023-06-15 21:45:48 -0500
• a7055d64e3
  Merge branch 'GTBarkley:main' into main Sayantan Santra 2023-06-15 21:43:09 -0500
• eb1e6118a0
  
  Some changes to dim_eq_dim_poly_add_one SinTan1729 2023-06-15 19:36:02 -0700
• e9fbb1a521
  
  Minor changes SinTan1729 2023-06-15 19:34:20 -0700
• 01bce563a5
  
  One side of poly_over_field SinTan1729 2023-06-15 19:33:24 -0700
• c1e8ddeaf7 Merge branch 'monalisa' of github.com:GTBarkley/comm_alg into monalisa Andre 2023-06-15 22:10:33 -0400
• b8928c8d90 refactored PolyType_0 Andre 2023-06-15 22:09:13 -0400
• 8ad3b1d55e
  Merge pull request #77 from GTBarkley/grant GTBarkley 2023-06-15 18:23:33 -0700
• 24a0460566 defined symbolicIdeal (generalized symbolic power) GTBarkley 2023-06-16 01:22:46 +0000
• 828bf44695
  Merge pull request #76 from GTBarkley/leo Leo Mayer 2023-06-15 18:06:41 -0700
• 204a2ed47e Merge branch 'main' of github.com:GTBarkley/comm_alg into main leopoldmayer 2023-06-15 18:05:48 -0700
• c1b99a1b22 Finished last sorry on dim_le_dim_polynomial!!! leopoldmayer 2023-06-15 18:05:33 -0700
• d5b2e4d431 Part of the base case of \Delta lemma chelseaandmadrid 2023-06-15 17:51:32 -0700
• 53c4675cb8 started the proof for the base case monula95 dutta 2023-06-15 23:07:55 +0000
• 300007621a Finish the PolyType_0 lemma! chelseaandmadrid 2023-06-15 15:38:25 -0700
• 57ecb6a9e3
  Merge pull request #75 from SinTan1729/main Sayantan Santra 2023-06-15 17:19:31 -0500
• 6148376bac
  Merge branch 'GTBarkley:main' into main Sayantan Santra 2023-06-15 17:18:46 -0500
• e93a53bd67
  
  Proved le_krullDim_iff SinTan1729 2023-06-15 15:18:22 -0700
• 007e8cf795 finish more on the PolyType_0 lemma chelseaandmadrid 2023-06-15 15:10:30 -0700
• 2d5a7d3deb defined codimension of an ideal GTBarkley 2023-06-15 20:35:28 +0000
• 61a7ae54bf change PolyType chelseaandmadrid 2023-06-15 13:31:48 -0700
• 41105f8623 Rename the file chelseaandmadrid 2023-06-15 12:40:41 -0700
• 75cc002bef finished a case of polytype 0 chelseaandmadrid 2023-06-15 12:31:37 -0700
• a75dadccd1
  Merge pull request #74 from ssavkar1/main ssavkar1 2023-06-15 10:28:00 -0700
• 4e819719a6 Implemented FieldisArtinian lemma Sameer Savkar 2023-06-15 10:26:31 -0700
• 5cebb2fa13
  Merge pull request #73 from SinTan1729/main Sayantan Santra 2023-06-15 01:54:36 -0500
• 5a463e00cc
  Merge branch 'GTBarkley:main' into main Sayantan Santra 2023-06-15 01:53:49 -0500
• 947c28f001
  
  Tried to avoid the finiteness condition on height P SinTan1729 2023-06-14 23:51:46 -0700
• 766c740c8d Add graded_isom (with error) chelseaandmadrid 2023-06-14 23:35:46 -0700
• 3078f0f8d9
  Merge pull request #72 from GTBarkley/grant GTBarkley 2023-06-14 22:51:57 -0700
• 5a86902118 changed chelseaandmadrid 2023-06-14 22:10:22 -0700
• fcb204d2d0
  Merge pull request #71 from GTBarkley/monalisa Monalisa Dutta 2023-06-14 22:06:45 -0700
• 1f7a809e2c unified monalisa.lean and HilbertFunction.lean monula95 dutta 2023-06-15 05:02:47 +0000
• fe64034b11 Added standard graded assumption monula95 dutta 2023-06-15 04:59:31 +0000
• 5fa7d286cd added standard graded assumption monula95 dutta 2023-06-15 04:58:58 +0000
• 804fd57037 a little standard graded chelseaandmadrid 2023-06-14 21:53:35 -0700
• 165d598066
  Merge pull request #70 from GTBarkley/jayden Jidong Wang 2023-06-14 21:32:54 -0700
• 40e26d8636 Hahaha poincare-duality 2023-06-14 21:32:22 -0700
• 82a4ded17c Ultimate version of HilbertFunction chelseaandmadrid 2023-06-14 21:30:17 -0700
• 37cc2c5a3c added graded morphism def monula95 dutta 2023-06-15 04:19:56 +0000
• f9e7942a60 Add statements for the reduced case M=R/p chelseaandmadrid 2023-06-14 21:13:11 -0700
• 191e02e984 Updated PolyType chelseaandmadrid 2023-06-14 20:51:45 -0700
• b7aae64f76
  Merge pull request #69 from GTBarkley/jayden Jidong Wang 2023-06-14 19:14:29 -0700
• 999659039d more stuff poincare-duality 2023-06-14 19:14:01 -0700
• 89d7be5bc9 added docstrings to krull.lean GTBarkley 2023-06-15 00:40:57 +0000
• e103d3d1ac
  Merge pull request #68 from SinTan1729/main Sayantan Santra 2023-06-14 19:02:19 -0500
• 70007679cd
  
  Trying to break it down to smaller parts SinTan1729 2023-06-14 17:01:34 -0700
• 08711d7689 not_maximal_of_lt_prime in dim_le_one_of_dimLEOne GTBarkley 2023-06-14 22:36:08 +0000
• ac0a660641 add shifting-inv lemma for PolyType chelseaandmadrid 2023-06-14 15:35:15 -0700
• 79a6844707 graded local lemmma added monula95 dutta 2023-06-14 22:00:39 +0000
• bbfba6a2f7 added graded submodule monula95 dutta 2023-06-14 21:50:00 +0000
• 900bf12da2 Added comments to everything chelseaandmadrid 2023-06-14 14:44:43 -0700
• c64025b1b4
  Merge pull request #67 from GTBarkley/leo Leo Mayer 2023-06-14 14:37:42 -0700
• 5035e6ba73 Merge branch 'main' of github.com:GTBarkley/comm_alg into main leopoldmayer 2023-06-14 14:36:24 -0700
• bdcfc9d821
  Merge pull request #66 from GTBarkley/grant GTBarkley 2023-06-14 14:36:20 -0700
• 1981cccbaf hot garbage test file leopoldmayer 2023-06-14 14:36:10 -0700
• 4690889149 proved dim_eq_zero_iff GTBarkley 2023-06-14 21:35:36 +0000
• 08b1fd3e7a clean some import chelseaandmadrid 2023-06-14 13:48:21 -0700
• 58140e01a9 quotient of a graded chelseaandmadrid 2023-06-14 13:44:23 -0700
• f5d4feccb1
  Merge pull request #65 from GTBarkley/monalisa ah1112 2023-06-14 16:38:05 -0400
• a62a8bfe4d removed two imports Andre 2023-06-14 16:37:08 -0400
• 80dbd2415e
  Merge pull request #64 from GTBarkley/monalisa ah1112 2023-06-14 16:33:08 -0400
• cf7f08df3e added associated prime graded monula95 dutta 2023-06-14 20:31:39 +0000
• 6379996b4b
  Merge pull request #63 from GTBarkley/monalisa ah1112 2023-06-14 16:30:26 -0400
• 0773a97fb5 reduced imports poly_type Andre 2023-06-14 16:28:25 -0400
• 3c4cfeab65 proved dim_le_zero_iff GTBarkley 2023-06-14 20:28:19 +0000
• 4e38ef0a73
  Merge pull request #62 from GTBarkley/monalisa ah1112 2023-06-14 16:22:07 -0400
• b5044e60a6 Merge branch 'monalisa' of github.com:GTBarkley/comm_alg into monalisa Andre 2023-06-14 16:20:58 -0400
• 7cec57bf56 replaced poly_type code Andre 2023-06-14 16:20:27 -0400
• 9667c3460c
  Merge pull request #61 from GTBarkley/monalisa ah1112 2023-06-14 16:17:56 -0400
• 009f768db6
  Merge pull request #60 from GTBarkley/main ah1112 2023-06-14 16:14:44 -0400
• 8f4fbccc15
  Merge pull request #59 from GTBarkley/monalisa ah1112 2023-06-14 16:11:09 -0400
• 99b06240a9
  Merge pull request #58 from GTBarkley/jayden Jidong Wang 2023-06-14 13:09:49 -0700
• 12e4802e51 added polytype Andre 2023-06-14 16:09:44 -0400
• 5485c26849 add more stuff poincare-duality 2023-06-14 13:09:23 -0700
• 51ecb4e119
  Merge pull request #57 from GTBarkley/monalisa ah1112 2023-06-14 16:04:51 -0400
• 6f6547c7a4 added homogeneous graded ideal monula95 dutta 2023-06-14 20:01:06 +0000
• 06e0227828 is there a def of graded submodule? chelseaandmadrid 2023-06-14 12:57:33 -0700
• e6e542ce4d
  Merge pull request #56 from GTBarkley/monalisa ah1112 2023-06-14 15:08:40 -0400
• a1888c51e6 removed imports Andre 2023-06-14 15:07:21 -0400
• b6ee56b192
  Merge pull request #55 from GTBarkley/leo Leo Mayer 2023-06-14 12:03:14 -0700
• fd6c8d2d1a Merge branch 'main' of github.com:GTBarkley/comm_alg into main leopoldmayer 2023-06-14 12:02:10 -0700
• ebbbfc88c3 added more sorried statements leopoldmayer 2023-06-14 12:02:01 -0700
• 27f3854281
  Merge pull request #54 from ssavkar1/main ssavkar1 2023-06-14 11:56:00 -0700
• c3472c9ccd Merge branch 'main' of https://github.com/ssavkar1/comm_alg Sameer Savkar 2023-06-14 11:50:35 -0700
• a3e4746b13 wrote proofs of 2 lemmas Sameer Savkar 2023-06-14 11:50:29 -0700
• 5db8e9cc6f
  Merge pull request #53 from SinTan1729/main Sayantan Santra 2023-06-14 13:49:06 -0500
• b9f64505eb
  
  Merge branch 'main' of https://github.com/SinTan1729/comm_alg SinTan1729 2023-06-14 11:31:32 -0700
• ae8bf07ee7
  
  Make the lemma names a little more descriptive SinTan1729 2023-06-14 11:23:29 -0700
• d4fef9c0e6 Finish all the statements!!! chelseaandmadrid 2023-06-14 11:23:01 -0700
• 01ac7a2777 Merge branch 'monalisa' of github.com:GTBarkley/comm_alg into monalisa Andre 2023-06-14 14:22:27 -0400
• 88a243d26d new homogeneous monula95 dutta 2023-06-14 18:20:41 +0000
• a2f481c7db
  
  Turn some simp into simp only SinTan1729 2023-06-14 11:12:33 -0700
• 50515d9ed8
  
  Completed most of the simple part SinTan1729 2023-06-14 11:02:02 -0700
• 8892567285
  Merge pull request #52 from GTBarkley/monalisa ah1112 2023-06-14 13:55:00 -0400
• 40fc5871a9 Merge branch 'monalisa' of github.com:GTBarkley/comm_alg into monalisa Andre 2023-06-14 13:44:13 -0400
• 7173aefe8d changed type of 1 in dim_le_one_of_dimLEOne GTBarkley 2023-06-14 17:43:16 +0000