doc(data/real/*): add a few docstrings, ereal.has_zero, and `ereal.…

…inhabited` (#4378)

src/data/real/basic.lean

@@ -10,6 +10,8 @@ import order.conditionally_complete_lattice
 import data.real.cau_seq_completion
 import algebra.archimedean
 
+/-- The type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational
+numbers. -/
 def real := @cau_seq.completion.Cauchy ℚ _ _ _ abs _
 notation `ℝ` := real
 

src/data/real/ereal.lean

@@ -31,7 +31,6 @@ In Isabelle they define + - * and / (making junk choices for things like -∞ +
 and then prove whatever bits of the ordered ring/field axioms still hold. They
 also do some limits stuff (liminf/limsup etc).
 See https://isabelle.in.tum.de/dist/library/HOL/HOL-Library/Extended_Real.html
-
 -/
 
 /-- ereal : The type `[-∞, ∞]` -/
@@ -48,7 +47,10 @@ by { unfold_coes, norm_num }
 @[simp, norm_cast] protected lemma coe_real_inj' {x y : ℝ} : (x : ereal) = (y : ereal) ↔ x = y :=
 by { unfold_coes, simp [option.some_inj] }
 
-/- neg -/
+instance : has_zero ereal := ⟨(0 : ℝ)⟩
+instance : inhabited ereal := ⟨0⟩
+
+/-! ### Negation -/
 
 /-- negation on ereal -/
 protected def neg : ereal → ereal

src/data/real/nnreal.lean

@@ -38,6 +38,7 @@ iff.intro nnreal.eq (congr_arg coe)
 lemma ne_iff {x y : ℝ≥0} : (x : ℝ) ≠ (y : ℝ) ↔ x ≠ y :=
 not_iff_not_of_iff $ nnreal.eq_iff
 
+/-- Reinterpret a real number `r` as a non-negative real number. Returns `0` if `r < 0`. -/
 protected def of_real (r : ℝ) : ℝ≥0 := ⟨max r 0, le_max_right _ _⟩
 
 lemma coe_of_real (r : ℝ) (hr : 0 ≤ r) : (nnreal.of_real r : ℝ) = r :=