fix(*): arsinh and complex.basic had module docs at the wrong position (

#6230) This is fixed and the module doc for `complex.basic` is expanded slightly.
leanprover-community · Feb 14, 2021 · b9af22d · b9af22d
1 parent c54a8d0
commit b9af22d
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 4 deletions.
diff --git a/src/analysis/special_functions/arsinh.lean b/src/analysis/special_functions/arsinh.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: James Arthur, Chris Hughes, Shing Tak Lam
 -/
 import analysis.special_functions.trigonometric
-noncomputable theory
 
 /-!
 # Inverse of the sinh function
@@ -23,6 +22,7 @@ inverse, arsinh.
 
 arsinh, arcsinh, argsinh, asinh, sinh injective, sinh bijective, sinh surjective
 -/
+noncomputable theory
 
 namespace real
 

diff --git a/src/data/complex/basic.lean b/src/data/complex/basic.lean
@@ -5,14 +5,16 @@ Authors: Kevin Buzzard, Mario Carneiro
 -/
 import data.real.sqrt
 
-open_locale big_operators
-
 /-!
 # The complex numbers
 
-The complex numbers are modelled as ℝ^2 in the obvious way.
+The complex numbers are modelled as ℝ^2 in the obvious way and it is shown that they form a field
+of characteristic zero. The result that the complex numbers are algebraically closed, see
+`field_theory.algebraic_closure`.
 -/
 
+open_locale big_operators
+
 /-! ### Definition and basic arithmmetic -/
 
 /-- Complex numbers consist of two `real`s: a real part `re` and an imaginary part `im`. -/