Commit 2024-03-04 07:58 dad5e8c4

View on Github →

chore: Golf Ideal.radical_pow (#11144) Also make n implicit and replace 0 < n with n ≠ 0

Estimated changes

Modified Mathlib/Algebra/Homology/LocalCohomology.lean

Modified Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

modified theorem PrimeSpectrum.zeroLocus_pow

Modified Mathlib/RingTheory/Ideal/Operations.lean

modified theorem Ideal.radical_pow