Ported permutation.ma and fermat_little_theorem.ma

[helm.git] / matita / matita / lib / arithmetics / sigma_pi.ma

diff --git a/matita/matita/lib/arithmetics/sigma_pi.ma b/matita/matita/lib/arithmetics/sigma_pi.ma
index 7e3fe19f04df5f44b586f815b8afeaa74312a24a..8d2a5858ab2d842302cc873c1756c3008ce9d5cc 100644 (file)
--- a/matita/matita/lib/arithmetics/sigma_pi.ma
+++ b/matita/matita/lib/arithmetics/sigma_pi.ma
@@ -186,3 +186,14 @@ theorem exp_sigma_l: ∀n,a,p,f.
   |>bigop_Sfalse [>bigop_Sfalse [@Hind|//] | //]
   ]
 qed.
+
+theorem exp_pi_l: ∀n,a,f. 
+  exp a n*(∏_{i < n}(f i)) = ∏_{i < n} (a*(f i)).
+#n #a #f elim n // #i #Hind >bigop_Strue // >bigop_Strue //
+<Hind <associative_times <associative_times @eq_f2 // normalize // 
+qed.
+
+theorem exp_pi_bc: ∀a,b,c,f. 
+  exp a (c-b)*(∏_{i ∈ [b,c[ }(f i)) = ∏_{i ∈ [b,c[ } (a*(f i)).
+#a #b #c #f @exp_pi_l 
+qed.
\ No newline at end of file