diff options
| author | Georges Gonthier | 2015-11-30 16:19:28 +0000 |
|---|---|---|
| committer | Georges Gonthier | 2015-12-04 15:07:15 +0000 |
| commit | 0b227098257e188bdb59e59e63b24e392e21dd87 (patch) | |
| tree | 676ff688b127a316c729378233b5cdfaa1ba9b0e /mathcomp/algebra | |
| parent | 12ee0cfa20b9411d2a59aabfcd8d20b07a8975db (diff) | |
Remove more redundant power type structures
Diffstat (limited to 'mathcomp/algebra')
| -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. |