Commit 2024-10-26 13:22 b76f29f5

View on Github →

chore(RingTheory): move Ideal.exists_pow_le_of_le_radical_of_fG (#18189) renamed to Ideal.exists_pow_le_of_le_radical_of_fg_radical, and added Ideal.exists_pow_le_of_le_radical_of_fg

Estimated changes

Modified Mathlib/Algebra/Homology/LocalCohomology.lean

deleted theorem localCohomology.Ideal.exists_pow_le_of_le_radical_of_fG

Modified Mathlib/RingTheory/Finiteness.lean

added theorem Ideal.exists_pow_le_of_le_radical_of_fg

added theorem Ideal.exists_pow_le_of_le_radical_of_fg_radical

Modified Mathlib/RingTheory/Ideal/Operations.lean

added theorem Ideal.sup_pow_add_le_pow_sup_pow