doc(algebra/{archimedean, char_zero}): provide docstrings (#6010)

src/algebra/archimedean.lean

@@ -2,12 +2,32 @@
 Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
-
-Archimedean groups and fields.
 -/
+
 import algebra.field_power
 import data.rat
 
+/-!
+# Archimedean groups and fields.
+
+This file defines the archimedean property for ordered groups and proves several results connected
+to this notion. Being archimedean means that for all elements `x` and `y>0` there exists a natural
+number `n` such that `x ≤ n •ℕ y`.
+
+## Main definitions
+
+* `archimedean` is a typeclass for an ordered additive commutative monoid to have the archimedean
+  property.
+* `archimedean.floor_ring` defines a floor function on an archimedean linearly ordered ring making
+  it into a `floor_ring`.
+* `round` defines a function rounding to the nearest integer for a linearly ordered field which is
+  also a floor ring.
+
+## Main statements
+
+* `ℕ`, `ℤ`, and `ℚ` are archimedean.
+-/
+
 variables {α : Type*}
 
 /-- An ordered additive commutative monoid is called `archimedean` if for any two elements `x`, `y`

src/algebra/char_zero.lean

@@ -2,13 +2,37 @@
 Copyright (c) 2014 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
-
-Natural homomorphism from the natural numbers into a monoid with one.
 -/
+
 import data.nat.cast
 import data.fintype.basic
 import tactic.wlog
 
+/-!
+# Characteristic zero
+
+A ring `R` is called of characteristic zero if every natural number `n` is non-zero when considered
+as an element of `R`. Since this definition doesn't mention the multiplicative structure of `R`
+except for the existence of `1` in this file characteristic zero is defined for additive monoids
+with `1`.
+
+## Main definition
+
+`char_zero` is the typeclass of an additive monoid with one such that the natural homomorphism
+from the natural numbers into it is injective.
+
+## Main statements
+
+* A linearly ordered semiring has characteristic zero.
+* Characteristic zero implies that the additive monoid is infinite.
+
+## TODO
+
+* Once order of a group is defined for infinite additive monoids redefine or at least connect to
+  order of `1` in the additive monoid with one.
+* Unify with `char_p` (possibly using an out-parameter)
+-/
+
 /-- Typeclass for monoids with characteristic zero.
   (This is usually stated on fields but it makes sense for any additive monoid with 1.) -/
 class char_zero (R : Type*) [add_monoid R] [has_one R] : Prop :=