GitHub - Brian-Nugent/RegularLocalRings: Formalization of regular local rings and regular sequences · GitHub

Name		Name	Last commit message	Last commit date
.lake		.lake
RegularLocalRings		RegularLocalRings
EmbDim'.lean		EmbDim'.lean
EmbeddingDimension.lean		EmbeddingDimension.lean
LICENSE		LICENSE
LocalRingDimension.lean		LocalRingDimension.lean
README.md		README.md
RegularLocalRings (old).lean		RegularLocalRings (old).lean
RegularLocalRings.lean		RegularLocalRings.lean
lake-manifest.json		lake-manifest.json
lakefile.lean		lakefile.lean
lean-toolchain		lean-toolchain

Repository files navigation

This is a UW community formalization project centered on formalizing regular local rings.

Goal 1: Prove the undone theorems in EmdDim.lean.

~~Goal 2: Regular local rings are integral domains.~~

Goal 3: Regular local rings are Cohen Macaulay.

Goal 4: 1 dimensional Regular local rings are PIDs.

About

Formalization of regular local rings and regular sequences

0 stars

0 watching

Report repository

Releases

Packages

Contributors

Languages