docs(data/*/sqrt): add one module docstring and expand the other (#7973)

src/data/int/sqrt.lean

@@ -5,14 +5,20 @@ Authors: Kenny Lau
 -/
 import data.nat.sqrt
 
+/-!
+# Square root of integers
+
+This file defines the square root function on integers. `int.sqrt z` is the greatest integer `r`
+such that `r * r ≤ z`. If `z ≤ 0`, then `int.sqrt z = 0`.
+-/
+
 namespace int
 
-/-- `sqrt n` is the square root of an integer `n`. If `n` is not a
-  perfect square, and is positive, it returns the largest `k:ℤ` such
-  that `k*k ≤ n`. If it is negative, it returns 0. For example,
-  `sqrt 2 = 1` and `sqrt 1 = 1` and `sqrt (-1) = 0` -/
-@[pp_nodot] def sqrt (n : ℤ) : ℤ :=
-nat.sqrt $ int.to_nat n
+/-- `sqrt z` is the square root of an integer `z`. If `z` is positive, it returns the largest
+integer `r` such that `r * r ≤ n`. If it is negative, it returns `0`. For example, `sqrt (-1) = 0`,
+`sqrt 1 = 1`, `sqrt 2 = 1` -/
+@[pp_nodot] def sqrt (z : ℤ) : ℤ :=
+nat.sqrt $ int.to_nat z
 
 theorem sqrt_eq (n : ℤ) : sqrt (n*n) = n.nat_abs :=
 by rw [sqrt, ← nat_abs_mul_self, to_nat_coe_nat, nat.sqrt_eq]

src/data/nat/sqrt.lean

@@ -4,14 +4,19 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Johannes Hölzl, Mario Carneiro
 -/
 import data.int.basic
+
 /-!
 # Square root of natural numbers
 
-An efficient binary implementation of a (`sqrt n`) function that
-returns `s` such that
-```
-s*s ≤ n ≤ s*s + s + s
-```
+This file defines an efficient binary implementation of the square root function that returns the
+unique `r` such that `r * r ≤ n < (r + 1) * (r + 1)`. It takes advantage of the binary
+representation by replacing the multiplication by 2 appearing in
+`(a + b)^2 = a^2 + 2 * a * b + b^2` by a bitmask manipulation.
+
+## Reference
+
+See [Wikipedia, *Methods of computing square roots*]
+[https://en.wikipedia.org/wiki/Methods_of_computing_square_roots#Binary_numeral_system_(base_2)].
 -/
 namespace nat