diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/ssralg.v | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index 7d4fdc0..a494f3f 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -5977,7 +5977,6 @@ Lemma ffunMnE f n x : (f *+ n) x = f x *+ n. Proof. by rewrite -[n]card_ord -!sumr_const sum_ffunE. Qed. End FinFunZmod. -Canonical exp_zmodType (M : zmodType) n := [zmodType of M ^ n]. Section FinFunRing. @@ -6046,8 +6045,6 @@ Canonical ffun_lmodType := Eval hnf in LmodType R {ffun aT -> rT} ffun_lmodMixin. End FinFunLmod. -Canonical exp_lmodType (R : ringType) (M : lmodType R) n := - [lmodType R of M ^ n]. (* External direct product. *) Section PairZmod. |