diff --git a/Coq/Coquelicot/PSeries.theory.xml b/Coq/Coquelicot/PSeries.theory.xml index dea0fcb..31b023a 100644 --- a/Coq/Coquelicot/PSeries.theory.xml +++ b/Coq/Coquelicot/PSeries.theory.xml @@ -60,7 +60,7 @@ COPYING file for more details. <ht:REQUIRE uri="cic:/Coquelicot/Derive"/> <ht:REQUIRE uri="cic:/Coquelicot/Seq_fct"/> <ht:REQUIRE uri="cic:/Coquelicot/Series"/> - This file describes power series: Σ a<sub>k</sub> + This file describes power series: Sigma a<sub>k</sub> x<sup>k</sup>. It contains definition, equivalence with the standard library, differentiability, integrability, and many results about the convergence circle. <ht:SECTION uri="cic:/Coquelicot/PSeries/Definitions" line="32"> diff --git a/Coq/Coquelicot/Rbar.theory.xml b/Coq/Coquelicot/Rbar.theory.xml index c27518c..97cab72 100644 --- a/Coq/Coquelicot/Rbar.theory.xml +++ b/Coq/Coquelicot/Rbar.theory.xml @@ -49,7 +49,7 @@ COPYING file for more details. <ht:REQUIRE uri="cic:/mathcomp/ssreflect/ssreflect"/> <ht:REQUIRE uri="cic:/Coquelicot/Rcomplements"/> This file contains the definition and properties of the set - <span class="inlinecode"><span class="id" title="var">R</span></span> ∪ {+ ∞} ∪ {- ∞} denoted by <span class="inlinecode"><span class="id" title="var">Rbar</span></span>. We have defined: + <span class="inlinecode"><span class="id" title="var">R</span></span> ∪ {+ infin} ∪ {- infin} denoted by <span class="inlinecode"><span class="id" title="var">Rbar</span></span>. We have defined: <ul class="doclist"> <li> coercions from <span class="inlinecode"><span class="id" title="var">R</span></span> to <span class="inlinecode"><span class="id" title="var">Rbar</span></span> and vice versa (<span class="inlinecode"><span class="id" title="var">Finite</span></span> gives <span class="inlinecode"><span class="id" title="var">R0</span></span> at infinity points)