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	24183	log plain
-rw-r--r--	BGappendixC.v	38992	log plain
-rw-r--r--	BGsection1.v	64022	log plain
-rw-r--r--	BGsection10.v	74100	log plain
-rw-r--r--	BGsection11.v	21990	log plain
-rw-r--r--	BGsection12.v	144569	log plain
-rw-r--r--	BGsection13.v	63185	log plain
-rw-r--r--	BGsection14.v	136672	log plain
-rw-r--r--	BGsection15.v	83889	log plain
-rw-r--r--	BGsection16.v	66761	log plain
-rw-r--r--	BGsection2.v	60640	log plain
-rw-r--r--	BGsection3.v	99782	log plain
-rw-r--r--	BGsection4.v	77429	log plain
-rw-r--r--	BGsection5.v	27660	log plain
-rw-r--r--	BGsection6.v	14578	log plain
-rw-r--r--	BGsection7.v	46058	log plain
-rw-r--r--	BGsection8.v	20785	log plain
-rw-r--r--	BGsection9.v	24691	log plain
l---------	CeCILL-B	18	log plain
l---------	INSTALL	17	log plain
-rw-r--r--	Make	505	log plain
-rw-r--r--	Makefile	892	log plain
-rw-r--r--	PFsection1.v	35796	log plain
-rw-r--r--	PFsection10.v	65314	log plain
-rw-r--r--	PFsection11.v	65515	log plain
-rw-r--r--	PFsection12.v	72176	log plain
-rw-r--r--	PFsection13.v	115055	log plain
-rw-r--r--	PFsection14.v	64946	log plain
-rw-r--r--	PFsection2.v	37504	log plain
-rw-r--r--	PFsection3.v	89507	log plain
-rw-r--r--	PFsection4.v	48726	log plain
-rw-r--r--	PFsection5.v	79720	log plain
-rw-r--r--	PFsection6.v	79110	log plain
-rw-r--r--	PFsection7.v	42921	log plain
-rw-r--r--	PFsection8.v	54466	log plain
-rw-r--r--	PFsection9.v	128255	log plain
l---------	README	16	log plain
-rw-r--r--	opam	969	log plain
-rw-r--r--	stripped_odd_order_theorem.v	9109	log plain
-rw-r--r--	wielandt_fixpoint.v	37521	log plain