added doc

Author: adjevahi

theories/lebesgue_integral_theory/simple_functions.v

@@ -28,8 +28,9 @@ From mathcomp Require Import borel_hierarchy.
 (*                                                                            *)
 (* Detailed contents:                                                         *)
 (* ````                                                                       *)
-(*         {sfun T >-> R} == type of simple functions                         *)
-(*                           They form a (potentially zero) ring.             *)
+(*         {sfun aT >-> bT} == type of simple functions                       *)
+(*                           They can form a ring or a module depending on    *)
+(*                            the structure of bT                             *)
 (*       {nnsfun T >-> R} == type of non-negative simple functions            *)
 (*          indic_sfun mD := mindic _ mD                                      *)
 (*             cst_sfun r == constant simple function                         *)