doc(Data/Rat/Cast/Defs): update docs (#17268)

The notation has been moved to `Batteries.Data.Rat`.
leanprover-community · Sep 30, 2024 · eed3300 · eed3300
1 parent 07a4873
commit eed3300
Showing 1 changed file with 0 additions and 4 deletions.
diff --git a/Mathlib/Data/Rat/Cast/Defs.lean b/Mathlib/Data/Rat/Cast/Defs.lean
@@ -19,10 +19,6 @@ import Mathlib.Data.Rat.Lemmas
 We define the canonical injection from ℚ into an arbitrary division ring and prove various
 casting lemmas showing the well-behavedness of this injection.
 
-## Notations
-
-- `/.` is infix notation for `Rat.divInt`.
-
 ## Tags
 
 rat, rationals, field, ℚ, numerator, denominator, num, denom, cast, coercion, casting