chore: Golf Ideal.radical_pow (#11144)

Also make `n` implicit and replace `0 < n` with `n ≠ 0`
leanprover-community · Apr 15, 2024 · e991859 · e991859
1 parent fbb4f8f
commit e991859
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 17 deletions.
diff --git a/Mathlib/Algebra/Homology/LocalCohomology.lean b/Mathlib/Algebra/Homology/LocalCohomology.lean
@@ -219,7 +219,7 @@ def idealPowersToSelfLERadical (J : Ideal R) : ℕᵒᵖ ⥤ SelfLERadical J :=
     change _ ≤ (J ^ unop k).radical
     cases' unop k with n
     · simp [Ideal.radical_top, pow_zero, Ideal.one_eq_top, le_top, Nat.zero_eq]
-    · simp only [J.radical_pow _ n.succ_pos, Ideal.le_radical]
+    · simp only [J.radical_pow n.succ_ne_zero, Ideal.le_radical]
 #align local_cohomology.ideal_powers_to_self_le_radical localCohomology.idealPowersToSelfLERadical
 
 variable {I J K : Ideal R}

diff --git a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean
@@ -374,9 +374,9 @@ theorem zeroLocus_singleton_mul (f g : R) :
 #align prime_spectrum.zero_locus_singleton_mul PrimeSpectrum.zeroLocus_singleton_mul
 
 @[simp]
-theorem zeroLocus_pow (I : Ideal R) {n : ℕ} (hn : 0 < n) :
+theorem zeroLocus_pow (I : Ideal R) {n : ℕ} (hn : n ≠ 0) :
     zeroLocus ((I ^ n : Ideal R) : Set R) = zeroLocus I :=
-  zeroLocus_radical (I ^ n) ▸ (I.radical_pow n hn).symm ▸ zeroLocus_radical I
+  zeroLocus_radical (I ^ n) ▸ (I.radical_pow hn).symm ▸ zeroLocus_radical I
 #align prime_spectrum.zero_locus_pow PrimeSpectrum.zeroLocus_pow
 
 @[simp]

diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean
@@ -1092,20 +1092,9 @@ variable {R}
 
 variable (I)
 
-theorem radical_pow (n : ℕ) (H : n > 0) : radical (I ^ n) = radical I :=
-  Nat.recOn n (Not.elim (by decide))
-    (fun n ih H =>
-      Or.casesOn (lt_or_eq_of_le <| Nat.le_of_lt_succ H)
-        (fun H =>
-          calc
-            radical (I ^ (n + 1)) = radical I ⊓ radical (I ^ n) := by
-              rw [pow_succ]
-              exact radical_mul _ _
-            _ = radical I ⊓ radical I := by rw [ih H]
-            _ = radical I := inf_idem
-            )
-        fun H => H ▸ (pow_one I).symm ▸ rfl)
-    H
+lemma radical_pow : ∀ {n}, n ≠ 0 → radical (I ^ n) = radical I
+  | 1, _ => by simp
+  | n + 2, _ => by rw [pow_succ, radical_mul, radical_pow n.succ_ne_zero, inf_idem]
 #align ideal.radical_pow Ideal.radical_pow
 
 theorem IsPrime.mul_le {I J P : Ideal R} (hp : IsPrime P) : I * J ≤ P ↔ I ≤ P ∨ J ≤ P := by