diff options
| author | Enrico Tassi | 2020-10-26 15:16:07 +0100 |
|---|---|---|
| committer | GitHub | 2020-10-26 15:16:07 +0100 |
| commit | 03003d87b98a836e692ffe46cba9fe6041336b91 (patch) | |
| tree | df9107d380f6836aedb3a89425c608e19ee9fee7 /mathcomp/algebra/mxpoly.v | |
| parent | 86f41151dd20220a19ae7b000c48e1464451a608 (diff) | |
| parent | a635c0047ec4c5f0880046c5970d50b283361110 (diff) | |
Merge pull request #584 from CohenCyril/stability
Theory of stability of a subspace by a matrix representing an endomorphism.
Diffstat (limited to 'mathcomp/algebra/mxpoly.v')
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index 79a28bf..9ffbe77 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -313,6 +313,15 @@ rewrite (bigD1 j)//= ihp mxE ?eqxx mulr1n -mulrnAl big1 ?addr0//. by move=> k /negPf nkF; rewrite mxE nkF mulr0. Qed. +Lemma horner_mx_stable (K : fieldType) m n p + (V : 'M[K]_(n.+1, m.+1)) (f : 'M_m.+1) : + stablemx V f -> stablemx V (horner_mx f p). +Proof. +move=> V_fstab; elim/poly_ind: p => [|p c]; first by rewrite rmorph0 stablemx0. +move=> fp_stable; rewrite rmorphD rmorphM/= horner_mx_X horner_mx_C. +by rewrite stablemxD ?stablemxM ?fp_stable ?stablemxC. +Qed. + Prenex Implicits horner_mx powers_mx. Section CharPoly. |