chore: Deprecated aliases for Rat.cast_natCast, Rat.cast_intCast (#…

…11636) These were moved in #11552.
leanprover-community · Mar 24, 2024 · 0e6c4e2 · 0e6c4e2
1 parent 1f8fea7
commit 0e6c4e2
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/Mathlib/Data/Rat/Cast/Defs.lean b/Mathlib/Data/Rat/Cast/Defs.lean
@@ -48,6 +48,10 @@ theorem cast_natCast (n : ℕ) : ((n : ℚ) : α) = n := by
   rw [← Int.cast_ofNat, cast_intCast, Int.cast_ofNat]
 #align rat.cast_coe_nat Rat.cast_natCast
 
+-- 2024-03-21
+@[deprecated] alias cast_coe_int := cast_intCast
+@[deprecated] alias cast_coe_nat := cast_natCast
+
 -- See note [no_index around OfNat.ofNat]
 @[simp, norm_cast] lemma cast_ofNat (n : ℕ) [n.AtLeastTwo] :
     ((no_index (OfNat.ofNat n : ℚ)) : α) = (OfNat.ofNat n : α) := by