coq-mathcomp - Library of mathematical components formalized in Coq

Age	Commit message (Collapse)	Author
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.
2016-05-12	Fixes doc of mxrepresentation.v	Florent Hivert

2015-12-12	switch ":" to "-"	Cyril Cohen

2015-12-04	Move finfield to field module	Georges Gonthier

2015-12-04	Add elementary abelian finite modules lemmas to abelian	Georges Gonthier
	This factors proofs in mxabelem and finfield and removes dependencies between these two files.
2015-11-10	fix INSTALL symlinks	Enrico Tassi

2015-07-28	update copyright banner	Enrico Tassi

2015-07-22	Add a From ...	Cyril Cohen

2015-07-22	remove duplicate fields	Cyril Cohen

2015-07-22	make the opam package meta data	Cyril Cohen

2015-07-21	update opam meta-data	Cyril Cohen

2015-07-18	update to preserve backward compatibility with v8.4	Cyril Cohen

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

2015-04-09	character for v8.5	Cyril Cohen

2015-04-09	Using the From X Require Y for v8.4	Cyril Cohen

2015-04-08	makefiles that are version dependent	Cyril Cohen

2015-03-30	character packaged	Cyril Cohen

2015-03-25	packaging real_closed	Cyril Cohen

2015-03-24	change finfield from field to character	Cyril Cohen

2015-03-09	Initial commit	Enrico Tassi