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