update ChangeLog and doc

1 files changed, 5 insertions, 4 deletions

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.                          *)