coq-mathcomp - Library of mathematical components formalized in Coq

Age	Commit message (Collapse)	Author
2018-07-14	Laurent's simplifications	Cyril Cohen

2018-07-04	small generalizations in poly	Cyril Cohen

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

2018-02-21	Change Implicit Arguments to Arguments in algebra	Jasper Hugunin

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

2017-12-14	Using x * y = 1 and x / y = 1 to derive the inverse	Cyril Cohen
	fixes #169
2017-11-27	following @ggonthier remark.	Cyril Cohen

2017-11-23	Add addrKA and subrKA (addrK and addrNK modulo Associativity)	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-12-04	Remove more redundant power type structures	Georges Gonthier

2015-12-04	Add missing export	Georges Gonthier

2015-07-28	update copyright banner	Enrico Tassi

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-03-09	Initial commit	Enrico Tassi