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	24269	log plain
-rw-r--r--	BGappendixC.v	39071	log plain
-rw-r--r--	BGsection1.v	64108	log plain
-rw-r--r--	BGsection10.v	74186	log plain
-rw-r--r--	BGsection11.v	22076	log plain
-rw-r--r--	BGsection12.v	144655	log plain
-rw-r--r--	BGsection13.v	63271	log plain
-rw-r--r--	BGsection14.v	136758	log plain
-rw-r--r--	BGsection15.v	83973	log plain
-rw-r--r--	BGsection16.v	66845	log plain
-rw-r--r--	BGsection2.v	60740	log plain
-rw-r--r--	BGsection3.v	99868	log plain
-rw-r--r--	BGsection4.v	77515	log plain
-rw-r--r--	BGsection5.v	27746	log plain
-rw-r--r--	BGsection6.v	14664	log plain
-rw-r--r--	BGsection7.v	46144	log plain
-rw-r--r--	BGsection8.v	20871	log plain
-rw-r--r--	BGsection9.v	24777	log plain
l---------	CeCILL-B	18	log plain
l---------	INSTALL	20	log plain
-rw-r--r--	Make	505	log plain
-rw-r--r--	Makefile	892	log plain
-rw-r--r--	PFsection1.v	35896	log plain
-rw-r--r--	PFsection10.v	65400	log plain
-rw-r--r--	PFsection11.v	65601	log plain
-rw-r--r--	PFsection12.v	72262	log plain
-rw-r--r--	PFsection13.v	115141	log plain
-rw-r--r--	PFsection14.v	65032	log plain
-rw-r--r--	PFsection2.v	37590	log plain
-rw-r--r--	PFsection3.v	89593	log plain
-rw-r--r--	PFsection4.v	48812	log plain
-rw-r--r--	PFsection5.v	79806	log plain
-rw-r--r--	PFsection6.v	79196	log plain
-rw-r--r--	PFsection7.v	43007	log plain
-rw-r--r--	PFsection8.v	54566	log plain
-rw-r--r--	PFsection9.v	128341	log plain
l---------	README	16	log plain
-rw-r--r--	descr	223	log plain
-rw-r--r--	opam	905	log plain
-rw-r--r--	stripped_odd_order_theorem.v	9257	log plain
-rw-r--r--	wielandt_fixpoint.v	37607	log plain