| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Describe extension and warn about incompatibilities.
|
|
|
|
|
|
itv_intersection, redefine prev_of_itv and itv_decompose using lersif, extend itv_rewrite, simplify proofs (#271)
|
|
* Add some theorems on lersif and intervals
* Add more theorems on lersif
* Remove needless parens
* ChangeLog
* Move lersifN
* Add lersif_anti
|
|
|
|
Refactored and completed implicit and scope signatures of constants of
MatrixGenField, the module that contains the construction of an
extension field for an irreducible representation, and for decidability
definitions.
Completed and corrected some errors in the corresponding header
documentation.
|
|
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.
|
|
|
|
|
|
This reverts commit 044634dcc2f645e3afbdad6cb8dcc66f3eb4a87e.
See issue https://github.com/math-comp/odd-order/pull/5
|
|
Statement of `bool_irrelevance` more consistent with its name.
|
|
|
|
- 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
|
|
they are already defined in ssrfun
ChangeLog updated
|
|
|
|
Tool to prove only P0 -> P1 -> ... -> Pn -> P0
but use any implication Pi -> Pj
|
|
|
|
thanks Yves
|
|
|
|
|
|
|
|
One paragraph per version + spell check
|
|
|
