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

drwxr-xr-x		..
-rw-r--r--	10107	binomial.ma	blob \| history \| raw
-rw-r--r--	56456	chebyshev.ma	blob \| history \| raw
-rw-r--r--	44803	chebyshev_thm.ma	blob \| history \| raw
-rw-r--r--	7425	chinese_reminder.ma	blob \| history \| raw
-rw-r--r--	7966	compare.ma	blob \| history \| raw
-rw-r--r--	5980	congruence.ma	blob \| history \| raw
-rw-r--r--	7801	count.ma	blob \| history \| raw
-rw-r--r--	10676	div_and_mod.ma	blob \| history \| raw
-rw-r--r--	8454	div_and_mod_diseq.ma	blob \| history \| raw
-rw-r--r--	10040	div_and_mod_new.ma.dontcompile	blob \| history \| raw
-rw-r--r--	12116	euler_theorem.ma	blob \| history \| raw
-rw-r--r--	6290	exp.ma	blob \| history \| raw
-rw-r--r--	2376	factorial.ma	blob \| history \| raw
-rw-r--r--	9338	factorial2.ma	blob \| history \| raw
-rw-r--r--	22530	factorization.ma	blob \| history \| raw
-rw-r--r--	8183	fermat_little_theorem.ma	blob \| history \| raw
-rw-r--r--	25106	gcd.ma	blob \| history \| raw
-rw-r--r--	8703	gcd_properties1.ma	blob \| history \| raw
-rw-r--r--	49921	generic_iter_p.ma	blob \| history \| raw
-rw-r--r--	28241	iteration2.ma	blob \| history \| raw
-rw-r--r--	4403	le_arith.ma	blob \| history \| raw
-rw-r--r--	11497	log.ma	blob \| history \| raw
-rw-r--r--	14455	lt_arith.ma	blob \| history \| raw
-rw-r--r--	25402	map_iter_p.ma	blob \| history \| raw
-rw-r--r--	11025	minimization.ma	blob \| history \| raw
-rw-r--r--	11146	minus.ma	blob \| history \| raw
-rw-r--r--	3144	nat.ma	blob \| history \| raw
-rw-r--r--	53776	neper.ma	blob \| history \| raw
-rw-r--r--	6235	nth_prime.ma	blob \| history \| raw
-rw-r--r--	16525	ord.ma	blob \| history \| raw
-rw-r--r--	11690	orders.ma	blob \| history \| raw
-rw-r--r--	23905	permutation.ma	blob \| history \| raw
-rw-r--r--	10380	pi_p.ma	blob \| history \| raw
-rw-r--r--	2494	plus.ma	blob \| history \| raw
-rw-r--r--	21982	primes.ma	blob \| history \| raw
-rw-r--r--	2110	relevant_equations.ma	blob \| history \| raw
-rw-r--r--	2800	sigma_and_pi.ma	blob \| history \| raw
-rw-r--r--	6680	sqrt.ma	blob \| history \| raw
-rw-r--r--	3102	times.ma	blob \| history \| raw
-rw-r--r--	5092	totient.ma	blob \| history \| raw
-rw-r--r--	8142	totient1.ma	blob \| history \| raw