Commit 2023-07-14 10:07 8fdefa01

View on Github →

feat: forward-port leanprover-community/mathlib#19105 (#5749) This is Jake Levinson's work. It's a proof that local cohomology agrees for ideals with equal radicals.

Estimated changes

Modified Mathlib/Algebra/Homology/LocalCohomology.lean

deleted theorem Ideal.exists_pow_le_of_le_radical_of_fg

added theorem localCohomology.Ideal.exists_pow_le_of_le_radical_of_fG

added def localCohomology.SelfLERadical.cast

added def localCohomology.SelfLERadical.isoOfSameRadical

added def localCohomology.diagramComp

modified def localCohomology.idealPowersToSelfLERadical

deleted def localCohomology.idealPowersToSelfLERadicalCompInclusion

added def localCohomology.isoOfFinal

added def localCohomology.isoOfSameRadical

added def localCohomology.isoSelfLERadical