update ChangeLog and doc

2 files changed, 9 insertions, 4 deletions

diff --git a/ChangeLog b/ChangeLog
index 13045e9..d59a140 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,7 @@
+??/??/???? - version 1.7.1
+	* Added companion matrix of a polynomial `companionmx p` and the
+	  theorems: companionmxK, map_mx_companion and companion_map_poly
+
 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
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
index 9676af2..87c7fbd 100644
--- a/mathcomp/algebra/mxpoly.v
+++ b/mathcomp/algebra/mxpoly.v
@@ -26,10 +26,11 @@ Require Import poly polydiv.
 (* powers_mx A d == the d x (n ^ 2) matrix whose rows are the mxvec encodings *)
 (*                  of the first d powers of A (n of the form n'.+1). Thus,   *)
 (*                  vec_mx (v *m powers_mx A d) = horner_mx A (rVpoly v).     *)
-(*   char_poly A == the characteristic polynomial of A.                       *)
-(* char_poly_mx A == a matrix whose detereminant is char_poly A.              *)
-(*   mxminpoly A == the minimal polynomial of A, i.e., the smallest monic     *)
-(*                  polynomial that annihilates A (A must be nontrivial).     *)
+(*   char_poly A  == the characteristic polynomial of A.                      *)
+(* char_poly_mx A == a matrix whose determinant is char_poly A.               *)
+(*  companionmx p == a matrix whose char_poly is p                            *)
+(*   mxminpoly A  == the minimal polynomial of A, i.e., the smallest monic     *)
+(*                   polynomial that annihilates A (A must be nontrivial).    *)
 (* degree_mxminpoly A == the (positive) degree of mxminpoly A.                *)
 (* mx_inv_horner A == the inverse of horner_mx A for polynomials of degree    *)
 (*                  smaller than degree_mxminpoly A.                          *)