math-comp
math-comp copied to clipboard
math-comp
Mathematical Components
This Pull Request is about porting the hierarchy of hand declared algebraic structures to the language of [hierarchy-builder](https://github.com/math-comp/hierarchy-builder) . Rules for contributing to this PR: - Tick the boxes down...
##### Motivation for this change Those simple lemmas should be useful. Fixes #886 ##### Things done/to do - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` (do not edit former entries) ~-...
##### Motivation for this change https://github.com/coq/coq/pull/16361
##### Motivation for this change Many lemmas for bigops on monoids (particularly abelian ones) were already valid on (abelian) semigroups. This generalization could be improved by adding semigroups to the...
##### Motivation for this change More generic theorem `take_take` ##### Things done/to do - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` (do not edit former entries) ##### Automatic note to reviewers...
This is a continuation of #425. The wish is to automate the verification that all new lemmas, canonical structures, and Export modules are duly exported by the GRing.Theory module, module...
**For mathcomp 1.14.0**, remove `big_uncond` (i.e. the deprecation warning set for 1.13.0 in #589, cf #492) Also remove other 1.13.0 deprecations
Add `[in A]` notation for `fun x => x \in A`, the natural applicative equivalent of a collective predicate `A`. Replace `(mem A)` and `[mem A]`, which had a similar...
This allows syntax such as ```coq Check [seq '(x, y) x + y) (zip (iota 0 5) (iota 0 5)). ``` prints as the ugly ```coq [seq (let '(x, y)...
The subspaces `{vspace vT}` of a vector space `vT` (defined in `vector.v`) seem to form a lattice. [A Wikipedia article](https://en.wikipedia.org/wiki/Linear_subspace) says that "the operations intersection and sum make the set...