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.
2015-12-12	switch ":" to "-"	Cyril Cohen

2015-11-10	fix INSTALL symlinks	Enrico Tassi

2015-11-06	basic has disappeared	Cyril Cohen

2015-07-28	update copyright banner	Enrico Tassi

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	Using the From X Require Y for v8.4	Cyril Cohen

2015-04-08	packaging for v8.5	Cyril Cohen

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

2015-03-19	packaging fingroup and algebra	Cyril Cohen
	The files zmodp and cyclic in fingroup had dependecies in algebra so I put them there. I'm not convinced it's the best solution to this problem. Maybe more subdivisions in algebra would bring a better solution? (Maybe we should send the whole problem to a solver? :P)
2015-03-09	Initial commit	Enrico Tassi