diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean
index c8f27f066..2e6dfe3d8 100644
--- a/library/data/rat/basic.lean
+++ b/library/data/rat/basic.lean
@@ -392,8 +392,10 @@ section
     inv_zero         := inv_zero,
     has_decidable_eq := has_decidable_eq⦄
 
-  migrate from algebra with rat
-    replacing sub → rat.sub
-end
+  definition divide (a b : rat) := algebra.divide a b
+  definition dvd (a b : rat) := algebra.dvd a b
 
+  migrate from algebra with rat
+    replacing sub → rat.sub, divide → divide, dvd → dvd
+end
 end rat
diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean
index 54c717d67..f4399d3df 100644
--- a/library/data/rat/order.lean
+++ b/library/data/rat/order.lean
@@ -222,6 +222,8 @@ section
 
   definition abs (n : rat) : rat := algebra.abs n
   definition sign (n : rat) : rat := algebra.sign n
-  migrate from algebra with rat replacing abs → abs, sign → sign
+
+  migrate from algebra with rat
+  replacing has_le.ge → ge, has_lt.gt → gt, sub → sub, abs → abs, sign → sign, dvd → dvd, divide → divide
 end
 end rat