diff options
| author | Kazuhiko Sakaguchi | 2020-10-30 12:12:26 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-10-30 12:12:26 +0900 |
| commit | bd02346e4038871f4d4021dd84df384fc8cf9aa4 (patch) | |
| tree | 62f0dc367dc9ab3fa4210ee5e003b03a34eda25f /mathcomp/algebra/mxpoly.v | |
| parent | a9767fcd4713fc37e57fc9cc2a7864879effbf73 (diff) | |
Use `exp` rather than `X` for exponents of polynomials
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} := |