chore(RingTheory/Ideal/KrullsHeightTheorem): fix capitalization of minimalPrimes (#37463)

Fixed capitalization convention for `minimal_prime` to lower camel case `minimalPrime` according to mathlib naming conventions. There is one changed lemma in `RingTheory/Ideal/KrullsHeightTheorem` and one in `RingTheory/Ideal/MinimalPrime/Localization`.

Author: hommmmm

Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean

@@ -26,7 +26,7 @@ In this file, we prove **Krull's principal ideal theorem** (also known as
   that: In a commutative Noetherian ring `R`, any prime ideal that is minimal over a principal ideal
   has height at most 1.
 
-* `Ideal.height_le_spanRank_toENat_of_mem_minimal_primes` : This theorem is the
+* `Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes` : This theorem is the
   **Krull's height theorem** (also known as **Krullscher Höhensatz**), which states that:
   In a commutative Noetherian ring `R`, any prime ideal that is minimal over an ideal generated by
   `n` elements has height at most `n`.
@@ -36,7 +36,7 @@ In this file, we prove **Krull's principal ideal theorem** (also known as
   a (finitely-generated) ideal is smaller than or equal to the minimum number of generators for
   this ideal.
 
-* `Ideal.height_le_iff_exists_minimal_primes` : In a commutative Noetherian ring `R`, a prime ideal
+* `Ideal.height_le_iff_exists_minimalPrimes` : In a commutative Noetherian ring `R`, a prime ideal
   `p` has height no greater than `n` if and only if it is a minimal ideal over some ideal generated
   by no more than `n` elements.
 -/
@@ -148,7 +148,7 @@ theorem Ideal.mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert {q p : Ide
     rw [height_eq_primeHeight] at h
     have := (primeHeight_strict_mono h_lt).trans_le h
     rw [ENat.lt_one_iff_eq_zero, primeHeight_eq_zero_iff] at this
-    have := minimal_primes_comap_of_surjective hf this
+    have := minimalPrimes_comap_of_surjective hf this
     rwa [comap_map_of_surjective f hf, ← RingHom.ker_eq_comap_bot,
       mk_ker, sup_eq_left.mpr hI'q] at this
   refine height_le_one_of_isPrincipal_of_mem_minimalPrimes ((span {x}).map f) (p.map f) ⟨⟨this,
@@ -167,7 +167,7 @@ open IsLocalRing in
 /-- **Krull's height theorem** (also known as **Krullscher Höhensatz**) :
   In a commutative Noetherian ring `R`, any prime ideal that is minimal over an ideal generated
   by `n` elements has height at most `n`. -/
-nonrec lemma Ideal.height_le_spanRank_toENat_of_mem_minimal_primes
+nonrec lemma Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes
     (I : Ideal R) (p : Ideal R) (hp : p ∈ I.minimalPrimes) :
     p.height ≤ I.spanRank.toENat := by
   classical
@@ -219,11 +219,14 @@ nonrec lemma Ideal.height_le_spanRank_toENat_of_mem_minimal_primes
       refine hspan.trans <| radical_mono ?_
       rw [← Set.union_singleton, span_union]
 
+@[deprecated (since := "2026-04-01")] alias Ideal.height_le_spanRank_toENat_of_mem_minimal_primes :=
+    Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes
+
 lemma Ideal.height_le_card_of_mem_minimalPrimes_span_finset {p : Ideal R} {s : Finset R}
     (hI : p ∈ (Ideal.span s).minimalPrimes) :
     p.height ≤ s.card := by
   trans (Cardinal.toENat (Submodule.spanRank (Ideal.span (s : Set R))))
-  · exact Ideal.height_le_spanRank_toENat_of_mem_minimal_primes _ _ hI
+  · exact Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes _ _ hI
   · simpa using Submodule.spanRank_span_le_card (s : Set R)
 
 lemma Ideal.height_le_card_of_mem_minimalPrimes_span {p : Ideal R} {s : Set R}
@@ -238,7 +241,7 @@ lemma Ideal.height_le_spanRank_toENat (I : Ideal R) (hI : I ≠ ⊤) :
     I.height ≤ I.spanRank.toENat := by
   obtain ⟨J, hJ⟩ := nonempty_minimalPrimes hI
   refine (iInf₂_le J hJ).trans ?_
-  convert (I.height_le_spanRank_toENat_of_mem_minimal_primes J hJ)
+  convert (I.height_le_spanRank_toENat_of_mem_minimalPrimes J hJ)
   exact Eq.symm (@height_eq_primeHeight _ _ J hJ.1.1)
 
 lemma Ideal.height_le_spanFinrank (I : Ideal R) (hI : I ≠ ⊤) :
@@ -291,7 +294,7 @@ lemma Ideal.height_le_iff_exists_minimalPrimes (p : Ideal R) [p.IsPrime]
     norm_cast
   · rintro ⟨I, hp, hI⟩
     exact le_trans
-      (Ideal.height_le_spanRank_toENat_of_mem_minimal_primes I p hp)
+      (Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes I p hp)
       (by simpa using (Cardinal.toENat.monotone' hI))
 
 /-- If `p` is a prime in a Noetherian ring `R`, there exists a `p`-primary ideal `I`
@@ -308,7 +311,7 @@ lemma Ideal.exists_finset_card_eq_height_of_isNoetherianRing (p : Ideal R) [p.Is
   · convert_to p.height ≤ I.spanRank.toENat
     · symm
       simpa [Submodule.fg_iff_spanRank_eq_spanFinrank] using (IsNoetherian.noetherian I)
-    · exact I.height_le_spanRank_toENat_of_mem_minimal_primes _ hI
+    · exact I.height_le_spanRank_toENat_of_mem_minimalPrimes _ hI
 
 /-- If `I ≤ p` and `p` is prime, the height of `p` is bounded by the height of `p ⧸ I R` plus
 the span rank of `I`. -/

Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean

@@ -127,7 +127,7 @@ section
 
 variable {R S : Type*} [CommRing R] [CommRing S] {I J : Ideal R}
 
-theorem Ideal.minimal_primes_comap_of_surjective {f : R →+* S} (hf : Function.Surjective f)
+theorem Ideal.minimalPrimes_comap_of_surjective {f : R →+* S} (hf : Function.Surjective f)
     {I J : Ideal S} (h : J ∈ I.minimalPrimes) : J.comap f ∈ (I.comap f).minimalPrimes := by
   have := h.1.1
   refine ⟨⟨inferInstance, Ideal.comap_mono h.1.2⟩, ?_⟩
@@ -139,6 +139,9 @@ theorem Ideal.minimal_primes_comap_of_surjective {f : R →+* S} (hf : Function.
   · exact ⟨Ideal.map_isPrime_of_surjective hf this, Ideal.le_map_of_comap_le_of_surjective f hf e₁⟩
   · exact Ideal.map_le_of_le_comap e₂
 
+@[deprecated (since := "2026-04-01")] alias Ideal.minimal_primes_comap_of_surjective :=
+    Ideal.minimalPrimes_comap_of_surjective
+
 theorem Ideal.comap_minimalPrimes_eq_of_surjective {f : R →+* S} (hf : Function.Surjective f)
     (I : Ideal S) : (I.comap f).minimalPrimes = Ideal.comap f '' I.minimalPrimes := by
   ext J
@@ -147,7 +150,7 @@ theorem Ideal.comap_minimalPrimes_eq_of_surjective {f : R →+* S} (hf : Functio
     obtain ⟨p, h, rfl⟩ := Ideal.exists_minimalPrimes_comap_eq f J H
     exact ⟨p, h, rfl⟩
   · rintro ⟨J, hJ, rfl⟩
-    exact Ideal.minimal_primes_comap_of_surjective hf hJ
+    exact Ideal.minimalPrimes_comap_of_surjective hf hJ
 
 lemma Ideal.minimalPrimes_map_of_surjective {S : Type*} [CommRing S] {f : R →+* S}
     (hf : Function.Surjective f) (I : Ideal R) :