]> matita.cs.unibo.it Git - helm.git/tree - matita/library/nat/
tagged 0.5.0-rc1 0.5.0-rc1
[helm.git] / matita / library / nat /
drwxr-xr-x   ..
-rw-r--r-- 48203 bertrand.ma
-rw-r--r-- 10804 binomial.ma
-rw-r--r-- 62430 chebyshev.ma
-rw-r--r-- 14966 chebyshev_teta.ma
-rw-r--r-- 44268 chebyshev_thm.ma
-rw-r--r-- 7374 chinese_reminder.ma
-rw-r--r-- 7924 compare.ma
-rw-r--r-- 5935 congruence.ma
-rw-r--r-- 7736 count.ma
-rw-r--r-- 10629 div_and_mod.ma
-rw-r--r-- 8402 div_and_mod_diseq.ma
-rw-r--r-- 10040 div_and_mod_new.ma.dontcompile
-rw-r--r-- 12068 euler_theorem.ma
-rw-r--r-- 6562 exp.ma
-rw-r--r-- 2332 factorial.ma
-rw-r--r-- 9148 factorial2.ma
-rw-r--r-- 22482 factorization.ma
-rw-r--r-- 8127 fermat_little_theorem.ma
-rw-r--r-- 25790 gcd.ma
-rw-r--r-- 8703 gcd_properties1.ma
-rw-r--r-- 49988 generic_iter_p.ma
-rw-r--r-- 28195 iteration2.ma
-rw-r--r-- 4360 le_arith.ma
-rw-r--r-- 11459 log.ma
-rw-r--r-- 14412 lt_arith.ma
-rw-r--r-- 25335 map_iter_p.ma
-rw-r--r-- 10978 minimization.ma
-rw-r--r-- 11106 minus.ma
-rw-r--r-- 3188 nat.ma
-rw-r--r-- 53956 neper.ma
-rw-r--r-- 6191 nth_prime.ma
-rw-r--r-- 6829 o.ma
-rw-r--r-- 16487 ord.ma
-rw-r--r-- 11649 orders.ma
-rw-r--r-- 23859 permutation.ma
-rw-r--r-- 10918 pi_p.ma
-rw-r--r-- 2455 plus.ma
-rw-r--r-- 21941 primes.ma
-rw-r--r-- 2057 relevant_equations.ma
-rw-r--r-- 2753 sigma_and_pi.ma
-rw-r--r-- 6920 sqrt.ma
-rw-r--r-- 3489 times.ma
-rw-r--r-- 5050 totient.ma
-rw-r--r-- 8099 totient1.ma