diff options
| author | Laurent Théry | 2020-11-16 16:54:53 +0100 |
|---|---|---|
| committer | GitHub | 2020-11-16 16:54:53 +0100 |
| commit | bae9cdb2a12083b8170c3999886839cc1495f969 (patch) | |
| tree | 9d33feef64df064a0fecd6222b6c656072fbaa95 /mathcomp/algebra/mxpoly.v | |
| parent | 1a098263b335ccc4cf72880662dccbe79185a8ab (diff) | |
| parent | 8b98bcedc4523e07e4fdc118159cf171366e952d (diff) | |
Merge pull request #636 from CohenCyril/fix_comm_mxC
`comm(Cmx|_mxC)` -> `comm(_scalar_mx|_mx_scalar)`
Diffstat (limited to 'mathcomp/algebra/mxpoly.v')
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index c7f8fb1..19a23e6 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -274,7 +274,7 @@ Section OneMatrix. Variable A : 'M[R]_n. -Definition horner_mx := horner_morph (comm_mxC^~ A). +Definition horner_mx := horner_morph (comm_mx_scalar^~ A). Canonical horner_mx_additive := [additive of horner_mx]. Canonical horner_mx_rmorphism := [rmorphism of horner_mx]. @@ -317,7 +317,8 @@ Qed. Lemma comm_mx_horner A B p : comm_mx A B -> comm_mx A (horner_mx B p). Proof. -by move=> fg; apply: commr_horner => // i; rewrite coef_map; apply/commCmx. +move=> fg; apply: commr_horner => // i. +by rewrite coef_map; apply/comm_scalar_mx. Qed. Lemma comm_horner_mx A B p : comm_mx A B -> comm_mx (horner_mx A p) B. |