odd_order « mathcomp - coq-mathcomp - Library of mathematical components formalized in Coq

Mode	Name	Size
l---------	AUTHORS	17	log plain
-rw-r--r--	BGappendixAB.v	24265	log plain
-rw-r--r--	BGappendixC.v	39087	log plain
-rw-r--r--	BGsection1.v	64108	log plain
-rw-r--r--	BGsection10.v	74167	log plain
-rw-r--r--	BGsection11.v	22074	log plain
-rw-r--r--	BGsection12.v	144572	log plain
-rw-r--r--	BGsection13.v	63261	log plain
-rw-r--r--	BGsection14.v	136736	log plain
-rw-r--r--	BGsection15.v	83960	log plain
-rw-r--r--	BGsection16.v	66838	log plain
-rw-r--r--	BGsection2.v	60735	log plain
-rw-r--r--	BGsection3.v	99865	log plain
-rw-r--r--	BGsection4.v	77494	log plain
-rw-r--r--	BGsection5.v	27736	log plain
-rw-r--r--	BGsection6.v	14659	log plain
-rw-r--r--	BGsection7.v	46124	log plain
-rw-r--r--	BGsection8.v	20869	log plain
-rw-r--r--	BGsection9.v	24775	log plain
l---------	CeCILL-B	18	log plain
l---------	INSTALL	20	log plain
-rw-r--r--	Make	505	log plain
-rw-r--r--	Makefile	485	log plain
-rw-r--r--	PFsection1.v	35891	log plain
-rw-r--r--	PFsection10.v	65396	log plain
-rw-r--r--	PFsection11.v	65597	log plain
-rw-r--r--	PFsection12.v	72250	log plain
-rw-r--r--	PFsection13.v	115128	log plain
-rw-r--r--	PFsection14.v	65021	log plain
-rw-r--r--	PFsection2.v	37580	log plain
-rw-r--r--	PFsection3.v	89500	log plain
-rw-r--r--	PFsection4.v	48802	log plain
-rw-r--r--	PFsection5.v	79770	log plain
-rw-r--r--	PFsection6.v	79197	log plain
-rw-r--r--	PFsection7.v	43005	log plain
-rw-r--r--	PFsection8.v	54564	log plain
-rw-r--r--	PFsection9.v	128330	log plain
l---------	README	16	log plain
-rw-r--r--	descr	223	log plain
-rw-r--r--	opam	912	log plain
-rw-r--r--	stripped_odd_order_theorem.v	9257	log plain
-rw-r--r--	wielandt_fixpoint.v	37606	log plain