matita.cs.unibo.it Git - helm.git/tree - matita/matita/library/nat/

drwxr-xr-x		..
-rw-r--r--	33418	bertrand.ma	blob \| history \| raw
-rw-r--r--	10804	binomial.ma	blob \| history \| raw
-rw-r--r--	63415	chebyshev.ma	blob \| history \| raw
-rw-r--r--	14966	chebyshev_teta.ma	blob \| history \| raw
-rw-r--r--	44268	chebyshev_thm.ma	blob \| history \| raw
-rw-r--r--	7374	chinese_reminder.ma	blob \| history \| raw
-rw-r--r--	8274	compare.ma	blob \| history \| raw
-rw-r--r--	5790	congruence.ma	blob \| history \| raw
-rw-r--r--	7736	count.ma	blob \| history \| raw
-rw-r--r--	10701	div_and_mod.ma	blob \| history \| raw
-rw-r--r--	8402	div_and_mod_diseq.ma	blob \| history \| raw
-rw-r--r--	10040	div_and_mod_new.ma.dontcompile	blob \| history \| raw
-rw-r--r--	12017	euler_theorem.ma	blob \| history \| raw
-rw-r--r--	6538	exp.ma	blob \| history \| raw
-rw-r--r--	2302	factorial.ma	blob \| history \| raw
-rw-r--r--	9092	factorial2.ma	blob \| history \| raw
-rw-r--r--	22591	factorization.ma	blob \| history \| raw
-rw-r--r--	7511	factorization2.ma	blob \| history \| raw
-rw-r--r--	8127	fermat_little_theorem.ma	blob \| history \| raw
-rw-r--r--	25690	gcd.ma	blob \| history \| raw
-rw-r--r--	8653	gcd_properties1.ma	blob \| history \| raw
-rw-r--r--	50088	generic_iter_p.ma	blob \| history \| raw
-rw-r--r--	28161	iteration2.ma	blob \| history \| raw
-rw-r--r--	4360	le_arith.ma	blob \| history \| raw
-rw-r--r--	11459	log.ma	blob \| history \| raw
-rw-r--r--	14412	lt_arith.ma	blob \| history \| raw
-rw-r--r--	25339	map_iter_p.ma	blob \| history \| raw
-rw-r--r--	11240	minimization.ma	blob \| history \| raw
-rw-r--r--	12124	minus.ma	blob \| history \| raw
-rw-r--r--	3246	nat.ma	blob \| history \| raw
-rw-r--r--	53957	neper.ma	blob \| history \| raw
-rw-r--r--	6191	nth_prime.ma	blob \| history \| raw
-rw-r--r--	6829	o.ma	blob \| history \| raw
-rw-r--r--	17799	ord.ma	blob \| history \| raw
-rw-r--r--	11294	orders.ma	blob \| history \| raw
-rw-r--r--	23906	permutation.ma	blob \| history \| raw
-rw-r--r--	11925	pi_p.ma	blob \| history \| raw
-rw-r--r--	2377	plus.ma	blob \| history \| raw
-rw-r--r--	21824	primes.ma	blob \| history \| raw
-rw-r--r--	2057	relevant_equations.ma	blob \| history \| raw
-rw-r--r--	16192	sieve.ma	blob \| history \| raw
-rw-r--r--	2753	sigma_and_pi.ma	blob \| history \| raw
-rw-r--r--	6920	sqrt.ma	blob \| history \| raw
-rw-r--r--	3830	times.ma	blob \| history \| raw
-rw-r--r--	5050	totient.ma	blob \| history \| raw
-rw-r--r--	8071	totient1.ma	blob \| history \| raw