feat(docs/*) Starts addings links and stubs to docs

Author: PatrickMassot

README.md

@@ -5,14 +5,15 @@
 Lean standard library
 
 Besides [Lean's general documentation](https://leanprover.github.io/documentation/), the documentation of mathlib consists of:
-* a description of [currently covered theories](docs/theories.md)
-* an explanation of [naming conventions](docs/naming.md) that is useful
+
+- a description of [currently covered theories](docs/theories.md)
+- an explanation of [naming conventions](docs/naming.md) that is useful
   to find or contribute definitions and lemmas
-* a description of [tactics](docs/tactics.md) introduced in mathlib
-* a [style guide](docs/style.md) for contributors
-* a tentative list of [work in progress](docs/wip.md) to make sure
+- a description of [tactics](docs/tactics.md) introduced in mathlib
+- a [style guide](docs/style.md) for contributors
+- a tentative list of [work in progress](docs/wip.md) to make sure
   efforts are not duplicated without collaboration
-* a [guide](docs/elan.md) on installing Lean and mathlib with elan.
+- a [guide](docs/elan.md) on installing Lean and mathlib with elan.
 
 This repository also contains [extra Lean documentation](docs/extras.md)
 not specific to mathlib.

docs/extras.md

@@ -1,6 +1,7 @@
 # Extra Lean documentation
 
 * The [conversion tactic mode](extras/conv.md)
-* Some [notes on simp](extras/simp.md)
+* The [simplifier](extras/simp.md)
 * The [calc environment](extras/calc.md)
 * The [congruence closure tactic](extras/cc.md)
+* [Well founded recursion](extras/well_founded_recursion.md)

docs/theories.md

@@ -3,20 +3,24 @@
 The core Lean library (imported automatically) and mathlib, the
 mathematics library, between them know quite a lot of basic
 undergraduate-level mathematical definitions. This page is an overview
-of the definitions and lemmas within these libraries that 
+of the definitions and lemmas within these libraries that
 mathematicians might be interested in.
 
-Note that there are many other things within these libraries which 
-are not documented here (for example red black trees and so on);  these
+Note that there are many other things within these libraries which
+are not documented here (for example red black trees and so on); these
 missing definitions and theorems may well be of interest to computer
 scientists.
 
-* [Groups](theories/groups.md)
-* [Rings and fields](theories/rings_fields.md)
-* [Partial and total orders](theories/orders.md)
 * [Functions between types](theories/functions.md)
-* [Relations on types](theories/relations.md)
-* [Quotients and equivalence classes](theories/quotients.md)
+* [Relations on types, quotients](theories/relations.md)
+* [Partial and total orders, lattices](theories/orders.md)
 * [Sets and set like objects](theories/sets.md)
+* [Categories](theories/categories.md)
 * [The natural numbers](theories/naturals.md)
-* [The integers.](theories/integers.md)
+* [The integers](theories/integers.md)
+* [Groups](theories/groups.md)
+* [Rings and fields](theories/rings_fields.md)
+* [Linear algebra](theories/linear_algebra.md)
+* [Number theory](theories/number_theory.md)
+* [Topological, uniform and metric spaces](theories/topological_spaces.md)
+* [Measure theory](theories/measure.md)

docs/theories/linear_algebra.md

@@ -0,0 +1,6 @@
+# Maths in Lean : Linear algebra
+
+The definitions of modules and vector fields are in `algebra/module`.
+In `linear_algebra` are their products,
+sub-objects, quotients, and morphisms. There are also (unordered) bases
+and the definition of dimension of a vector space. But there is nothing specific to finite dimension and matrices yet.

docs/theories/measure.md

@@ -0,0 +1,4 @@
+# Maths in Lean : Measure theory
+
+In `analysis/measure_theory`, are measure spaces, measurable functions,
+outer measures, Lebesgue measure, but no integral yet.

docs/theories/number_theory.md

@@ -0,0 +1,12 @@
+# Maths in Lean : number theory
+
+In addition to the basic operations on `ℤ` and `ℚ`, there are
+things on diophantine sets in `number_theory/dioph`, and on Pell's
+equation in `number_theory/pell`. Those things are used to prove
+Matiyasevič's theorem, which states that the power function is
+Diophantine, forming the last and hardest piece of the MRDP theorem of
+the unsolvability of Hilbert's 10th problem (asking for algorithmic
+solution to all diophantine equations). 
+
+A set `S ⊆ ℕ^α` is diophantine if there exists a polynomial on 
+`α ⊕ β` such that `v ∈ S` iff there exists `t : ℕ^β` with `p (v, t) = 0`. 

docs/theories/polynomials.md

@@ -0,0 +1,9 @@
+# Maths in Lean : polynomials
+
+General purposes multivariate polynomials over rings are defined in
+`linear_algebra/mv_polynomial.lean`. Univariate polynomials get a special
+treatment in `data/polynomial`. Multivariate polynomial over `ℤ` 
+get a special treatment with a view towards diophantine equations in
+`number_theory/dioph`. 
+
+

docs/theories/quotients.md

@@ -5,20 +5,29 @@ definitions of the basic relations on types such as `reflexive`,
 `irreflexive`, `symmetric`, `anti_symmetric`, `transitive`,
 `equivalence`, and `total` (i.e. for all `x` and `y`,
 `x R y` or `y R x`).
-One key usage of equivalence relations is the construction of
-equivalence classes; this is well documented in 
-[Theorem Proving In Lean](https://leanprover.github.io/theorem_proving_in_lean/).
 
 ### Examples.
 
 ```lean
 variable (X : Type*)
 
 -- equality is symmetric
-example : symmetric (λ x y : X, x=y) := 
+example : symmetric (λ x y : X, x = y) := 
 λ x y, eq.symm
 
 -- "less than" is transitive on the natural numbers.
-example : transitive (λ a b : nat, a<b) := 
-λ x y z : nat, lt_trans
+example : transitive (λ a b : ℕ, a < b) := 
+λ x y z : ℕ, lt_trans
 ```
+
+Transitivity of relations allows to use them in [calc environments](../extras/calc.md).
+
+One key usage of equivalence relations is the construction of quotients.
+A type with an equivalence relation on it is called a `setoid` in Lean.
+Setoids are defined in `init/data/setoid.lean` and the quotient type
+corresponding to the equivalence classes of the equivalence relation is
+defined in `init/data/quot.lean` . The online document 
+*Theorem Proving In Lean* has 
+[quite a good section about setoids and quotients](https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#quotients)
+
+A nice mathematical example can be found in `linear_algebra/quotient_module`.