diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean
index eabaf743ea..b932785795 100644
--- a/src/Init/Data/Int/Basic.lean
+++ b/src/Init/Data/Int/Basic.lean
@@ -9,12 +9,39 @@ prelude
 import Init.Coe
 import Init.Data.Nat.Div
 import Init.Data.List.Basic
+set_option linter.missingDocs true -- keep it documented
 open Nat
 
-/-! # the Type, coercions, and notation -/
+/-! # Integer Type, Coercions, and Notation
 
+This file defines the `Int` type as well as
+
+* coercions, conversions, and compatibility with numeric literals,
+* basic arithmetic operations add/sub/mul/div/mod/pow,
+* a few `Nat`-related operations such as `negOfNat` and `subNatNat`,
+* relations `<`/`≤`/`≥`/`>`, the `NonNeg` property and `min`/`max`,
+* decidability of equality, relations and `NonNeg`.
+-/
+
+/--
+The type of integers. It is defined as an inductive type based on the
+natural number type `Nat` featuring two constructors: "a natural
+number is an integer", and "the negation of a successor of a natural
+number is an integer". The former represents integers between `0`
+(inclusive) and `∞`, and the latter integers between `-∞` and `-1`
+(inclusive).
+
+This type is special-cased by the compiler. The runtime has a special
+representation for `Int` which stores "small" signed numbers directly,
+and larger numbers use an arbitrary precision "bignum" library
+(usually [GMP](https://gmplib.org/)). A "small number" is an integer
+that can be encoded with 63 bits (31 bits on 32-bits architectures).
+-/
 inductive Int : Type where
+  /-- A natural number is an integer (`0` to `∞`). -/
   | ofNat   : Nat → Int
+  /-- The negation of the successor of a natural number is an integer
+    (`-1` to `-∞`). -/
   | negSucc : Nat → Int
 
 attribute [extern "lean_nat_to_int"] Int.ofNat
@@ -28,32 +55,69 @@ instance : OfNat Int n where
 namespace Int
 instance : Inhabited Int := ⟨ofNat 0⟩
 
+/-- Negation of a natural number. -/
 def negOfNat : Nat → Int
   | 0      => 0
   | succ m => negSucc m
 
 set_option bootstrap.genMatcherCode false in
+/-- Negation of an integer.
+
+  Implemented by efficient native code. -/
 @[extern "lean_int_neg"]
 protected def neg (n : @& Int) : Int :=
   match n with
   | ofNat n   => negOfNat n
   | negSucc n => succ n
 
+/-
+  The `Neg Int` default instance must have priority higher than `low`
+  since the default instance `OfNat Nat n` has `low` priority.
+
+  ```
+  #check -42
+  ```
+-/
+@[default_instance mid]
+instance : Neg Int where
+  neg := Int.neg
+
+/-- Subtraction of two natural numbers. -/
 def subNatNat (m n : Nat) : Int :=
   match (n - m : Nat) with
   | 0        => ofNat (m - n)  -- m ≥ n
   | (succ k) => negSucc k
 
 set_option bootstrap.genMatcherCode false in
+/-- Addition of two integers.
+
+  ```
+  #eval (7 : Int) + (6 : Int) -- 13
+  #eval (6 : Int) + (-6 : Int) -- 0
+  ```
+
+  Implemented by efficient native code. -/
 @[extern "lean_int_add"]
-  protected def add (m n : @& Int) : Int :=
+protected def add (m n : @& Int) : Int :=
   match m, n with
   | ofNat m,   ofNat n   => ofNat (m + n)
   | ofNat m,   negSucc n => subNatNat m (succ n)
   | negSucc m, ofNat n   => subNatNat n (succ m)
   | negSucc m, negSucc n => negSucc (succ (m + n))
 
+instance : Add Int where
+  add := Int.add
+
 set_option bootstrap.genMatcherCode false in
+/-- Multiplication of two integers.
+
+  ```
+  #eval (63 : Int) * (6 : Int) -- 378
+  #eval (6 : Int) * (-6 : Int) -- -36
+  #eval (7 : Int) * (0 : Int) -- 0
+  ```
+
+  Implemented by efficient native code. -/
 @[extern "lean_int_mul"]
 protected def mul (m n : @& Int) : Int :=
   match m, n with
@@ -62,21 +126,18 @@ protected def mul (m n : @& Int) : Int :=
   | negSucc m, ofNat n   => negOfNat (succ m * n)
   | negSucc m, negSucc n => ofNat (succ m * succ n)
 
-/--
-  The `Neg Int` default instance must have priority higher than `low` since
-  the default instance `OfNat Nat n` has `low` priority.
-  ```
-  #check -42
-  ```
--/
-@[default_instance mid]
-instance : Neg Int where
-  neg := Int.neg
-instance : Add Int where
-  add := Int.add
 instance : Mul Int where
   mul := Int.mul
 
+/-- Subtraction of two integers.
+
+  ```
+  #eval (63 : Int) - (6 : Int) -- 57
+  #eval (7 : Int) - (0 : Int) -- 7
+  #eval (0 : Int) - (7 : Int) -- -7
+  ```
+
+  Implemented by efficient native code. -/
 @[extern "lean_int_sub"]
 protected def sub (m n : @& Int) : Int :=
   m + (- n)
@@ -84,20 +145,33 @@ protected def sub (m n : @& Int) : Int :=
 instance : Sub Int where
   sub := Int.sub
 
+/-- A proof that an `Int` is non-negative. -/
 inductive NonNeg : Int → Prop where
+  /-- Sole constructor, proving that `ofNat n` is positive. -/
   | mk (n : Nat) : NonNeg (ofNat n)
 
+/-- Definition of `a ≤ b`, encoded as `b - a ≥ 0`. -/
 protected def le (a b : Int) : Prop := NonNeg (b - a)
 
 instance : LE Int where
   le := Int.le
 
+/-- Definition of `a < b`, encoded as `a + 1 ≤ b`. -/
 protected def lt (a b : Int) : Prop := (a + 1) ≤ b
 
 instance : LT Int where
   lt := Int.lt
 
 set_option bootstrap.genMatcherCode false in
+/-- Decides equality between two `Int`s.
+
+  ```
+  #eval (7 : Int) = (3 : Int) + (4 : Int) -- true
+  #eval (6 : Int) = (3 : Int) * (2 : Int) -- true
+  #eval ¬ (6 : Int) = (3 : Int) -- true
+  ```
+
+  Implemented by efficient native code. -/
 @[extern "lean_int_dec_eq"]
 protected def decEq (a b : @& Int) : Decidable (a = b) :=
   match a, b with
@@ -113,27 +187,93 @@ protected def decEq (a b : @& Int) : Decidable (a = b) :=
 instance : DecidableEq Int := Int.decEq
 
 set_option bootstrap.genMatcherCode false in
+/-- Decides whether an integer is negative.
+
+  ```
+  #eval (7 : Int).decNonneg.decide -- true
+  #eval (0 : Int).decNonneg.decide -- true
+  #eval ¬ (-7 : Int).decNonneg.decide -- true
+  ```
+
+  Implemented by efficient native code. -/
 @[extern "lean_int_dec_nonneg"]
 private def decNonneg (m : @& Int) : Decidable (NonNeg m) :=
   match m with
   | ofNat m   => isTrue <| NonNeg.mk m
   | negSucc _ => isFalse <| fun h => nomatch h
 
+/-- Decides whether `a ≤ b`.
+
+  ```
+  #eval ¬ ( (7 : Int) ≤ (0 : Int) ) -- true
+  #eval (0 : Int) ≤ (0 : Int) -- true
+  #eval (7 : Int) ≤ (10 : Int) -- true
+  ```
+
+  Implemented by efficient native code. -/
 @[extern "lean_int_dec_le"]
 instance decLe (a b : @& Int) : Decidable (a ≤ b) :=
   decNonneg _
 
+/-- Decides whether `a < b`.
+
+  ```
+  #eval `¬ ( (7 : Int) < 0 )` -- true
+  #eval `¬ ( (0 : Int) < 0 )` -- true
+  #eval `(7 : Int) < 10` -- true
+  ```
+
+  Implemented by efficient native code. -/
 @[extern "lean_int_dec_lt"]
 instance decLt (a b : @& Int) : Decidable (a < b) :=
   decNonneg _
 
 set_option bootstrap.genMatcherCode false in
+/-- Absolute value (`Nat`) of an integer.
+
+  ```
+  #eval (7 : Int).natAbs -- 7
+  #eval (0 : Int).natAbs -- 0
+  #eval (-11 : Int).natAbs -- 11
+  ```
+
+  Implemented by efficient native code. -/
 @[extern "lean_nat_abs"]
 def natAbs (m : @& Int) : Nat :=
   match m with
   | ofNat m   => m
   | negSucc m => m.succ
 
+/-- Integer division. This function uses the
+  [*"T-rounding"*][t-rounding] (**T**runcation-rounding) convention,
+  meaning that it rounds toward zero. Also note that division by zero
+  is defined to equal zero.
+
+  The relation between integer division and modulo is found in [the
+  `Int.mod_add_div` theorem in std][theo mod_add_div] which states
+  that `a % b + b * (a / b) = a`, unconditionally.
+
+  [t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862
+  [theo mod_add_div]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.mod_add_div#doc
+
+  Examples:
+
+  ```
+  #eval (7 : Int) / (0 : Int) -- 0
+  #eval (0 : Int) / (7 : Int) -- 0
+
+  #eval (12 : Int) / (6 : Int) -- 2
+  #eval (12 : Int) / (-6 : Int) -- -2
+  #eval (-12 : Int) / (6 : Int) -- -2
+  #eval (-12 : Int) / (-6 : Int) -- 2
+
+  #eval (12 : Int) / (7 : Int) -- 1
+  #eval (12 : Int) / (-7 : Int) -- -1
+  #eval (-12 : Int) / (7 : Int) -- -2
+  #eval (-12 : Int) / (-7 : Int) -- 2
+  ```
+
+  Implemented by efficient native code. -/
 @[extern "lean_int_div"]
 def div : (@& Int) → (@& Int) → Int
   | ofNat m,   ofNat n   => ofNat (m / n)
@@ -141,6 +281,36 @@ def div : (@& Int) → (@& Int) → Int
   | negSucc m, ofNat n   => -ofNat (succ m / n)
   | negSucc m, negSucc n => ofNat (succ m / succ n)
 
+instance : Div Int where
+  div := Int.div
+
+/-- Integer modulo. This function uses the
+  [*"T-rounding"*][t-rounding] (**T**runcation-rounding) convention
+  to pair with `Int.div`, meaning that `a % b + b * (a / b) = a`
+  unconditionally (see [`Int.mod_add_div`][theo mod_add_div]). In
+  particular, `a % 0 = a`.
+
+  [t-rounding]: https://dl.acm.org/doi/pdf/10.1145/128861.128862
+  [theo mod_add_div]: https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Int.mod_add_div#doc
+
+  Examples:
+
+  ```
+  #eval (7 : Int) % (0 : Int) -- 7
+  #eval (0 : Int) % (7 : Int) -- 0
+
+  #eval (12 : Int) % (6 : Int) -- 0
+  #eval (12 : Int) % (-6 : Int) -- 0
+  #eval (-12 : Int) % (6 : Int) -- 0
+  #eval (-12 : Int) % (-6 : Int) -- 0
+
+  #eval (12 : Int) % (7 : Int) -- 5
+  #eval (12 : Int) % (-7 : Int) -- 5
+  #eval (-12 : Int) % (7 : Int) -- 2
+  #eval (-12 : Int) % (-7 : Int) -- 2
+  ```
+
+  Implemented by efficient native code. -/
 @[extern "lean_int_mod"]
 def mod : (@& Int) → (@& Int) → Int
   | ofNat m,   ofNat n   => ofNat (m % n)
@@ -148,16 +318,31 @@ def mod : (@& Int) → (@& Int) → Int
   | negSucc m, ofNat n   => -ofNat (succ m % n)
   | negSucc m, negSucc n => -ofNat (succ m % succ n)
 
-instance : Div Int where
-  div := Int.div
-
 instance : Mod Int where
   mod := Int.mod
 
+/-- Turns an integer into a natural number, negative numbers become
+  `0`.
+
+  ```
+  #eval (7 : Int).toNat -- 7
+  #eval (0 : Int).toNat -- 0
+  #eval (-7 : Int).toNat -- 0
+  ```
+-/
 def toNat : Int → Nat
   | ofNat n   => n
   | negSucc _ => 0
 
+/-- Power of an integer to some natural number.
+
+  ```
+  #eval (2 : Int) ^ 4 -- 16
+  #eval (10 : Int) ^ 0 -- 1
+  #eval (0 : Int) ^ 10 -- 0
+  #eval (-7 : Int) ^ 3 -- -343
+  ```
+-/
 protected def pow (m : Int) : Nat → Int
   | 0      => 1
   | succ n => Int.pow m n * m