coq-mathcomp - Library of mathematical components formalized in Coq

Age	Commit message (Collapse)	Author
2020-10-29	Switch from long suffixes to short suffixes	Kazuhiko Sakaguchi

2020-09-27	Putting ord1 in fintype	Cyril Cohen
	ord1 is in zmodp, but it does not really require the zmodType structure of 'I_n to be stated and proven if we state it with ord0. We still keep the variant in zmodp with 0 instead of ord0 (for readability purposes).
2019-11-14	Update zmodp.v (#411)	Gabriel Taumaturgo

2019-04-26	Cleaning Require and Require Imports	Cyril Cohen

2018-12-13	Adjust implicits of cancellation lemmas	Georges Gonthier
	Like injectivity lemmas, instances of cancellation lemmas (whose conclusion is `cancel ? ?`, `{in ?, cancel ? ?}`, `pcancel`, or `ocancel`) are passed to generic lemmas such as `canRL` or `canLR_in`. Thus such lemmas should not have trailing on-demand implicits _just before_ the `cancel` conclusion, as these would be inconvenient to insert (requiring essentially an explicit eta-expansion). We therefore use `Arguments` or `Prenex Implicits` directives to make all such arguments maximally inserted implicits. We don’t, however make other arguments implicit, so as not to spoil direct instantiation of the lemmas (in, e.g., `rewrite -[y](invmK injf)`). We have also tried to do this with lemmas whose statement matches a `cancel`, i.e., ending in `forall x, g (E[x]) = x` (where pattern unification will pick up `f = fun x => E[x]`). We also adjusted implicits of a few stray injectivity lemmas, and defined constants. We provide a shorthand for reindexing a bigop with a permutation. Finally we used the new implicit signatures to simplify proofs that use injectivity or cancellation lemmas.
2018-10-26	moving countalg and closed_field around	Cyril Cohen
	- countalg goes to the algebra package - finalg now get the expected inheritance from countalg - closed_field now contains the construction of algebraic closure for countable fields (previously in countalg) - proof of quantifier elimination for closed field rewritten in a monadic style
2018-02-21	Change Implicit Arguments to Arguments in algebra	Jasper Hugunin

2016-11-07	update copyright banner	Assia Mahboubi

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-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)