refactor(RingTheory/RamificationInertia/Inertia): swap inertiaDeg and inertiaDeg' (#41325)

This PR swaps `inertiaDeg` and `inertiaDeg'`.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/NumberTheory/NumberField/ClassNumber.lean

@@ -143,7 +143,7 @@ The way this theorem should be used is to first compute `⌊(M K)⌋₊` and the
 to deal with the finite number of primes `p` in the interval. -/
 theorem isPrincipalIdealRing_of_isPrincipal_of_pow_le_of_mem_primesOver_of_mem_Icc
     (h : ∀ p ∈ Finset.Icc 1 ⌊(M K)⌋₊, p.Prime → ∀ (P : Ideal (𝓞 K)),
-      P ∈ primesOver (span {(p : ℤ)}) (𝓞 K) → p ^ P.inertiaDeg' ℤ ≤ ⌊(M K)⌋₊ →
+      P ∈ primesOver (span {(p : ℤ)}) (𝓞 K) → p ^ P.inertiaDeg ℤ ≤ ⌊(M K)⌋₊ →
       Submodule.IsPrincipal P) : IsPrincipalIdealRing (𝓞 K) := by
   refine isPrincipalIdealRing_of_isPrincipal_of_norm_le_of_isPrime <|
     fun ⟨P, HP⟩ hP hPN ↦ ?_
@@ -157,18 +157,18 @@ theorem isPrincipalIdealRing_of_isPrincipal_of_pow_le_of_mem_primesOver_of_mem_I
     simpa [h, span_singleton_neg p, ← submodule_span_eq, ← hp] using over_under P
   have hspan : span {↑p.natAbs} = span {p} := by
     rcases abs_choice p with h | h <;> simp [h]
-  have hple : p.natAbs ^ P.inertiaDeg' ℤ ≤ ⌊(M K)⌋₊ := by
+  have hple : p.natAbs ^ P.inertiaDeg ℤ ≤ ⌊(M K)⌋₊ := by
     refine le_floor ?_
     have : P.IsMaximal := hP.isMaximal (by simpa using HP.2)
     have : (span {p}).IsMaximal := (hpprime (.under ℤ P)).isMaximal_span_singleton
-    simpa only [hspan, ← cast_pow, ← natAbs_pow_inertiaDeg' p P] using hPN
+    simpa only [hspan, ← cast_pow, ← natAbs_pow_inertiaDeg p P] using hPN
   have hpabsprime := Int.prime_iff_natAbs_prime.mp (hpprime (hP.under _))
   refine h _ ?_ hpabsprime _ ⟨hP, ?_⟩ hple
-  · suffices 0 < P.inertiaDeg' ℤ by
+  · suffices 0 < P.inertiaDeg ℤ by
       exact Finset.mem_Icc.mpr ⟨hpabsprime.one_le, le_trans (le_pow this) hple⟩
     have := (isPrime_of_prime (prime_span_singleton_iff.mpr <|
       hpprime (hP.under _))).isMaximal <| by simp [((hpprime (hP.under _))).ne_zero]
-    exact inertiaDeg'_pos ..
+    exact inertiaDeg_pos ..
   · exact hspan ▸ hlies
 
 /-- Let `K` be a number field such that `K/ℚ` is Galois and let `M K` be the Minkowski bound of `K`.
@@ -183,15 +183,15 @@ to deal with the finite number of primes `p` in the interval. -/
 theorem isPrincipalIdealRing_of_isPrincipal_of_lt_or_isPrincipal_of_mem_primesOver_of_mem_Icc
     [IsGalois ℚ K] (h : ∀ p ∈ Finset.Icc 1 ⌊(M K)⌋₊, p.Prime →
       ∃ P ∈ primesOver (span {(p : ℤ)}) (𝓞 K),
-        ⌊(M K)⌋₊ < p ^ P.inertiaDeg' ℤ ∨
+        ⌊(M K)⌋₊ < p ^ P.inertiaDeg ℤ ∨
           Submodule.IsPrincipal P) :
       IsPrincipalIdealRing (𝓞 K) := by
   refine isPrincipalIdealRing_of_isPrincipal_of_pow_le_of_mem_primesOver_of_mem_Icc
     (fun p hpmem hp P ⟨hP1, hP2⟩ hple ↦ ?_)
   obtain ⟨Q, ⟨hQ1, hQ2⟩, H⟩ := h p hpmem hp
   have := (isPrime_of_prime (prime_span_singleton_iff.mpr (prime_iff_prime_int.mp hp))).isMaximal
     (by simp [hp.ne_zero])
-  by_cases h : ⌊(M K)⌋₊ < p ^ P.inertiaDeg' ℤ
+  by_cases h : ⌊(M K)⌋₊ < p ^ P.inertiaDeg ℤ
   · linarith
   rw [inertiaDeg_eq_of_isGaloisGroup (span {↑p}) Q P (K ≃ₐ[ℚ] K)] at H
   obtain ⟨σ, rfl⟩ := exists_smul_eq_of_isGaloisGroup (span ({↑p} : Set ℤ)) Q P (K ≃ₐ[ℚ] K)

Mathlib/NumberTheory/NumberField/Completion/Ramification.lean

@@ -86,15 +86,15 @@ variable (w)
 open scoped Classical in
 /-- The inertia degree of `w` over `v`. -/
 protected noncomputable def inertiaDeg : ℕ :=
-  if _ : w.1.LiesOver v.1 then (⊥ : Ideal w.Completion).inertiaDeg' v.Completion else 0
+  if _ : w.1.LiesOver v.1 then (⊥ : Ideal w.Completion).inertiaDeg v.Completion else 0
 
 theorem inertiaDeg_of_liesOver [w.1.LiesOver v.1] :
-    v.inertiaDeg w = (⊥ : Ideal w.Completion).inertiaDeg' v.Completion := by
+    v.inertiaDeg w = (⊥ : Ideal w.Completion).inertiaDeg v.Completion := by
   simp only [InfinitePlace.inertiaDeg, dif_pos]
 
 theorem inertiaDeg_eq_finrank [w.1.LiesOver v.1] :
     v.inertiaDeg w = Module.finrank v.Completion w.Completion := by
-  rw [inertiaDeg_of_liesOver, Ideal.inertiaDeg'_eq_of_isMaximal ⊥]
+  rw [inertiaDeg_of_liesOver, Ideal.inertiaDeg_eq_of_isMaximal ⊥]
   exact Algebra.finrank_eq_of_equiv_equiv (RingEquiv.quotientBot v.Completion)
     (RingEquiv.quotientBot w.Completion) (by ext; simp [RingHom.algebraMap_toAlgebra])
 

Mathlib/NumberTheory/NumberField/Cyclotomic/Galois.lean

@@ -122,7 +122,7 @@ theorem mem_zpowers_galEquivZMod_of_mem_stabilizer {σ : Gal(K/ℚ)} (hσ : σ 
   have h₀ : IsPrimitiveRoot (Ideal.Quotient.mk P hζ.toInteger) n := by
     refine hζ.toInteger_isPrimitiveRoot.idealQuotient_mk
       (by simpa using IsMaximal.ne_top inferInstance) ?_
-    rw [← pow_inertiaDeg' p]
+    rw [← pow_inertiaDeg p]
     exact Nat.Coprime.pow_left _ hn
   have h₁ := IsFractionRing.stabilizerHom_apply_apply_mk Gal(K/ℚ) (Ideal.span {(p : ℤ)}) P
       (ℤ ⧸ span {(p : ℤ)}) (𝓞 K ⧸ P) ⟨σ, hσ⟩ hζ.toInteger

Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean

@@ -97,9 +97,9 @@ instance liesOver_span_zeta_sub_one : (span {hζ.toInteger - 1}).LiesOver 𝒑 :
   rw [span_singleton_le_iff_mem, mem_comap, algebraMap_int_eq, map_natCast]
   exact p_mem_span_zeta_sub_one p k hζ
 
-theorem inertiaDeg_span_zeta_sub_one : inertiaDeg' (span {hζ.toInteger - 1}) ℤ = 1 := by
+theorem inertiaDeg_span_zeta_sub_one : inertiaDeg (span {hζ.toInteger - 1}) ℤ = 1 := by
   have : IsMaximal (span {hζ.toInteger - 1}) := .of_liesOver_isMaximal _ 𝒑
-  rw [← Nat.pow_right_inj hp.out.one_lt, pow_one, pow_inertiaDeg',
+  rw [← Nat.pow_right_inj hp.out.one_lt, pow_one, pow_inertiaDeg,
     absNorm_span_zeta_sub_one]
 
 attribute [local instance] FractionRing.liftAlgebra in
@@ -156,7 +156,7 @@ theorem eq_span_zeta_sub_one_of_liesOver (P : Ideal (𝓞 K)) [hP₁ : P.IsPrime
 
 include hK in
 theorem inertiaDeg_eq_of_prime_pow (P : Ideal (𝓞 K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver 𝒑] :
-    inertiaDeg' P ℤ = 1 := by
+    inertiaDeg P ℤ = 1 := by
   rw [eq_span_zeta_sub_one_of_liesOver p k K hK.zeta_spec P, inertiaDeg_span_zeta_sub_one]
 
 include hK in
@@ -228,7 +228,7 @@ theorem isCoprime_of_not_zeta_sub_one_dvd {x : 𝓞 K} (hx : ¬ hζ.toInteger -
     (prime_span_singleton_iff.mpr
     hζ.zeta_sub_one_prime').irreducible.gcd_eq_one_iff, dvd_span_singleton, mem_span_singleton]
 
-theorem inertiaDeg_span_zeta_sub_one' : inertiaDeg' (span {hζ.toInteger - 1}) ℤ = 1 := by
+theorem inertiaDeg_span_zeta_sub_one' : inertiaDeg (span {hζ.toInteger - 1}) ℤ = 1 := by
   rw [← pow_one p] at hK hζ
   exact inertiaDeg_span_zeta_sub_one p 0 hζ
 
@@ -259,7 +259,7 @@ theorem eq_span_zeta_sub_one_of_liesOver' (P : Ideal (𝓞 K)) [hP₁ : P.IsPrim
 
 include hK in
 theorem inertiaDeg_eq_of_prime (P : Ideal (𝓞 K)) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver 𝒑] :
-    inertiaDeg' P ℤ = 1 := by
+    inertiaDeg P ℤ = 1 := by
   rw [eq_span_zeta_sub_one_of_liesOver' p K hK.zeta_spec P, inertiaDeg_span_zeta_sub_one']
 
 include hK in
@@ -291,7 +291,7 @@ open NumberField.Ideal Polynomial
 variable {m} [NeZero m] [hK : IsCyclotomicExtension {m} ℚ K]
 
 theorem inertiaDeg_eq_of_not_dvd (hm : ¬ p ∣ m) :
-    inertiaDeg' P ℤ = orderOf (p : ZMod m) := by
+    inertiaDeg P ℤ = orderOf (p : ZMod m) := by
   replace hm : p.Coprime m := hp.out.coprime_iff_not_dvd.mpr hm
   let ζ := (zeta_spec m ℚ K).toInteger
   have h₁ : ¬ p ∣ exponent ζ := by
@@ -427,7 +427,7 @@ theorem ramificationIdxIn_eq (hn : n = p ^ (k + 1) * m) (hm : ¬ p ∣ m) :
   (inertiaDegIn_ramificationIdxIn_aux n K hn hm).2
 
 theorem inertiaDeg_eq (hn : n = p ^ (k + 1) * m) (hm : ¬ p ∣ m) :
-    inertiaDeg' P ℤ = orderOf (p : ZMod m) := by
+    inertiaDeg P ℤ = orderOf (p : ZMod m) := by
   have : IsGalois ℚ K := isGalois {n} ℚ K
   rw [← inertiaDegIn_eq_inertiaDeg 𝒑 P Gal(K/ℚ), inertiaDegIn_eq n K hn hm]
 

Mathlib/NumberTheory/NumberField/Discriminant/Different.lean

@@ -189,9 +189,9 @@ lemma not_dvd_discr_iff_forall_liesOver [IsIntegralClosure 𝒪 ℤ K] {p : ℤ}
     exact ⟨P, hP, ⟨h₁.symm⟩, h₂⟩
   · rintro ⟨P, hP, hP', hP''⟩
     have := Ideal.absNorm_dvd_absNorm_of_le (Ideal.dvd_iff_le.mp hP'')
-    rw [absNorm_differentIdeal K, ← Ideal.natAbs_pow_inertiaDeg' p,
+    rw [absNorm_differentIdeal K, ← Ideal.natAbs_pow_inertiaDeg p,
       ← Int.natAbs_pow, Int.natAbs_dvd_natAbs] at this
-    exact (dvd_pow_self _ (Ideal.inertiaDeg'_pos ..).ne').trans this
+    exact (dvd_pow_self _ (Ideal.inertiaDeg_pos ..).ne').trans this
 
 /-- A prime `p` does not divide `discr K` if and only if `p` (as the ideal `span {p}`) is
 unramified in the ring of integers `𝒪`.

Mathlib/NumberTheory/NumberField/Ideal/KummerDedekind.lean

@@ -209,7 +209,7 @@ The residual degree of the ideal corresponding to the class of `Q ∈ ℤ[X]` mo
 -/
 theorem inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply (hp : ¬ p ∣ exponent θ)
     {Q : ℤ[X]} (hQ : Q.map (Int.castRingHom (ZMod p)) ∈ monicFactorsMod θ p) :
-    inertiaDeg' ((primesOverSpanEquivMonicFactorsMod hp).symm
+    inertiaDeg ((primesOverSpanEquivMonicFactorsMod hp).symm
       ⟨Q.map (Int.castRingHom (ZMod p)), hQ⟩ : Ideal (𝓞 K)) ℤ =
         natDegree (Q.map (Int.castRingHom (ZMod p))) := by
   -- This is needed for `inertiaDeg_algebraMap` below to work
@@ -218,14 +218,14 @@ theorem inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply (hp : ¬ p ∣
     apply Ideal.primesOver.isMaximal
   have := liesOver_primesOverSpanEquivMonicFactorsMod_symm hp hQ
   rw [primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span,
-    inertiaDeg'_eq_of_isMaximal (span {(p : ℤ)}),
+    inertiaDeg_eq_of_isMaximal (span {(p : ℤ)}),
     ← finrank_quotient_span_eq_natDegree]
   refine Algebra.finrank_eq_of_equiv_equiv (Int.quotientSpanNatEquivZMod p) ?_ (by ext; simp)
   exact (ZModXQuotSpanEquivQuotSpanPair hp hQ).symm
 
 theorem inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply' (hp : ¬ p ∣ exponent θ)
     {Q : (ZMod p)[X]} (hQ : Q ∈ monicFactorsMod θ p) :
-    inertiaDeg'
+    inertiaDeg
       ((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Q, hQ⟩ : Ideal (𝓞 K)) ℤ = natDegree Q := by
   obtain ⟨S, rfl⟩ := (map_surjective _ (ZMod.ringHom_surjective (Int.castRingHom (ZMod p)))) Q
   rw [inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply]

Mathlib/NumberTheory/RamificationInertia/Basic.lean

@@ -527,8 +527,8 @@ open scoped Classical in
 theorem Factors.finrank_pow_ramificationIdx [p.IsMaximal]
     (P : (factors (map (algebraMap R S) p)).toFinset) :
     finrank (R ⧸ p) (S ⧸ (P : Ideal S) ^ ramificationIdx' p P.1) =
-      ramificationIdx' p P.1 * inertiaDeg p (P : Ideal S) := by
-  rw [finrank_prime_pow_ramificationIdx, inertiaDeg_algebraMap]
+      ramificationIdx' p P.1 * inertiaDeg' p (P : Ideal S) := by
+  rw [finrank_prime_pow_ramificationIdx, inertiaDeg'_algebraMap]
   exacts [Factors.ne_bot p P, NeZero.ne _]
 
 open scoped Classical in
@@ -537,7 +537,7 @@ instance Factors.finiteDimensional_quotient_pow [Module.Finite R S] [p.IsMaximal
     FiniteDimensional (R ⧸ p) (S ⧸ (P : Ideal S) ^ ramificationIdx' p P.1) := by
   refine .of_finrank_pos ?_
   rw [pos_iff_ne_zero, Factors.finrank_pow_ramificationIdx]
-  exact mul_ne_zero (Factors.ramificationIdx_ne_zero p P) (inertiaDeg_pos p P.1).ne'
+  exact mul_ne_zero (Factors.ramificationIdx_ne_zero p P) (inertiaDeg'_pos p P.1).ne'
 
 universe w
 
@@ -595,10 +595,10 @@ here `S` is a finite `R`-module (and thus `Frac(S) : Frac(R)` is a finite extens
 is maximal. -/
 theorem sum_ramification_inertia {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) :
     ∑ P ∈ IsDedekindDomain.primesOverFinset p S,
-        ramificationIdx' p P * inertiaDeg p P = finrank K L := by
+        ramificationIdx' p P * inertiaDeg' p P = finrank K L := by
   set e := ramificationIdx' p (S := S)
   calc
-    ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset, e P * inertiaDeg p P =
+    ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset, e P * inertiaDeg' p P =
         ∑ P ∈ (factors (map (algebraMap R S) p)).toFinset.attach,
           finrank (R ⧸ p) (S ⧸ (P : Ideal S) ^ e P) := ?_
     _ = finrank (R ⧸ p)
@@ -616,7 +616,7 @@ theorem sum_ramification_inertia {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) :
 
 theorem inertiaDeg_le_finrank [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal]
     (P : Ideal S) [hP₁ : P.IsPrime] [hP₂ : P.LiesOver p] (hp0 : p ≠ ⊥) :
-    p.inertiaDeg P ≤ Module.finrank K L := by
+    p.inertiaDeg' P ≤ Module.finrank K L := by
   classical
   have hP : P ∈ IsDedekindDomain.primesOverFinset p S :=
     (IsDedekindDomain.mem_primesOverFinset_iff hp0 _).mpr ⟨hP₁, hP₂⟩
@@ -634,7 +634,7 @@ theorem ramificationIdx_le_finrank [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsM
     (IsDedekindDomain.mem_primesOverFinset_iff hp0 _).mpr ⟨hP₁, hP₂⟩
   rw [← sum_ramification_inertia S K L hp0, ← Finset.add_sum_erase _ _ hP]
   refine le_trans (Nat.le_mul_of_pos_right _ ?_) (Nat.le_add_right _ _)
-  exact Nat.pos_iff_ne_zero.mpr <| inertiaDeg_ne_zero p P
+  exact Nat.pos_iff_ne_zero.mpr <| inertiaDeg'_ne_zero p P
 
 theorem card_primesOverFinset_le_finrank [NoZeroSMulDivisors R S] {p : Ideal R} [p.IsMaximal]
     (hp0 : p ≠ ⊥) : Finset.card (IsDedekindDomain.primesOverFinset p S) ≤ Module.finrank K L := by
@@ -644,13 +644,13 @@ theorem card_primesOverFinset_le_finrank [NoZeroSMulDivisors R S] {p : Ideal R}
   have : P.LiesOver p := ((IsDedekindDomain.mem_primesOverFinset_iff hp0 _).mp hP).2
   refine Right.one_le_mul ?_ ?_
   · exact Nat.pos_iff_ne_zero.mpr <| IsDedekindDomain.ramificationIdx'_ne_zero_of_liesOver _ hp0
-  · exact Nat.pos_iff_ne_zero.mpr <| inertiaDeg_ne_zero p P
+  · exact Nat.pos_iff_ne_zero.mpr <| inertiaDeg'_ne_zero p P
 
 /-- `Ideal.sum_ramification_inertia`, in the local (DVR) case. -/
 lemma ramificationIdx_mul_inertiaDeg_of_isLocalRing [IsLocalRing S] {p : Ideal R} [p.IsMaximal]
     (hp0 : p ≠ ⊥) :
     ramificationIdx' p (IsLocalRing.maximalIdeal S) *
-      p.inertiaDeg (IsLocalRing.maximalIdeal S) = Module.finrank K L := by
+      p.inertiaDeg' (IsLocalRing.maximalIdeal S) = Module.finrank K L := by
   have := FaithfulSMul.of_field_isFractionRing R S K L
   simp_rw [← sum_ramification_inertia S K L hp0, IsLocalRing.primesOverFinset_eq S hp0,
     Finset.sum_singleton]

Mathlib/NumberTheory/RamificationInertia/Galois.lean

@@ -67,7 +67,7 @@ open scoped Classical in
   maximal ideal `p` of `A` are the same, which we define as `Ideal.inertiaDegIn`. -/
 noncomputable def inertiaDegIn {A : Type*} [CommRing A] (p : Ideal A)
     (B : Type*) [CommRing B] [Algebra A B] : ℕ :=
-  if h : ∃ P : Ideal B, P.IsPrime ∧ P.LiesOver p then h.choose.inertiaDeg' A else 0
+  if h : ∃ P : Ideal B, P.IsPrime ∧ P.LiesOver p then h.choose.inertiaDeg A else 0
 
 section MulAction
 
@@ -145,9 +145,9 @@ theorem ramificationIdx_eq_of_isGaloisGroup :
 include p G in
 /-- All the `Ideal.inertiaDeg` over a fixed maximal ideal are the same. -/
 theorem inertiaDeg_eq_of_isGaloisGroup :
-    P.inertiaDeg' A = Q.inertiaDeg' A := by
+    P.inertiaDeg A = Q.inertiaDeg A := by
   rcases exists_smul_eq_of_isGaloisGroup p P Q G with ⟨σ, rfl⟩
-  rw [inertiaDeg'_smul]
+  rw [inertiaDeg_smul]
 
 include p G in
 /-- The `ramificationIdxIn` is equal to any ramification index over the same ideal. -/
@@ -168,7 +168,7 @@ theorem ramificationIdxIn_ne_zero [Module.Finite A B] [FaithfulSMul A B] {p : Id
 include G in
 /-- The `inertiaDegIn` is equal to any ramification index over the same ideal. -/
 theorem inertiaDegIn_eq_inertiaDeg :
-    inertiaDegIn p B = P.inertiaDeg' A := by
+    inertiaDegIn p B = P.inertiaDeg A := by
   have h : ∃ P : Ideal B, P.IsPrime ∧ P.LiesOver p := ⟨P, hPp, hp⟩
   obtain ⟨_, _⟩ := h.choose_spec
   rw [inertiaDegIn, dif_pos h]
@@ -179,7 +179,7 @@ theorem inertiaDegIn_ne_zero [Module.Finite A B] [FaithfulSMul A B] {p : Ideal A
     inertiaDegIn p B ≠ 0 := by
   obtain ⟨P⟩ := (inferInstance : Nonempty (primesOver p B))
   rw [inertiaDegIn_eq_inertiaDeg p P G]
-  exact (P.1.inertiaDeg'_pos A).ne'
+  exact (P.1.inertiaDeg_pos A).ne'
 
 section tower
 
@@ -194,7 +194,7 @@ theorem inertiaDegIn_mul_inertiaDegIn :
   obtain ⟨⟨Q, _, _⟩⟩ := (inferInstance : Nonempty (primesOver P C))
   have : Q.LiesOver p := LiesOver.trans Q P p
   rw [inertiaDegIn_eq_inertiaDeg p P G, inertiaDegIn_eq_inertiaDeg p Q GAC,
-    inertiaDegIn_eq_inertiaDeg P Q GBC, ← inertiaDeg'_tower P Q]
+    inertiaDegIn_eq_inertiaDeg P Q GBC, ← inertiaDeg_tower P Q]
 
 variable {p} in
 include G GAC GBC in
@@ -286,7 +286,7 @@ open Algebra
 attribute [local instance] Ideal.Quotient.field in
 theorem card_stabilizer_eq_card_inertia_mul_finrank (p : Ideal R) [p.IsPrime]
     (P : Ideal S) [P.LiesOver p] [P.IsPrime] [PerfectField p.ResidueField] :
-    Nat.card (MulAction.stabilizer G P) = Nat.card (inertia G P) * P.inertiaDeg' R := by
+    Nat.card (MulAction.stabilizer G P) = Nat.card (inertia G P) * P.inertiaDeg R := by
   let := Localization.AtPrime.algebraOfLiesOver p P
   have heq : (algebraMap (S ⧸ P) P.ResidueField).comp (algebraMap (R ⧸ p) (S ⧸ P)) =
       (algebraMap p.ResidueField P.ResidueField).comp (algebraMap (R ⧸ p) p.ResidueField) := by
@@ -301,14 +301,14 @@ theorem card_stabilizer_eq_card_inertia_mul_finrank (p : Ideal R) [p.IsPrime]
     Ideal.IsFractionRing.finite_of_isInvariant G p P p.ResidueField P.ResidueField
   have : Subgroup.index _ = _ := Nat.card_congr
     (IsFractionRing.stabilizerQuotientInertiaEquiv G p P p.ResidueField P.ResidueField).toEquiv
-  rw [inertiaDeg'_eq p P, ← IsGalois.card_aut_eq_finrank p.ResidueField P.ResidueField, ← this,
+  rw [inertiaDeg_eq p P, ← IsGalois.card_aut_eq_finrank p.ResidueField P.ResidueField, ← this,
     ← ((inertia G P).subgroupOf (MulAction.stabilizer G P)).card_mul_index,
     Nat.card_congr (Subgroup.subgroupOfEquivOfLe (inertia_le_stabilizer (M := G) P)).toEquiv,
     AddSubgroup.subgroupOf_inertia]
 
 lemma ncard_primesOver_mul_card_inertia_mul_finrank (p : Ideal R) [p.IsPrime]
     (P : Ideal S) [P.LiesOver p] [P.IsPrime] [PerfectField p.ResidueField] :
-    (p.primesOver S).ncard * Nat.card (P.inertia G) * P.inertiaDeg' R = Nat.card G := by
+    (p.primesOver S).ncard * Nat.card (P.inertia G) * P.inertiaDeg R = Nat.card G := by
   rw [mul_assoc, ← card_stabilizer_eq_card_inertia_mul_finrank p P,
     ← IsInvariant.orbit_eq_primesOver R S G p P]
   simpa using Nat.card_congr (MulAction.orbitProdStabilizerEquivGroup G P)

Mathlib/NumberTheory/RamificationInertia/HilbertTheory.lean

@@ -296,7 +296,7 @@ private lemma ramificationIdxIn_eq_and_inertiaDegIn_eq (hp : p ≠ ⊥) :
     exact 𝓟D.ramificationIdx_above_le P
   · rw [inertiaDegIn_eq_inertiaDeg p P Gal(L/K),
       inertiaDegIn_eq_inertiaDeg _ P (stabilizer Gal(L/K) P)]
-    exact inertiaDeg'_above_le 𝓟D P
+    exact inertiaDeg_above_le 𝓟D P
   · have := ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn 𝓟D B (stabilizer Gal(L/K) P)
     rw [primesOver_eq_singleton K L P D 𝓞D, Set.ncard_singleton, one_mul] at this
     rw [this, IsGaloisGroup.card_eq_finrank (stabilizer Gal(L/K) P) D L,
@@ -339,9 +339,9 @@ Let `D` be the decomposition field of `P` in `L/K`. Let `𝓟D` be a prime ideal
 then the inertia degree of `𝓟D` over `K` is equal to `1`.
 -/
 theorem inertiaDeg_eq (hp : p ≠ ⊥) :
-    𝓟D.inertiaDeg' A = 1 := by
+    𝓟D.inertiaDeg A = 1 := by
   obtain ⟨_, _, _, _, _, _⟩ := instances A K L P D 𝓞D 𝓟D hp
-  have := inertiaDeg'_tower (R := A) 𝓟D P
+  have := inertiaDeg_tower (R := A) 𝓟D P
   rwa [← inertiaDegIn_eq_inertiaDeg p P Gal(L/K), ← inertiaDegIn_eq A K L P D 𝓞D 𝓟D hp,
     ← inertiaDegIn_eq_inertiaDeg 𝓟D P (stabilizer Gal(L/K) P),
     right_eq_mul₀ <| inertiaDegIn_ne_zero (stabilizer Gal(L/K) P)] at this