Skip to content

feat(RingTheory): Complete intersection local ring is Gorenstein#41103

Open
Thmoas-Guan wants to merge 5178 commits into
leanprover-community:masterfrom
Thmoas-Guan:Complete-Intersection-is-Gorenstein
Open

feat(RingTheory): Complete intersection local ring is Gorenstein#41103
Thmoas-Guan wants to merge 5178 commits into
leanprover-community:masterfrom
Thmoas-Guan:Complete-Intersection-is-Gorenstein

Conversation

@Thmoas-Guan

Copy link
Copy Markdown
Collaborator

In this PR we proved that complete intersection local ring is Gorenstein, together with the full implication chain of local rings.


Open in Gitpod

@github-actions github-actions Bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 12, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports t-ring-theory Ring theory

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant