matita/contribs/CoRN-Decl/algebra/CSums.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSums".
  18
  19 include "CoRN.ma".
  20
  21 (* $Id: CSums.v,v 1.8 2004/04/23 10:00:54 lcf Exp $ *)
  22
  23 (*#* printing Sum0 %\ensuremath{\sum_0}% #&sum;<sub>0</sub># *)
  24
  25 (*#* printing Sum1 %\ensuremath{\sum_1}% #&sum;<sub>1</sub># *)
  26
  27 (*#* printing Sum2 %\ensuremath{\sum_2}% #&sum;<sub>2</sub># *)
  28
  29 (*#* printing Sum %\ensuremath{\sum}% #&sum;# *)
  30
  31 (*#* printing Sumx %\ensuremath{\sum'}% #&sum;'&*)
  32
  33 include "algebra/CAbGroups.ma".
  34
  35 (*#* * Sums
  36
  37 %\begin{convention}% Let [G] be an abelian group.
  38 %\end{convention}%
  39 *)
  40
  41 (* UNEXPORTED
  42 Section Sums
  43 *)
  44
  45 alias id "G" = "cic:/CoRN/algebra/CSums/Sums/G.var".
  46
  47 (* Sum1 and Sum use subtraction *)
  48
  49 inline "cic:/CoRN/algebra/CSums/Sumlist.con".
  50
  51 inline "cic:/CoRN/algebra/CSums/Sumx.con".
  52
  53 (*#*
  54 It is sometimes useful to view a function defined on $\{0,\ldots,i-1\}$
  55 #{0, ... i-1}# as a function on the natural numbers which evaluates to
  56 [Zero] when the input is greater than or equal to [i].
  57 *)
  58
  59 inline "cic:/CoRN/algebra/CSums/part_tot_nat_fun.con".
  60
  61 inline "cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch1.con".
  62
  63 inline "cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch2.con".
  64
  65 (*#* [Sum0] defines the sum for [i=0..(n-1)] *)
  66
  67 inline "cic:/CoRN/algebra/CSums/Sum0.con".
  68
  69 (*#* [Sum1] defines the sum for [i=m..(n-1)] *)
  70
  71 inline "cic:/CoRN/algebra/CSums/Sum1.con".
  72
  73 inline "cic:/CoRN/algebra/CSums/Sum.con".
  74
  75 (* Sum i=m..n *)
  76
  77 (*#* [Sum2] is similar to [Sum1], but does not require the summand to be
  78 defined outside where it is being added. *)
  79
  80 inline "cic:/CoRN/algebra/CSums/Sum2.con".
  81
  82 inline "cic:/CoRN/algebra/CSums/Sum_one.con".
  83
  84 (* UNEXPORTED
  85 Hint Resolve Sum_one: algebra.
  86 *)
  87
  88 inline "cic:/CoRN/algebra/CSums/Sum_empty.con".
  89
  90 (* UNEXPORTED
  91 Hint Resolve Sum_empty: algebra.
  92 *)
  93
  94 inline "cic:/CoRN/algebra/CSums/Sum_Sum.con".
  95
  96 (* UNEXPORTED
  97 Hint Resolve Sum_Sum: algebra.
  98 *)
  99
 100 inline "cic:/CoRN/algebra/CSums/Sum_first.con".
 101
 102 inline "cic:/CoRN/algebra/CSums/Sum_last.con".
 103
 104 (* UNEXPORTED
 105 Hint Resolve Sum_last: algebra.
 106 *)
 107
 108 inline "cic:/CoRN/algebra/CSums/Sum_last'.con".
 109
 110 (*#*
 111 We add some extensionality results which will be quite useful
 112 when working with integration.
 113 *)
 114
 115 inline "cic:/CoRN/algebra/CSums/Sum0_strext.con".
 116
 117 inline "cic:/CoRN/algebra/CSums/Sum_strext.con".
 118
 119 inline "cic:/CoRN/algebra/CSums/Sumx_strext.con".
 120
 121 inline "cic:/CoRN/algebra/CSums/Sum0_strext'.con".
 122
 123 inline "cic:/CoRN/algebra/CSums/Sum_strext'.con".
 124
 125 inline "cic:/CoRN/algebra/CSums/Sum0_wd.con".
 126
 127 inline "cic:/CoRN/algebra/CSums/Sum_wd.con".
 128
 129 inline "cic:/CoRN/algebra/CSums/Sumx_wd.con".
 130
 131 inline "cic:/CoRN/algebra/CSums/Sum_wd'.con".
 132
 133 inline "cic:/CoRN/algebra/CSums/Sum2_wd.con".
 134
 135 inline "cic:/CoRN/algebra/CSums/Sum0_plus_Sum0.con".
 136
 137 (* UNEXPORTED
 138 Hint Resolve Sum0_plus_Sum0: algebra.
 139 *)
 140
 141 inline "cic:/CoRN/algebra/CSums/Sum_plus_Sum.con".
 142
 143 inline "cic:/CoRN/algebra/CSums/Sumx_plus_Sumx.con".
 144
 145 inline "cic:/CoRN/algebra/CSums/Sum2_plus_Sum2.con".
 146
 147 inline "cic:/CoRN/algebra/CSums/inv_Sum0.con".
 148
 149 (* UNEXPORTED
 150 Hint Resolve inv_Sum0: algebra.
 151 *)
 152
 153 inline "cic:/CoRN/algebra/CSums/inv_Sum.con".
 154
 155 (* UNEXPORTED
 156 Hint Resolve inv_Sum: algebra.
 157 *)
 158
 159 inline "cic:/CoRN/algebra/CSums/inv_Sumx.con".
 160
 161 inline "cic:/CoRN/algebra/CSums/inv_Sum2.con".
 162
 163 inline "cic:/CoRN/algebra/CSums/Sum_minus_Sum.con".
 164
 165 (* UNEXPORTED
 166 Hint Resolve Sum_minus_Sum: algebra.
 167 *)
 168
 169 inline "cic:/CoRN/algebra/CSums/Sumx_minus_Sumx.con".
 170
 171 inline "cic:/CoRN/algebra/CSums/Sum2_minus_Sum2.con".
 172
 173 inline "cic:/CoRN/algebra/CSums/Sum_apzero.con".
 174
 175 inline "cic:/CoRN/algebra/CSums/Sum_zero.con".
 176
 177 inline "cic:/CoRN/algebra/CSums/Sum_term.con".
 178
 179 inline "cic:/CoRN/algebra/CSums/Sum0_shift.con".
 180
 181 (* UNEXPORTED
 182 Hint Resolve Sum0_shift: algebra.
 183 *)
 184
 185 inline "cic:/CoRN/algebra/CSums/Sum_shift.con".
 186
 187 inline "cic:/CoRN/algebra/CSums/Sum_big_shift.con".
 188
 189 inline "cic:/CoRN/algebra/CSums/Sumx_Sum0.con".
 190
 191 (* UNEXPORTED
 192 End Sums
 193 *)
 194
 195 (* UNEXPORTED
 196 Implicit Arguments Sum [G].
 197 *)
 198
 199 (* UNEXPORTED
 200 Implicit Arguments Sum0 [G].
 201 *)
 202
 203 (* UNEXPORTED
 204 Implicit Arguments Sumx [G n].
 205 *)
 206
 207 (* UNEXPORTED
 208 Implicit Arguments Sum2 [G m n].
 209 *)
 210
 211 (*#*
 212 The next results are useful for calculating some special sums,
 213 often referred to as ``Mengolli Sums''.
 214 %\begin{convention}% Let [G] be an abelian group.
 215 %\end{convention}%
 216 *)
 217
 218 (* UNEXPORTED
 219 Section More_Sums
 220 *)
 221
 222 alias id "G" = "cic:/CoRN/algebra/CSums/More_Sums/G.var".
 223
 224 inline "cic:/CoRN/algebra/CSums/Mengolli_Sum.con".
 225
 226 inline "cic:/CoRN/algebra/CSums/Mengolli_Sum_gen.con".
 227
 228 inline "cic:/CoRN/algebra/CSums/str_Mengolli_Sum_gen.con".
 229
 230 inline "cic:/CoRN/algebra/CSums/Sumx_to_Sum.con".
 231
 232 (* UNEXPORTED
 233 End More_Sums
 234 *)
 235
 236 (* UNEXPORTED
 237 Hint Resolve Sum_one Sum_Sum Sum_first Sum_last Sum_last' Sum_wd
 238   Sum_plus_Sum: algebra.
 239 *)
 240
 241 (* UNEXPORTED
 242 Hint Resolve Sum_minus_Sum inv_Sum inv_Sum0: algebra.
 243 *)
 244