diff options
| -rw-r--r-- | ChangeLog | 4 | ||||
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 9 |
2 files changed, 9 insertions, 4 deletions
@@ -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. *) |