diff options
| author | Cyril Cohen | 2020-11-25 10:34:24 +0100 |
|---|---|---|
| committer | GitHub | 2020-11-25 10:34:24 +0100 |
| commit | a32027b47948045c24b63645546371544a839609 (patch) | |
| tree | 7976c57a094667eb98c6ac89e6be83d63f407e4b /mathcomp/algebra/matrix.v | |
| parent | 7189708809e3c79effe40a2c9ecf693f66423cd3 (diff) | |
| parent | ac30dae7377f9762ceba1c5553f0542831a0bb5c (diff) | |
Merge pull request #601 from pi8027/sorting_in
Add `_in` variants of the sorting lemmas
Diffstat (limited to 'mathcomp/algebra/matrix.v')
0 files changed, 0 insertions, 0 deletions