From a2d36f6f0746531d207e760a22d47dd2ebb77ade Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Wed, 5 Dec 2018 11:23:46 +0100
Subject: Adding lemma `eqmxMunitP`

---
 ChangeLog | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'ChangeLog')

diff --git a/ChangeLog b/ChangeLog
index e37f1e8..4f17072 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -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
-- 
cgit v1.2.3