coq-mathcomp - Library of mathematical components formalized in Coq

Age	Commit message (Collapse)	Author
2018-04-17	move odd_order to its own repository	Enrico Tassi

2018-03-04	Change deprecated Arguments Scope to Arguments	Jasper Hugunin

2018-02-22	Change Implicit Arguments to Arguments in odd_order	Jasper Hugunin

2018-02-06	running semi-automated linting on the whole library	Cyril Cohen

2016-11-07	update copyright banner	Assia Mahboubi

2016-08-25	Enriched numClosedFieldType so that it factors a lot of theory from both ↵	Cyril Cohen
	complex and algC. The definitions of 'i, conjC, Re, Im, n.-root, sqrtC and their theory have been moved to the numClosedFieldType structure in ssrnum. This covers boths the uses in algC and complex.v. To that end the numClosedFieldType structure has been enriched with conjugation and 'i. Note that 'i can be deduced from the property of algebraic closure and is only here to let the user chose which definitional equality should hold on 'i. Same thing for conjC that could be written `\|x\|^+2/x, the only nontrivial (up to my knowledge) property is the fact that conjugation is a ring morphism.
2015-07-28	update copyright banner	Enrico Tassi

2015-07-17	Updating files + reorganizing everything	Cyril Cohen

2015-03-09	Initial commit	Enrico Tassi