diff options
Diffstat (limited to 'mathcomp/algebra/mxpoly.v')
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index acf0e95..c7f8fb1 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -938,7 +938,7 @@ Lemma mxdirect_sum_geigenspace {in P &, injective a_} -> mxdirect (\sum_(i | P i) geigenspace g (a_ i)). Proof. move=> /inj_in_eq eq_a; apply: mxdirect_sum_kermx => i j Pi Pj Nji. -by rewrite coprimepXr ?coprimepXl// coprimep_XsubC root_XsubC eq_a. +by rewrite coprimep_expr ?coprimep_expl// coprimep_XsubC root_XsubC eq_a. Qed. Definition eigenpoly n (g : 'M_n) : pred {poly K} := |