Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-06-06 19:24
22a865fa
View on Github →
feat: port Algebra.Homology.LocalCohomology (
#4749
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Algebra/Homology/LocalCohomology.lean
added
theorem
Ideal.exists_pow_le_of_le_radical_of_fG
added
def
localCohomology.SelfLeRadical
added
def
localCohomology.diagram
added
def
localCohomology.idealPowersDiagram
added
def
localCohomology.idealPowersToSelfLeRadical
added
def
localCohomology.idealPowersToSelfLeRadicalCompInclusion
added
def
localCohomology.ofDiagram
added
def
localCohomology.ofSelfLeRadical
added
def
localCohomology.ringModIdeals
added
def
localCohomology.selfLeRadicalDiagram
added
def
localCohomology