add mul and div to time units

would be cool to add something like this to each of time units

--- a/src/Std/Time/Time/Unit/Millisecond.lean
+++ b/src/Std/Time/Time/Unit/Millisecond.lean
@@ -80,6 +80,34 @@ Creates an `Offset` from an integer.
 def ofInt (data : Int) : Offset :=
   UnitVal.ofInt data

+/--
+Multiplies the `Offset` by an `Int`.
+-/
+@[inline]
+def mulFactor (offset : Offset) (factor : Int) : Offset :=
+  Offset.ofInt (offset.val * factor)
+
+/--
+Divides the `Offset` by an `Int`, using the E-rounding convention (euclidean division).
+-/
+@[inline]
+def edivFactor (offset : Offset) (divisor : Int) : Offset :=
+  Offset.ofInt (offset.val.ediv divisor)
+
+/--
+Divides the `Offset` by an `Int`, using the "T-rounding" (truncation rounding) convention.
+-/
+@[inline]
+def tdivFactor (offset : Offset) (divisor : Int) : Offset :=
+  Offset.ofInt (offset.val.tdiv divisor)
+
+/--
+Divides the `Offset` by an `Int` (default = truncation rounding).
+-/
+@[inline]
+def divFactor (offset : Offset) (divisor : Int) : Offset :=
+  Offset.ofInt (offset.val.tdiv divisor)
+
 end Offset
 namespace Ordinal

N.B. why not just def mul (offset : Offset) (factor : Int) : Offset? bc it would break src/Std/Time/Time/Unit/Basic.lean

Start with src/Std/Time/Time/Unit/Millisecond.lean and inspect src/Std/Time/Time/Unit/Basic.lean to understand how the unit definitions interact. Add the requested multiplication and division operations to each time unit, then verify the standard library still compiles without breaking Basic.lean.