docs(data/real/*): add module docstrings (#8145)

leanprover-community · Jul 3, 2021 · edb72b4 · edb72b4
1 parent 10f6c2c
commit edb72b4
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 16 deletions.
diff --git a/src/data/real/basic.lean b/src/data/real/basic.lean
@@ -2,15 +2,20 @@
 Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Floris van Doorn
-
-The (classical) real numbers ℝ. This is a direct construction
-from Cauchy sequences.
 -/
 import order.conditionally_complete_lattice
 import data.real.cau_seq_completion
 import algebra.archimedean
 import algebra.star.basic
 
+/-!
+# Real numbers from Cauchy sequences
+
+This file defines `ℝ` as the type of equivalence classes of Cauchy sequences of rational numbers.
+This choice is motivated by how easy it is to prove that `ℝ` is a commutative ring, by simply
+lifting everything to `ℚ`.
+-/
+
 /-- The type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
 numbers. -/
 structure real := of_cauchy ::
@@ -246,16 +251,16 @@ noncomputable instance : linear_ordered_field ℝ :=
 
 /- Extra instances to short-circuit type class resolution -/
 
-noncomputable instance : linear_ordered_add_comm_group ℝ := by apply_instance
-noncomputable instance field : field ℝ := by apply_instance
-noncomputable instance : division_ring ℝ           := by apply_instance
-noncomputable instance : integral_domain ℝ         := by apply_instance
-noncomputable instance : distrib_lattice ℝ := by apply_instance
-noncomputable instance : lattice ℝ         := by apply_instance
-noncomputable instance : semilattice_inf ℝ := by apply_instance
-noncomputable instance : semilattice_sup ℝ := by apply_instance
-noncomputable instance : has_inf ℝ         := by apply_instance
-noncomputable instance : has_sup ℝ         := by apply_instance
+noncomputable instance : linear_ordered_add_comm_group ℝ          := by apply_instance
+noncomputable instance field : field ℝ                            := by apply_instance
+noncomputable instance : division_ring ℝ                          := by apply_instance
+noncomputable instance : integral_domain ℝ                        := by apply_instance
+noncomputable instance : distrib_lattice ℝ                        := by apply_instance
+noncomputable instance : lattice ℝ                                := by apply_instance
+noncomputable instance : semilattice_inf ℝ                        := by apply_instance
+noncomputable instance : semilattice_sup ℝ                        := by apply_instance
+noncomputable instance : has_inf ℝ                                := by apply_instance
+noncomputable instance : has_sup ℝ                                := by apply_instance
 noncomputable instance decidable_lt (a b : ℝ) : decidable (a < b) := by apply_instance
 noncomputable instance decidable_le (a b : ℝ) : decidable (a ≤ b) := by apply_instance
 noncomputable instance decidable_eq (a b : ℝ) : decidable (a = b) := by apply_instance

diff --git a/src/data/real/cau_seq_completion.lean b/src/data/real/cau_seq_completion.lean
@@ -2,12 +2,16 @@
 Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Robert Y. Lewis
-
-Generalizes the Cauchy completion of (ℚ, abs) to the completion of a
-commutative ring with absolute value.
 -/
 import data.real.cau_seq
 
+/-!
+# Cauchy completion
+
+This file generalizes the Cauchy completion of `(ℚ, abs)` to the completion of a commutative ring
+with absolute value.
+-/
+
 namespace cau_seq.completion
 open cau_seq