From ceec387c6e912f83b918955011caacc14a825da3 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 3 Aug 2018 12:59:32 +0200 Subject: update ChangeLog and doc --- mathcomp/algebra/mxpoly.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'mathcomp') 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. *) -- cgit v1.2.3