X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCSums.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCSums.ma;h=0177138c73ca71f48d8378048b4fa3e102f01ed3;hb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;hp=0000000000000000000000000000000000000000;hpb=438a29376390222b94c1fe9772917c3aad50d42e;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma new file mode 100644 index 000000000..0177138c7 --- /dev/null +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CSums.ma @@ -0,0 +1,248 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +set "baseuri" "cic:/matita/CoRN-Decl/algebra/CSums". + +(* $Id: CSums.v,v 1.8 2004/04/23 10:00:54 lcf Exp $ *) + +(*#* printing Sum0 %\ensuremath{\sum_0}% #∑0# *) + +(*#* printing Sum1 %\ensuremath{\sum_1}% #∑1# *) + +(*#* printing Sum2 %\ensuremath{\sum_2}% #∑2# *) + +(*#* printing Sum %\ensuremath{\sum}% #∑# *) + +(*#* printing Sumx %\ensuremath{\sum'}% #∑'&*) + +(* INCLUDE +CAbGroups +*) + +(* INCLUDE +Peano_dec +*) + +(*#* * Sums + +%\begin{convention}% Let [G] be an abelian group. +%\end{convention}% +*) + +(* UNEXPORTED +Section Sums. +*) + +inline cic:/CoRN/algebra/CSums/G.var. + +(* Sum1 and Sum use subtraction *) + +inline cic:/CoRN/algebra/CSums/Sumlist.con. + +inline cic:/CoRN/algebra/CSums/Sumx.con. + +(*#* +It is sometimes useful to view a function defined on $\{0,\ldots,i-1\}$ +#{0, ... i-1}# as a function on the natural numbers which evaluates to +[Zero] when the input is greater than or equal to [i]. +*) + +inline cic:/CoRN/algebra/CSums/part_tot_nat_fun.con. + +inline cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch1.con. + +inline cic:/CoRN/algebra/CSums/part_tot_nat_fun_ch2.con. + +(*#* [Sum0] defines the sum for [i=0..(n-1)] *) + +inline cic:/CoRN/algebra/CSums/Sum0.con. + +(*#* [Sum1] defines the sum for [i=m..(n-1)] *) + +inline cic:/CoRN/algebra/CSums/Sum1.con. + +inline cic:/CoRN/algebra/CSums/Sum.con. + +(* Sum i=m..n *) + +(*#* [Sum2] is similar to [Sum1], but does not require the summand to be +defined outside where it is being added. *) + +inline cic:/CoRN/algebra/CSums/Sum2.con. + +inline cic:/CoRN/algebra/CSums/Sum_one.con. + +(* UNEXPORTED +Hint Resolve Sum_one: algebra. +*) + +inline cic:/CoRN/algebra/CSums/Sum_empty.con. + +(* UNEXPORTED +Hint Resolve Sum_empty: algebra. +*) + +inline cic:/CoRN/algebra/CSums/Sum_Sum.con. + +(* UNEXPORTED +Hint Resolve Sum_Sum: algebra. +*) + +inline cic:/CoRN/algebra/CSums/Sum_first.con. + +inline cic:/CoRN/algebra/CSums/Sum_last.con. + +(* UNEXPORTED +Hint Resolve Sum_last: algebra. +*) + +inline cic:/CoRN/algebra/CSums/Sum_last'.con. + +(*#* +We add some extensionality results which will be quite useful +when working with integration. +*) + +inline cic:/CoRN/algebra/CSums/Sum0_strext.con. + +inline cic:/CoRN/algebra/CSums/Sum_strext.con. + +inline cic:/CoRN/algebra/CSums/Sumx_strext.con. + +inline cic:/CoRN/algebra/CSums/Sum0_strext'.con. + +inline cic:/CoRN/algebra/CSums/Sum_strext'.con. + +inline cic:/CoRN/algebra/CSums/Sum0_wd.con. + +inline cic:/CoRN/algebra/CSums/Sum_wd.con. + +inline cic:/CoRN/algebra/CSums/Sumx_wd.con. + +inline cic:/CoRN/algebra/CSums/Sum_wd'.con. + +inline cic:/CoRN/algebra/CSums/Sum2_wd.con. + +inline cic:/CoRN/algebra/CSums/Sum0_plus_Sum0.con. + +(* UNEXPORTED +Hint Resolve Sum0_plus_Sum0: algebra. +*) + +inline cic:/CoRN/algebra/CSums/Sum_plus_Sum.con. + +inline cic:/CoRN/algebra/CSums/Sumx_plus_Sumx.con. + +inline cic:/CoRN/algebra/CSums/Sum2_plus_Sum2.con. + +inline cic:/CoRN/algebra/CSums/inv_Sum0.con. + +(* UNEXPORTED +Hint Resolve inv_Sum0: algebra. +*) + +inline cic:/CoRN/algebra/CSums/inv_Sum.con. + +(* UNEXPORTED +Hint Resolve inv_Sum: algebra. +*) + +inline cic:/CoRN/algebra/CSums/inv_Sumx.con. + +inline cic:/CoRN/algebra/CSums/inv_Sum2.con. + +inline cic:/CoRN/algebra/CSums/Sum_minus_Sum.con. + +(* UNEXPORTED +Hint Resolve Sum_minus_Sum: algebra. +*) + +inline cic:/CoRN/algebra/CSums/Sumx_minus_Sumx.con. + +inline cic:/CoRN/algebra/CSums/Sum2_minus_Sum2.con. + +inline cic:/CoRN/algebra/CSums/Sum_apzero.con. + +inline cic:/CoRN/algebra/CSums/Sum_zero.con. + +inline cic:/CoRN/algebra/CSums/Sum_term.con. + +inline cic:/CoRN/algebra/CSums/Sum0_shift.con. + +(* UNEXPORTED +Hint Resolve Sum0_shift: algebra. +*) + +inline cic:/CoRN/algebra/CSums/Sum_shift.con. + +inline cic:/CoRN/algebra/CSums/Sum_big_shift.con. + +inline cic:/CoRN/algebra/CSums/Sumx_Sum0.con. + +(* UNEXPORTED +End Sums. +*) + +(* UNEXPORTED +Implicit Arguments Sum [G]. +*) + +(* UNEXPORTED +Implicit Arguments Sum0 [G]. +*) + +(* UNEXPORTED +Implicit Arguments Sumx [G n]. +*) + +(* UNEXPORTED +Implicit Arguments Sum2 [G m n]. +*) + +(*#* +The next results are useful for calculating some special sums, +often referred to as ``Mengolli Sums''. +%\begin{convention}% Let [G] be an abelian group. +%\end{convention}% +*) + +(* UNEXPORTED +Section More_Sums. +*) + +inline cic:/CoRN/algebra/CSums/G.var. + +inline cic:/CoRN/algebra/CSums/Mengolli_Sum.con. + +inline cic:/CoRN/algebra/CSums/Mengolli_Sum_gen.con. + +inline cic:/CoRN/algebra/CSums/str_Mengolli_Sum_gen.con. + +inline cic:/CoRN/algebra/CSums/Sumx_to_Sum.con. + +(* UNEXPORTED +End More_Sums. +*) + +(* UNEXPORTED +Hint Resolve Sum_one Sum_Sum Sum_first Sum_last Sum_last' Sum_wd + Sum_plus_Sum: algebra. +*) + +(* UNEXPORTED +Hint Resolve Sum_minus_Sum inv_Sum inv_Sum0: algebra. +*) +