diff options
| author | Cyril Cohen | 2020-09-08 03:48:55 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-10-21 15:57:42 +0200 |
| commit | a635c0047ec4c5f0880046c5970d50b283361110 (patch) | |
| tree | 88c4ec6f85e6ba97bf2dc039fe07bcb8d63993b6 /mathcomp/algebra/mxpoly.v | |
| parent | ed3d822bc5a1c3759140b7fd7567f2b4278ae0be (diff) | |
Theory of stability of a subspace by a matrix representing an endomorphism.
Added `stablemx` notation and a few lemmas about it.
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 24de1bc..9cc7c94 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. |