diff options
| author | Cyril Cohen | 2018-12-05 11:23:46 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2018-12-10 18:32:20 +0100 |
| commit | a2d36f6f0746531d207e760a22d47dd2ebb77ade (patch) | |
| tree | 33bfd5ebefbde4b3fef0841d6e039d22104201ab /ChangeLog | |
| parent | 67ccc34eb6f05383e0e7bd90c7df9e4fb51f2a87 (diff) | |
Adding lemma `eqmxMunitP`
Diffstat (limited to 'ChangeLog')
| -rw-r--r-- | ChangeLog | 4 |
1 files changed, 4 insertions, 0 deletions
@@ -26,6 +26,10 @@ * Specialized `bool_irrelevance` so that the statement reflects the name + * Added lemma `eqmxMunitP`: two matrices with the same shape + represent the same subspace iff they differ only by a change of + basis. + 24/04/2018 - compatibility with Coq 8.8 and several small fixes - version 1.7 * Added compatibility with Coq 8.8 and lost compatibility with |