diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 9 |
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. *) |