b8c986d26f48e4d32b798e0bed1ffe453864b8480c6bbf9d73c2855fd6b99a59  check/AuditCheck.lean
71d76eeb71899d6fee5b2fb9c8237e2b2567e44175696360e9e3fd00648c51fc  check/AuditTarget.lean
8d763314cf6da185aa662c4ca30f11e30127b4eeb416c2ebe85180804e55692c  .gitignore
f6851a00c9b4e85a8ab6aaf119ba5049414b21bc78e046a68fcd56a441e7bcc0  Hilb3/AxiomProofs/CILength.lean
c2790973d20d74fe34f296c3eddfaddd5df105e979c5d5958360c20b055c0c26  Hilb3/AxiomProofs/GorensteinRay.lean
ea766198212577a6b026dc0d3f1ce0572f6cacbde1bbdf5f56c0fb980b6e8945  Hilb3/AxiomProofs/Gotzmann.lean
1161ad0b9a135f166d38adf80b3ac928df38e5274ca2d9435883957ee9354e03  Hilb3/AxiomProofs/JRSLinkage.lean
ca6354238c9f48943ab2fcb339197f3d29ce91a493f8688ecf0a97d56523f178  Hilb3/AxiomProofs/LinkageExplicit.lean
13281986648f09c0e765188def2f07ff296fe65e4521ef9ce41314270ad01569  Hilb3/AxiomProofs/LinkageFamField.lean
a20a1881acd68da06c5bee31f45a411d3d34ab08af7b2c46b1b3ee7f62a59c95  Hilb3/AxiomProofs/LinkageFam.lean
0c15e18815f212950c95a633330a67fbedd43522c14343ee28f8925008c0a07a  Hilb3/AxiomProofs/LinkageFormal.lean
cef3a413325e73226ae40615a71f40358d32020e2b56d34b001000506b851199  Hilb3/AxiomProofs/LinkageGeneric.lean
e9fecbeaa4911f14569edd880108164d237d01084591c9bf49d92cb56f153005  Hilb3/AxiomProofs/LinkageGen.lean
770886f4469fbddbad2be6a242ce82de65a8d53584efe08be410ccf82cea65a9  Hilb3/AxiomProofs/LinkageGrid.lean
3071b28cf52dff7c4164a2f24f5f6cd8e4041cac823f831b23c97b86ae257434  Hilb3/AxiomProofs/LinkageNF.lean
3199db68d58c9f638e453703d4ab58375f20268b19db09425f019565f94fc3b4  Hilb3/AxiomProofs/LinkageSpecial.lean
0ceda4e24b386c1065dd4af328427cab7555e043905aa180f8f45e2d9ff926a3  Hilb3/AxiomProofs/LocalAtPoint.lean
439043395578cccd3c2f8fe461cf1771dfb39616a70bca8a7135df2e104d4872  Hilb3/AxiomProofs/MacaulayBound.lean
b9e6cbfe692e2be99a27e26f3a5eb684730c9c9dfca56589485318c7f35a5837  Hilb3/AxiomProofs/SmoothableFactor.lean
02c63a1544a45e81f4397306c8ed1224d84b30d72036981f00a019a093e46121  Hilb3/Axioms.lean
2bbc8299b1a5dc168070da6da8a924d1a28859ccc05a5c39c334adf78b1e05ef  Hilb3/Foundations/AnnGorenstein.lean
0bf6638d730e2f89d277d0d771cef7e14aeb49f4607550fccf088cfafdc77844  Hilb3/Foundations/Artinian.lean
f11bbeed2b8f137918a553e93258426de8acc2f2b9df1e63bf123265956179f0  Hilb3/Foundations/CaseSplit16.lean
8ff1c4b6dfb62505119c21d7022ae4b5594099b1a86359f9fd6b3856f6dbc7a0  Hilb3/Foundations/Dominance.lean
405032fc287084170177dfbf358846040a44ce81c4083a58766dfadeddd81790  Hilb3/Foundations/HilbertFunction.lean
c4e153f8e8cde6088a79af8967aaa9c39ac0601c1aa82cdd14fefb4d05a3df60  Hilb3/Foundations/KerIdeal.lean
dbaddaa04aa2e7828fcd1f636d46c12f5959e1d7b1aa5314a8d370d2b60cad05  Hilb3/Foundations/LinearChange.lean
1d4b2aa13b9830a5139f3999d20a475446d694ab7b7c15d2d253461951c70b12  Hilb3/Foundations/Local.lean
acc465e9cd68f4551ea7c88b37b9b8bc07146655f6f79c93dc1481574eb28b20  Hilb3/Foundations/Macaulay.lean
77914dc977b77a931f57c14472eb926499ccc9eb2a34d6c621f8614a911d671b  Hilb3/Foundations/Triangular.lean
49dc98b13716ab87ab7f7bf2d5483f5ec32a117e2e113acdceb06613a2d93b48  Hilb3/Foundations/Zariski.lean
e6974b2201ab3d808db984b308cfe2a2bbef3fc0f9d6eeb006764956164abe1e  Hilb3.lean
29d17c5c42c16e6e1e155737f55cc1e6590347011e0bbc9f5ed36000c8b2b582  Hilb3/Linkage/Case13641.lean
9cd0e65fe495e9f2e340f6b8de674dc4426d75f57dcc20865b9d59f9c6cb7ad0  Hilb3/Linkage/Case13651.lean
8270ea4f7a66643a8a4d3ea88ea199e6b46743c60a6b591f98950d22ca4e617e  Hilb3/Linkage/Cert13641.lean
32bedaa05b14771584c8fe073c373deb555fa58f34c936997735c1fdfa2229e4  Hilb3/Linkage/Cert13651.lean
8245b0edbd774745c795e9ddb2b5ee2bdea51f212cb3277188eeafaaa5e459fd  Hilb3/Linkage/Chart.lean
a27bd5343b987b3d48f717ca736c0cb5649715b11f3b8eb3f64315eff5f65a27  Hilb3/Linkage/Cross.lean
277c192cfeb83c20865dac29d52cc0a3051cf0e2b18a452d89fff5dbb1769ffe  Hilb3/Linkage/Cubics.lean
0d1e7e6b985e7640a8aba81222c8f5bc7655f49d0ae680f8faf6b6a2cba59bc8  Hilb3/Linkage/NormalForm2.lean
d1a12139678d24be9a6340acdff5d85087ffcc5d7feeed8e5eea856983679041  Hilb3/Linkage/NormalForm.lean
8cd043c44bdff85baa11d33b88f97cbfc15dd74e0a57f5555744d81502f68b34  Hilb3/Linkage/Rank2b.lean
9d49f367c7aeecc0b1a57571644519da60dd02470f7d8f6c1da4682cb08d2702  Hilb3/Linkage/Rank2.lean
3b4144b455a65a87a3f7cd8dc477366667a5eefa463066479341149cd1f272ad  Hilb3/Main/B12.lean
31d385588953277b0b81a9227bb3626c6893d8feb73f91e201561d2e146529af  Hilb3/Main/B14.lean
1f26699f069b7b320ec441b6e2a5cc057c77645a39b817c20a9b29f05fc54c6d  Hilb3/Main/B16.lean
c72466dfc78d5ab01c51ad3784d62bbc1586d6083b5942a6d2a80e0191ac9267  Hilb3/Pencils/Case13632.lean
098b1123dfc8f947a181b0196acebe5e0b1bf1ecf39ef3d018d8d361b001eb37  Hilb3/Pencils/Case13633.lean
25550bfaa8eca2a26a50b46322727120c736408ed4a934d0e7b9567d7e9f60a8  Hilb3/Pencils/Case13642.lean
1d762fbfcccc18c90db961b9998a1cf6a193c46950eea0461a1dfcdb590f6f7d  Hilb3/Pencils/Case13642Low.lean
88625da560891ee8afab03391ac7fdbc14ffb080ee97cdcc02c9ea29f215f38d  Hilb3/Pencils/CaseConcise.lean
77663d534183dc9c86b27bd708139dafdb68689be5eaaa5cd79366aad5bb3a17  Hilb3/Pencils/CaseFourth.lean
79e9c3cf4db220541699569cdd3d2987a79b61406045d10cbbe9907b415cba33  Hilb3/Pencils/CaseNoConcise.lean
08880e0597355ce1d874d8f93d85e2d3e9ea0b51c41b75f49661a80d13848d9d  Hilb3/Pencils/ChartNC.lean
f706ae25d52dfde2349daf525375a22797d86ce020be299f25d61a59a5832eb0  Hilb3/Pencils/ChartT1.lean
1cdc4153b9a95bd867f5656b7160b68bbc38084d0fc8877c09765bdb1c634e30  Hilb3/Pencils/Coords.lean
4932c4f9ae9632c2088e1fc42264702928f7f069e0a55aa8b49f9742f246033a  Hilb3/Pencils/CurveFamily.lean
12c4eeaeabaad7ad8deb87df35c7d032e028863cc7cfda99d7a5df3c9445d364  Hilb3/Pencils/Curve.lean
ad6b7a327f01a1276e7b304cf9bd172e4e5b89178cb0e9e7c0f117b87846f498  Hilb3/Pencils/Cyclic.lean
bcc684912fc90c1d8df2788ec0952ffb2fb5d378240f562b83142c59af7c11ba  Hilb3/Pencils/DoubleFat.lean
36a8ffdd1aa1b58da97e133c28689d0a2127a75e1a261ea66ccf5266ec19ccda  Hilb3/Pencils/Family.lean
2fe690dafcae6eec61d9c54ac2116859096f5d8bc3260fe00aace11d179fe6df  Hilb3/Pencils/FourthPowers.lean
6e361588851b7b08ee1aa43df3ee6b12e2f2f6c36ec4cc40d4b65611dee53837  Hilb3/Pencils/Line.lean
ebdf48e157a38c0bb3a9f94d53f21cc4af88d1c59f8197b47987c78b392499a7  Hilb3/Pencils/Net13633.lean
dd8af4773c902fd89b0c7fc49953278f0c46d293647a49b24dd1f1585530db2a  Hilb3/Pencils/PencilChart.lean
4eff7ed110a61d130aa2e3775a7777074cacb50c40e492876680e3c1d3b99bb4  Hilb3/Pencils/Recurrence.lean
d9789a026ebb57b59ff0c1056b16068f5e8e1203038967fc0f6a3650eef3e09e  Hilb3/Pencils/SPrime.lean
e8794da5dc1c372ef1b0c82a2017b06435e1595e52d2c97190e021708a5be788  Hilb3/Rays/Case135311.lean
1b09120db456aac61806b72926e705b92cd3f9e6e1b328c584819e865d853d76  Hilb3/Rays/Case1354111.lean
ea041463ab02aff3ecbbe64ea5bdc1d4d53e8882b172258526311c48e233bdff  Hilb3/Rays/Case13541.lean
73d77064376b7379a540b654cc2217caa141afa802a6c3ec3880c59c9f8acaf2  Hilb3/Rays/Case135k.lean
b4f45cd64f06bfd8d4ae04b7d5e3a85c33c52caeff3803ff6e30e118d5eb5f41  Hilb3/Rays/Case13611.lean
f85d61916818d3d885c445dd27d332c63ec21de05ae282bac8cddd607f49ae88  Hilb3/Rays/Case13621.lean
8b0643becfa7b9a6782089819e314882bb73f5ce618109fc55a9be8d1b9bfb19  Hilb3/Rays/Case1362211Family.lean
88480c447c68ac1da3183b4db19502c2e4bf1e48296c59cb1c254070248d2c5a  Hilb3/Rays/Case1362211.lean
51e7e8d4bd502f0acca6cefe3cfb3a773a39625d4e3e38e21e1fc2b73c1d03cc  Hilb3/Rays/Case1362211Two.lean
ffb3aee7a1ebbf6f56944f69898bbbb349dba0d99a4a6ab933be3b9e7d1078ad  Hilb3/Rays/Case136221Double.lean
3c097cd29e8cf0a5595318691a6aa7ff5cb1c2b139e97125633c07a9b4476ba1  Hilb3/Rays/Case136221Family.lean
0a915b907f89d37d43479b6142fdc79aea70e92c632dcacd5bf9507a0db1676c  Hilb3/Rays/Case136221.lean
ca87c267cfe06f7b7f3a7e02a3be3d5c9c37356e849d7c2509f617c4430968c7  Hilb3/Rays/Case136221Main.lean
a4bc72ea96edca80d582496782cf536b56af2f8349da22107efbf670ce05fe9f  Hilb3/Rays/Case136222Family.lean
22f134d1f5fa5d2daeb44a7ed0bd5f693bbea5371aa2bab9a3461e0966ce3ceb  Hilb3/Rays/Case136222.lean
ad8f27608fea5e8c48bd499d652eff1e8c0fdc08d6a0f03f068b56ee2d1c4211  Hilb3/Rays/Case13622Family.lean
3418d35d5a86e3b59d11abbafba654e8730c9b4e46e61ae9088d83bf05c2fd42  Hilb3/Rays/Case13622.lean
cbfce5620217cc58fc9fe3642d2be5c5b84882f8c5327a3db8f1cedad47e2e9c  Hilb3/Rays/Case13631.lean
e5b03961cfae577dffe2dd3ff47f14ca60582b73f2d335d2c6b23d80f82ef79d  Hilb3/Rays/Case136321Curv.lean
d07901b45d8d331e0323d7a6ceeaff5c33c61c9fead2e195f3c6062a8818a715  Hilb3/Rays/Case136321Dp.lean
c9755a57aad235132cd20d9a90b1a1cb6958fcd0aa8533a37b7a1f73117064f9  Hilb3/Rays/Case136321Gor.lean
8b2d5895b019eb35a059b0ececd1fc04f50188f9d4844d3bc9e2fb03da46128f  Hilb3/Rays/Case136321.lean
be055216dd6cdf4279de07e72b9b050e114e0c845568b0577b390cdc90f0af73  Hilb3/Rays/Case136321Normal.lean
7715d0fc2d5c6ce7a6302f98bde9dc76b8f9839826ca6cc6eb512f9747949dd8  Hilb3/Rays/Case136321R1.lean
cfd48aaaa69e0c382b2aa6d33cd6e08536d325ccfa9ca00b6c08a58901d1a83b  Hilb3/Rays/Case136321Transverse.lean
286c403be938fd2f3765916c2bff41744392b1a74455c634bf605f62fba5050d  Hilb3/Rays/Cases136.lean
bda94a0191c6dde41415be291faa1d3ceb19c8dd68a6a6ff351de74702ba5d23  Hilb3/Rays/DiffQuot.lean
0bf23bf273677d28f1cb50512db98ae1f4dea12cd5516110a44f0aca55805145  Hilb3/Rays/Family.lean
cb19d73849ee49cbb0b507b3d0306b866aba9a0a57b3ec6da27e2647056b4630  Hilb3/Rays/GoodPoint.lean
c9f83aafd5fbb3f90fbd2490568de5f26942c050ed8890c8923e4ae1f9c251a7  Hilb3/Rays/Helpers.lean
8d089946b10dd1028f0e8b9633d3b6f3a79464d245a05cb222e4a0d206afe30a  Hilb3/Rays/PencilAlgebra.lean
c1ae7dc6fc2933182b414e371f055691f1c4d71671c54d397bcdd80be36398f4  Hilb3/Rays/Pencil.lean
d08b301bedcc13c89967c4d1be889078aca363c3d01135d8dbea779b6d85bba5  Hilb3/Rays/Socle6Ray.lean
8cf92787f632fbc2e5ed58342e7b9ca6937f2db035bdb2e3196401bd695f9645  Hilb3/Rays/Tail.lean
6522223155215aee54cdcdfaa7c5263468bb551c29b24a3f408e50a83530ff3e  Hilb3/Rays/TwoPointsM6.lean
2c7df2771fd08da662763b8c84c05cddb615a680a6c6dacd379f288f25e36c7e  Hilb3/Smoothability/BaseChange.lean
3f5bf6b4fe7640def3c5e93330dc2c93422de57ddea02ed82b0308cfa5163a24  Hilb3/Smoothability/Basic.lean
bc04804ae1f195b8ad35cac94239d003ce3ba51be5d8fdc8af973de42721bb8d  Hilb3/Smoothability/Curvilinear.lean
618915d7a89912df3ce1e18c2d2b0867b4970cf4b5a9a582717cf38f3a031360  Hilb3/Smoothability/Defs.lean
7bf47c2e5b3cf4c684ff6145527a80c7c4a123f00acea84f5d70e9f411a1df7c  Hilb3/Smoothability/Families.lean
f2dbee6bbc74005c2501619d4a6b89099a39f286f48c188bc7cafa2db4de541f  Hilb3/Smoothability/FormalLimit.lean
ac753d51f6be78c59b2ed324080ab07de023a96f19a974a0f1cf91ffcbc66dc9  Hilb3/Smoothability/Pairs.lean
cf2623a878d657990889fec153191991b7408c973fad172787763c2c0d80e878  Hilb3/Smoothability/Products.lean
35fc7554ac49dd3fe8f100812c9ada77c5def87c688ce48c9277fc27ae288db7  Hilb3/Smoothability/RatFamily.lean
5ed60c660aca3c7eb54a6c3ecf0eb51504b944aa4da96d14d64657190058be9b  Hilb3/Smoothability/Reduction.lean
0f7e6a181cd9bdd131a9eef9e342cc6c57f3b5f5dff0cd367c67131f497d79dc  Hilb3/Surfaces/ADE.lean
6b7d2e9ce1d65fcc028e112d60263c5738512aba8b550b8c99b75737b95dd702  Hilb3/Surfaces/BinaryForms.lean
4db94fffed7acdc532d8d7ef888194b39c8827748264b9f6d5f207ebd9e434e6  Hilb3/Surfaces/E6Pencil.lean
e0adee8fd5ea88b5cadd56e51afb4777bc7a157d3aa483afd5c89d1718f3f29e  Hilb3/Surfaces/E6Scaled.lean
57c1459432a396258fcac3f7ad6dd5dbc092448cfa2b10d7371d3422ef3dcd6a  Hilb3/Surfaces/NormalE.lean
ba4dae53f84d1538c000fb986394f2b89a5f69b4f5ce495e62680bb294149b46  Hilb3/Surfaces/SocleFiveGen.lean
6218121078c450fff5ceb7bd8ba97babebbb22821a1ebfb1a7a41bbbedc9f8c4  Hilb3/Surfaces/SocleFive.lean
5473a83d374d8e90f09a7584eee7ea46aaa35130d97c17bf8082b8c283e9206c  Hilb3/Surfaces/SurfaceCriterion.lean
7f5daa73f6fcf249fff8eb3a6d0c298ae1f5ae8d5d1847f1acb355f356bd8726  Hilb3/Surfaces/TurningE.lean
b36be09dddbc9860aae21752677e8505a0078882ef32596bdb851f45019c8113  Hilb3/Surfaces/Turning.lean
7c0af448af6933ce277b2036ac1181ff9785217b49626baebc5e6c9325806f0f  Hilb3/Surfaces/TypeA.lean
b38171806274da85c751dd45f6952c3b42dd1e9082c585e65bed7d52b23a6914  Hilb3/Surfaces/TypeDE.lean
2b4321c04192b292d47575c1b932cdfab31dd27ead39ebee26eb6c9f1fe9d0ed  Hilb3/Surfaces/TypeE6.lean
6b709bc7ad87f1fcbf043b37fc54cd77ff41b890a46cff19f3769b18af19aec1  Hilb3/Surfaces/TypeEFamily.lean
1778bfc5ad44f0dd529bd5c733d19f133c6ecd717b3b2bcece22248e149fcb93  Hilb3/Truncated/Basic.lean
5ec5d2cd6151d4e9b9cb917c071fc387c06f4b4d8d6c8926bd977d7fae49eca3  Hilb3/Truncated/FactorLift.lean
c7d415f31aa7fdf38d7e3a42aa92f5da8c6c617b521ae9c447bd9a36f1981488  Hilb3/Truncated/Hensel.lean
4eacc4e2f0b745124cdbb199d11997fc246ea4316721c2a901617be1c377a439  Hilb3/Truncated/Splitting.lean
6477433b40cbc31417cee631d379806b69eeeb307eb0c8e0ec1e450a8b0862e0  Hilb3/VeryCompressed/Cert10.lean
5055d6da47acd95094fd3d0f4e8a82d1570903a3f851ca1554b3fe48fbb0faa1  Hilb3/VeryCompressed/Cert3.lean
af0faa6c4c690911787a6e2a8709b914ff3a1795e93e9ad117ac54c0b13194d6  Hilb3/VeryCompressed/Cert4.lean
22933b347d8a7c4cf04373756aa45e15e0fe687eff8cff349c6f854b8b578e7c  Hilb3/VeryCompressed/Cert5.lean
3d81d968b4d9d5bd096e72f0c479079294a13398c2a3e069498cf495fc5c6c84  Hilb3/VeryCompressed/Cert6.lean
fcb617729136900c2af26562ee101139ba98e49053d3d3febea52b30a0bc1f06  Hilb3/VeryCompressed/Cert7.lean
8fbb6f3f9d21f0a50116e03d8d8d6241f07f09ab4875e1d022c448b1e94987df  Hilb3/VeryCompressed/Cert8.lean
5fa1928397fbe406eccf2e7948421f5225c9babcc2b7e6912b980cb62e68b643  Hilb3/VeryCompressed/Cert9.lean
27994dbb86bdc7a4c48ff1745277fdef6138f50772a3587ffc9d5753281b2f04  Hilb3/VeryCompressed/Cert.lean
fc1d8ea06f54532e69df7760a768eb666f6f4736e0028bd0a3e9b38741fcc3eb  Hilb3/VeryCompressed/Chart.lean
e52e60add33c1bc50a4c266e24c061f292cb61fbf83d504416eb4e53b5aa57fa  Hilb3/VeryCompressed/Derivative.lean
51dbba675bc50293ee2b6e8622566b339866229f6af58af875241ae8887c9e8e  Hilb3/VeryCompressed/Functional.lean
c69035a66360e092ef27cb8eae8dfc303bbd0bdaedc8b768097fa3712b04a6e9  Hilb3/VeryCompressed/Main.lean
e79b05211ee33eadf1ef775249fbdd6c8757dfe86ccb3e2ba679ca070951aed9  Hilb3/VeryCompressed/Monomials.lean
5fa59a371ac8c8461b44bde9bf8c2e7d6eccda3a9adc136adc2751a0a344cdf0  Hilb3/VeryCompressed/Points.lean
bd3ce42dd987f35e455c92dbd300d8085721581925c435c5b79664949d4e83c4  Hilb3/Zheng/A/Classification.lean
110f483d1684940a36f3fd9c4b4fb2df0cef135e7023ff766d40835bfa6c8eae  Hilb3/Zheng/A/Family.lean
5535cd906621c8503bb6fdb6ca464116a1fc88f34d33a81a0534c6112e28bb94  Hilb3/Zheng/A/FreeSyz.lean
4ec2efe06f9d133bf224fd4a0087340d2ba483280245aaf2f3608255c0bd3a84  Hilb3/Zheng/A/Main.lean
1a695e93372f0b4d5c558d440736b7179a721b26f6d10fe63169020876500c8c  Hilb3/Zheng/A/Move.lean
0c0c365ab63f478193de1843523f9883aa31b826e7a235cde48c09f8be984882  Hilb3/Zheng/A/Presentation.lean
4b01eb7f46e4ca9eec7248b75393599e387780da512c26be3485d6f7e32c4a7d  Hilb3/Zheng/A/Up.lean
c8b1561d8f3b217c2ef0ae537384c3f13f778a24b4b910da7472a1fd81459e5f  Hilb3/Zheng/A/Weights.lean
82fde540f986e91b81f2d143cbde2df8e65e5457142f37c87362491d531908fe  Hilb3/Zheng/CovariantsA.lean
8291e2a752130dbdbca563b4360fa61b9e4cee6e1a76d8d9fad585ca97f374ce  Hilb3/Zheng/D/Classification.lean
5790b89cd452346dd649af02507188be690600b4f0ca3e91dcfefee11e8a3d34  Hilb3/Zheng/D/Generators.lean
8a5c2a65719f41e44f17b651a4e7166a884f3cd7c66de464cd1a16642c541c29  Hilb3/Zheng/Dichotomy.lean
389a0fcf475b52412fce7ab0a11c09e09aea7fd11fe70b46c9538d100be68d95  Hilb3/Zheng/D/Main.lean
8cabda3b4078ea34ab7ee70a42649030f37b42c4e88a8b29f599715d85b01eeb  Hilb3/Zheng/D/MovesL1.lean
f9910d7a98c216687d783ffdf1fca2ecb8fd9afc68e32fd42c3fc705cb8cbe93  Hilb3/Zheng/D/MovesT1a.lean
dd67ff36ec7b087e3c67685a998eece9c9b2c9b5ab812553bc7e6b8c5c1cf246  Hilb3/Zheng/D/MovesT1b.lean
efc07df6c44942b7c7680e0087c883425a083256f9c753ea64a1bf6056236cef  Hilb3/Zheng/D/NormalForm.lean
6aaed3eed24a6ac15a0706a2e51c49400f28fd70a848d063bdc7863d613c7cad  Hilb3/Zheng/D/Potential.lean
5cba731576af63ca9860e11a9c923920769f160467200830e9c94305882d0305  Hilb3/Zheng/D/PseudoBlock.lean
f01908a9138043c349700cb2411210e102e23f3a2cf630a164b581cf002661e6  Hilb3/Zheng/D/Rep/Basic.lean
f2b54a55bb69ba5895ceb721c29f088e4e8b41fb12c78673bc8e306fbca13261  Hilb3/Zheng/D/Rep.lean
958f5859be21a20854daa4b79408d93905bd2277700a898f901b3366c1ab06c7  Hilb3/Zheng/E6/Classification/Decomp.lean
0c2671e7a7a23b220d4451e922f6e04fb24a258f807218f9ecaf590a97da5f9b  Hilb3/Zheng/E6/Classification/Frame.lean
69c669bd2c3abd3c06c4cd5c15bea3d1f57f112f2b1fe9b6aed2198d8dcab039  Hilb3/Zheng/E6/Classification.lean
651fd6b053983af6818c9de33ed6747aaafc3ab3a960f83e654c41b9d2fb790b  Hilb3/Zheng/E6/Classification/NormalForm.lean
9ff367a94041dd035db1d5e3842403365a04dba4c6b20c512fc2af81560f609a  Hilb3/Zheng/E6/Classification/Residue.lean
2f6e3f59b35bf8c4580e9f56e9fb127d0638ab732b7efdcfba53e951c16b9adf  Hilb3/Zheng/E6/Final.lean
4b80ac423ba5c96a3d45a85b5d3b589b2523255342670d5a7df4fd3179f9a7c5  Hilb3/Zheng/E6/Generators/Basic.lean
c6bf5b6b9c97b4a0c7286d853f3bd4a0bd6a9a61a254d7f0f983c5702d8276ec  Hilb3/Zheng/E6/Generators.lean
602bc4576b755e0f30cfb23609b73767ae1bb7c3ea19aa75febf37795e8bf812  Hilb3/Zheng/E6/Main.lean
7992be3954d08afd2c72b801d56e2186e5c55d3b5c300aa4d06e87f7f936bee5  Hilb3/Zheng/E6/MovesAR1.lean
ae886cbd6cab8ead91a8f56745b2cb51c86304e244095cb6aa81a39d92b44fd3  Hilb3/Zheng/E6/MovesAR2Data.lean
d20f4d9f2c1a8ea3887c4e280d5159f293f16037db47ab66f044a269a40e5515  Hilb3/Zheng/E6/MovesAR2.lean
81a7044a614868e5d9845c794e97d7e216354354c753b689634378466ac00d9c  Hilb3/Zheng/E6/MovesAR5Data.lean
679ca66bf63204d0e14eafb595b994a0ce682342c37e981e682a4ba73e48eece  Hilb3/Zheng/E6/MovesAR5.lean
16960dfdb6aec9b0987ce98ac78cfbf1f9505fad4b1ccbebbd28552a1663e95e  Hilb3/Zheng/E6/MovesAR6.lean
aab7ab2e659d7f93ab4e19ae6ac12288349cbf9d803f977b595ae01ece14dfab  Hilb3/Zheng/E6/MovesARBasic.lean
c582ec4553a363cf3d7ea0514b43ccdf73e468ff8610a766a656a827df01e831  Hilb3/Zheng/E6/MovesL1/Basic.lean
ba6d80c96eb7e67ee6d8d6a33bb9b2151508fd589d01201e4a5c06ef11232b33  Hilb3/Zheng/E6/MovesL1/Gens.lean
3d869ff010470214d06739e2a70545b2ad4d0e6f3912779142cdfc17e47f980a  Hilb3/Zheng/E6/MovesL1/M3Data.lean
1886124884ab422f4e54c571cde2026cef4265bc562c27b9944398ec128e6312  Hilb3/Zheng/E6/MovesL1/M3Dual.lean
4d7d70c7edd6c2875100fc1b53e6df433f53b1fbf5f8e3502fec9855915b9ad8  Hilb3/Zheng/E6/MovesL1M3.lean
b7219f4be691eeae574038d376379d5319bdcc1682fafb1917c9d1a038e8465e  Hilb3/Zheng/E6/MovesL1/M3Push.lean
2d231c02b8736f17c619b2f11d62d8a48a3b6577adcc5658e79085845acdda3b  Hilb3/Zheng/E6/MovesL1/M4Certs.lean
43a51ac4c17c2a1c71f2186778f111df64da8cd8a5eee14d180faa03036833b8  Hilb3/Zheng/E6/MovesL1/M4Data.lean
07b71fde5354bfeb0bf85c41a2393d1b7368ab09102958da268b98839371afa3  Hilb3/Zheng/E6/MovesL1M4.lean
de6e23ce12e5bb773fb88d9275d8ee22c9e77109bbaafb004cd0e4a1f84fc382  Hilb3/Zheng/E6/MovesL1/Reflect.lean
6b8447fb552f88d02e923d4d2ee7663ff150d1a1ce671c9063aaa4c39ebb53e7  Hilb3/Zheng/E6/MovesL1/ReflectMat.lean
0af17aa1169947e05f92d2d45e4a84a75d25288ab8fc6e663a3b14ae3ed81628  Hilb3/Zheng/E6/MovesSyzLad/Basic.lean
d22443104bc6e9cfa123a1b2111dbbcd6d11e61eba0aca8c32364bd439b6708c  Hilb3/Zheng/E6/MovesSyzLad/LadData.lean
7af855b7c243b9af3315bf46ed2d8fd25e1590f47611fcd95c967bf10ca9c322  Hilb3/Zheng/E6/MovesSyzLad/Lad.lean
939cb25657aaf0efcd83adae0b534f35c9b69b4b23ce3c883ce90bc1b648ceb6  Hilb3/Zheng/E6/MovesSyzLad/LadPData.lean
32401b45003036abc62639d4c54d6fe5e5e304ba56dcd8f8dcc2a5e35fa44146  Hilb3/Zheng/E6/MovesSyzLad/LadP.lean
977443af9273397b757b816725a766e3ff0b83684ccc54caed800a97b60fcff5  Hilb3/Zheng/E6/MovesSyzLad.lean
93cb1291fff1bbbdc270d81b9556ea6df86beb2aba199401ea83d85666c0eb85  Hilb3/Zheng/E6/MovesSyzLad/Syz52Data.lean
c516e7aed7fd0be57bfae413f6068c99de01ab1ba763c54d5dc86a6f88003325  Hilb3/Zheng/E6/MovesSyzLad/Syz52Gens1.lean
a736b26d2c457bb310d1bdd6677e67ddb3c6808e7becb0006fc19cddc82eef1f  Hilb3/Zheng/E6/MovesSyzLad/Syz52Gens2.lean
8b1068c862c1c7654cc437e77906d09ae10e545e58eb1f3609f217a5e2337709  Hilb3/Zheng/E6/MovesSyzLad/Syz52.lean
7021a45e1395ade1bc09c1adc3611d8b8f6272ca4f8e1db6cf7ce19205d01698  Hilb3/Zheng/E6/MovesSyzLad/Syz52O4.lean
4d400f2c3a2286059462e9b2fab814efb4f5a5e5e4430b73f4aea4e14429f1d9  Hilb3/Zheng/E6/MovesSyzLad/Syz52O5.lean
4563127234f2ea24ab75425e8350704559b66ace0e66504b7e4641fd14241307  Hilb3/Zheng/E6/MovesSyzLad/Syz61.lean
cb7851a0955074c03b8c3f8de7c61a35de1cb61944805acf49dbdc4fb94db773  Hilb3/Zheng/E6/Potential.lean
781ed1373503877ff6101311922454278802392374f557bd5d6ef346a291d916  Hilb3/Zheng/E6/Rep/Basic.lean
9477309a755f31708274d5470b641dd43b1216a9c858ce6eb4656249ac99c3c3  Hilb3/Zheng/E6/Rep.lean
d87443f82eb4ba01d6514291712e0e756f1555c82cba2765cf145fc41fa4a327  Hilb3/Zheng/E6/Rep/Matrices.lean
cf6974c55d50b552720e5864517746bd4e6b2c7388176733af55aaaf984fa318  Hilb3/Zheng/Family.lean
6f4029cf8421d72cb5476da3b506f9c86637abee272f179d31ef9957b760eaf1  Hilb3/Zheng/FlatLift.lean
6ee7e86e32d0ec7ffd064ba3fb09143c53259227301ec62a02e8c56ea9710ac2  Hilb3/Zheng/FreeSyz.lean
c631b567476ee1e69d0d90e68909506b3b6b99e42f65b473db4416046d9692f7  Hilb3/Zheng/HilbertBurch.lean
1dcbb25e65d5bb6adabe7d60b30720ba8f11d45dea31815809c7e389cd82675b  Hilb3/Zheng/Invariants/ModelA.lean
ed17cc61781142cd39461a2473d3f334f9fcf83f4ae5c1e81c8d416967964c94  Hilb3/Zheng/Invariants/ModelD/Basic.lean
4365541982b05cce2c0b55bc6c89ef008875d7873e6711041549b59d57e94b58  Hilb3/Zheng/Invariants/ModelD.lean
815756d2338cbe584f4d138c3d9e3fe864ed6725b6e8bae9b1ed156f564545b1  Hilb3/Zheng/Invariants/ModelE6/Basic.lean
e7a1da94f4e0bc6b9938c4b6da679d2a199f7d7e17f515633d8f470d5958a269  Hilb3/Zheng/Invariants/ModelE6.lean
d4a651383be211e8f16f09a82a5cad77d364b28a6245c5f62c6455ada0fc9b3e  Hilb3/Zheng/Invariants/Reynolds.lean
ecf0d97825fdc2800580dccbd4cd29ae40d9933a05449a09000a3174d796af77  Hilb3/Zheng/LocalSyzygy.lean
de93c5cf6f076b5e12e5fa76755fa685a586739a103c11811f4009a047a6e73d  Hilb3/Zheng/Minors2.lean
a0b90b70729a68c834d81998178d1a0782dc534c68abe724295a196b9a1a0186  Hilb3/Zheng/Minors.lean
2aa016b248da0697bcc775f295f49d720b2d18d2280c48f96ffd6b61f5cd157a  Hilb3/Zheng/Model.lean
92cfa53093085d6b043f826ee3731d6a0e7288b392c35b07a0a780551457e98e  Hilb3/Zheng/NearPartFibres.lean
9e57d85410490c78e2c87c9707dc49bef54d587f1fc45b208476dfbe83dee158  Hilb3/Zheng/NearPart.lean
d47f1a9a3c48ca7b7416f0b6dffa2db37d06f43fcb71df040e345d7fe14469e6  Hilb3/Zheng/Pres.lean
6cbbdb033d3f9ea09ed2f51300523b4c9fa0715bcaaf3aad0b0ddb3e4756a9a4  Hilb3/Zheng/Reduction.lean
c9dbe830422dc72059957e28bf5e7764e5d18438f2f31ec94a5f4dfca2adf329  Hilb3/Zheng/SubstL1Gen.lean
41467126736737be662ad8a0b8a22afb73e6d3931b6f8a53a5da42c1cc3e602a  Hilb3/Zheng/SubstL1.lean
d7aa3a669a044de3e1725d5493061e10f7f406ae9c9ea93c8e9d73b5aec4b249  Hilb3/Zheng/SubstMove.lean
90fa27644e4d968ab9a5d1eb13854a6e2dc92f75b48371a8879541db44bb43db  Hilb3/Zheng/SubstT1E.lean
82ed82f2135b1965557fa6de68c227b2351cff465a80efe92b4a046d8536ab90  Hilb3/Zheng/SubstT1.lean
706677061fa91cf038336d209b614f4adb5583bd9ce9a00aeb1cd1adea3bd8df  Hilb3/Zheng/Up.lean
23bbc7c78454c57d0e58a2835006c9522b96c4143c14907bccfd8d3c85a1997a  lakefile.toml
5a43f8cfe231742c7a9282383d03aac7ca3db03af186abe046a25a01ae22abe1  lake-manifest.json
8733782dc070a99b312039cda424f601b80f3be6f6f512627da5ba25adc27632  lean-toolchain
091872374d359a3a63f2b619ea9d6f5b281d6e771c9389a60c7de60c749a5231  LICENSE
6a4b03fa3373b082e6ab34f20f19e5ac8717d2eb34d4f63383735ca1dfb23c11  README.md
1931cd06704e6d5d2afe4cc6bc5f0075e3aefe86a960e7facc27a6f510e43cc9  VERIFY.sh
