Skip to content

feat(RingTheory): Gorenstein of exists a vanishing ext#36527

Open
Thmoas-Guan wants to merge 2098 commits intoleanprover-community:masterfrom
Thmoas-Guan:Gorenstein-Local-Ring-of-exists-vanishing-Ext
Open

feat(RingTheory): Gorenstein of exists a vanishing ext#36527
Thmoas-Guan wants to merge 2098 commits intoleanprover-community:masterfrom
Thmoas-Guan:Gorenstein-Local-Ring-of-exists-vanishing-Ext

Conversation

@Thmoas-Guan
Copy link
Copy Markdown
Collaborator

A n-dimensional Noetherian local ring R is Gorenstein if there is an i > n, Ext^i(k, R) = 0.


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 Mar 21, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 2, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

This pull request has conflicts, please merge master and resolve them.

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 merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant