chore(CyclotomicField): add missing deprecated aliases for leanprover-community#30010 (leanprover-community#32149)

These results were removed since they were not needed anymore but I forgot to add the deprecated aliases.

Author: xroblot

Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean

@@ -835,6 +835,9 @@ instance _root_.IsCyclotomicExtension.ringOfIntegers [IsCyclotomicExtension {n}
   let _ := (zeta_spec (n) ℚ K).adjoin_isCyclotomicExtension ℤ
   IsCyclotomicExtension.equiv _ ℤ _ (zeta_spec n ℚ K).adjoinEquivRingOfIntegers
 
+@[deprecated (since := "2025-11-26")] alias _root_.IsCyclotomicExtension.ring_of_integers' :=
+  _root_.IsCyclotomicExtension.ringOfIntegers
+
 /-- The integral `PowerBasis` of `𝓞 K` given by a primitive root of unity, where `K` is a `n`-th
 cyclotomic extension of `ℚ`. -/
 noncomputable def integralPowerBasis [IsCyclotomicExtension {n} ℚ K]
@@ -871,6 +874,17 @@ theorem subOneIntegralPowerBasis_gen [IsCyclotomicExtension {n} ℚ K]
       ⟨ζ - 1, Subalgebra.sub_mem _ (hζ.isIntegral (NeZero.pos _)) (Subalgebra.one_mem _)⟩ := by
   simp [subOneIntegralPowerBasis]
 
+@[deprecated (since := "2025-11-26")] alias integralPowerBasis' := integralPowerBasis
+@[deprecated (since := "2025-11-26")] alias integralPowerBasis'_gen := integralPowerBasis_gen
+@[deprecated (since := "2025-11-26")] alias power_basis_int'_dim := integralPowerBasis_dim
+@[deprecated (since := "2025-11-26")] alias subOneIntegralPowerBasis' := subOneIntegralPowerBasis
+@[deprecated (since := "2025-11-26")] alias subOneIntegralPowerBasis'_gen :=
+  subOneIntegralPowerBasis_gen
+@[deprecated (since := "2025-11-26")] alias subOneIntegralPowerBasis'_gen_prime :=
+  subOneIntegralPowerBasis_gen
+@[deprecated (since := "2025-11-26")] alias subOneIntegralPowerBasis_gen_prime :=
+  subOneIntegralPowerBasis_gen
+
 end IsPrimitiveRoot
 
 end discr