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

Mode	Name	Size
-rw-r--r--	BGappendixAB.v	24185	log plain
-rw-r--r--	BGappendixC.v	38856	log plain
-rw-r--r--	BGsection1.v	64198	log plain
-rw-r--r--	BGsection10.v	74424	log plain
-rw-r--r--	BGsection11.v	22086	log plain
-rw-r--r--	BGsection12.v	144925	log plain
-rw-r--r--	BGsection13.v	63114	log plain
-rw-r--r--	BGsection14.v	136652	log plain
-rw-r--r--	BGsection15.v	84217	log plain
-rw-r--r--	BGsection16.v	66643	log plain
-rw-r--r--	BGsection2.v	60600	log plain
-rw-r--r--	BGsection3.v	100079	log plain
-rw-r--r--	BGsection4.v	77865	log plain
-rw-r--r--	BGsection5.v	27787	log plain
-rw-r--r--	BGsection6.v	14510	log plain
-rw-r--r--	BGsection7.v	46473	log plain
-rw-r--r--	BGsection8.v	21463	log plain
-rw-r--r--	BGsection9.v	24728	log plain
-rw-r--r--	PFsection1.v	37598	log plain
-rw-r--r--	PFsection10.v	64935	log plain
-rw-r--r--	PFsection11.v	65494	log plain
-rw-r--r--	PFsection12.v	72532	log plain
-rw-r--r--	PFsection13.v	114822	log plain
-rw-r--r--	PFsection14.v	64805	log plain
-rw-r--r--	PFsection2.v	37386	log plain
-rw-r--r--	PFsection3.v	89360	log plain
-rw-r--r--	PFsection4.v	48587	log plain
-rw-r--r--	PFsection5.v	79351	log plain
-rw-r--r--	PFsection6.v	93709	log plain
-rw-r--r--	PFsection7.v	42802	log plain
-rw-r--r--	PFsection8.v	54296	log plain
-rw-r--r--	PFsection9.v	128294	log plain
-rw-r--r--	all.v	922	log plain
-rw-r--r--	stripped_odd_order_theorem.v	9109	log plain
-rw-r--r--	wielandt_fixpoint.v	37611	log plain