| Age | Commit message (Collapse) | Author |
|---|
|
- Fix implicits of `eq_map_mx`, `eq_in_map_mx`, `map_mx_id_in` and `map_mx_id`,
in order to give more practical arguments first.
- Generalized `map_mx_id` to take the shape f =1 id -> M ^ f = M.
The previous behaviour can be recovered through `map_mx_id (frefl id)` or `[_ ^ id]map_mx_id`
|
|
Injectivity for additive functions and mulmxr.
|
|
Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
|
|
|
|
- `x <= y ?< if c` (lersif) has been replaced with `x < y ?<= if c'` (lteif)
where `c'` is negation of `c`. This change makes statements of several lemmas
(e.g., `lteif_orb`) easily comprehensible.
- The first constructor `BOpen_if` of `itv_bound` has been replaced with
`BClose_if` where the first argument is inverted. Now `pred_of_itv` is defined
by using `lteif` instead of `lersif`.
- Intervals of `T : porderType` form a `porderType` where the ordering relation
is the subset relation. If `T` is a `latticeType`, intervals also form a
`latticeType` where the join and meet are intersection and convex hull
respectively. They are distributive if `T` is an `orderType`.
|
|
Putting `ord1` in `fintype.v`
|
|
|
|
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).
|
|
|
|
|
|
Polynomial evaluation and minimal/char poly of a diagonal/triangular matrices
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Adding mxOver predicate
|
|
+ eq_liftF and lift_eqF
+ proof simplificaions
|
|
into CohenCyril-missing_mxalgebra
|
|
|
|
|
|
Expliciting relation between split and [lr]shift
|
|
More pinvmx theory
|
|
Adding commr_horner lemma
|
|
|
|
|
|
|
|
|
|
+ shortening some proofs
|
|
|
|
Overlay for coq/coq#12756, which changes the default argument name to
just `S` from `S0`. This change preserves the old name; switching instead
to use `S` may be preferable but introduces a potential impact on
downstream users of mathcomp.
|
|
- In the definition of structures in order.v, displays are removed from
parameters of mixins and fields of classes internally and now only appear in
parameters of structures. Consequently, each mixin is now parameterized by a
class rather than a structure, and the corresponding factory parameterized by
a structure is provided to replace the use of the mixin. These factories have
the same names as in the mixins before this change except that `bLatticeMixin`
and `tbLatticeMixin` have been renamed to `bottomMixin` and `topMixin`
respectively.
- Added a factory `distrLatticePOrderMixin` in order.v to build a
`distrLatticeType` from a `porderType`.
|
|
|
|
|
|
|
|
- deprecating `fintype.arg_(min|max)P`
- removing dangling comments connecting min max and meet join
- better compatibility module
- removing broken notations with `\min` and `\max` (no neutral available)
- fixing `incompare` and `incomparel` in order.v
- adding missing elimination lemmas (`(comparable_)?(max|min)E[lg][et]`)
- adding missing `(comparable|real)_arg(min|max)P`
- CHANGELOG update
|
|
- mostly gathered the changes from previous commits
- add `minrC`
- minor doc addition to `order.v`
|
|
- min and max can now be used in a partial order (sometimes under preconditions)
- min and max can now be used in a numDomainType (sometimes under preconditions)
|
|
|
|
|
|
|
|
|
|
|
|
mathcomp-analysis project
|
|
switching long suffixes to short suffixes
|
|
Remove hint declarations using non-global definitions.
|
|
+ `odd_add` -> `oddD`
+ `odd_sub` -> `oddB`
+ `take_addn` -> `takeD`
+ `rot_addn` -> `rotD`
+ `nseq_addn` -> `nseqD`
fixes #359
|
|
Documentation typos
|
|
|
