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

drwxr-xr-x		..
-rw-r--r--	33428	bertrand.ma	blob \| history \| raw
-rw-r--r--	10804	binomial.ma	blob \| history \| raw
-rw-r--r--	62430	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--	7924	compare.ma	blob \| history \| raw
-rw-r--r--	5935	congruence.ma	blob \| history \| raw
-rw-r--r--	7736	count.ma	blob \| history \| raw
-rw-r--r--	10629	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--	12068	euler_theorem.ma	blob \| history \| raw
-rw-r--r--	6562	exp.ma	blob \| history \| raw
-rw-r--r--	2332	factorial.ma	blob \| history \| raw
-rw-r--r--	9148	factorial2.ma	blob \| history \| raw
-rw-r--r--	22927	factorization.ma	blob \| history \| raw
-rw-r--r--	8127	fermat_little_theorem.ma	blob \| history \| raw
-rw-r--r--	25790	gcd.ma	blob \| history \| raw
-rw-r--r--	8703	gcd_properties1.ma	blob \| history \| raw
-rw-r--r--	49988	generic_iter_p.ma	blob \| history \| raw
-rw-r--r--	28195	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--	25335	map_iter_p.ma	blob \| history \| raw
-rw-r--r--	10978	minimization.ma	blob \| history \| raw
-rw-r--r--	11106	minus.ma	blob \| history \| raw
-rw-r--r--	3106	nat.ma	blob \| history \| raw
-rw-r--r--	53956	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--	16487	ord.ma	blob \| history \| raw
-rw-r--r--	11649	orders.ma	blob \| history \| raw
-rw-r--r--	23859	permutation.ma	blob \| history \| raw
-rw-r--r--	10918	pi_p.ma	blob \| history \| raw
-rw-r--r--	2455	plus.ma	blob \| history \| raw
-rw-r--r--	21941	primes.ma	blob \| history \| raw
-rw-r--r--	2057	relevant_equations.ma	blob \| history \| raw
-rw-r--r--	15405	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--	3489	times.ma	blob \| history \| raw
-rw-r--r--	5050	totient.ma	blob \| history \| raw
-rw-r--r--	8099	totient1.ma	blob \| history \| raw