diff options
| author | Georges Gonthier | 2015-11-30 18:29:12 +0000 |
|---|---|---|
| committer | Georges Gonthier | 2015-12-04 15:07:16 +0000 |
| commit | a2b30aa3fd9e2204dbbffa85c04c7e7b9992b53a (patch) | |
| tree | 5c46a958f8ea12b2694512e94c19585bc76fe14b | |
| parent | 7737563121b069ab5e15f1f8ddf2533d3fef1434 (diff) | |
Add finLmodType, finLalgType and finAlgType instances
| -rw-r--r-- | mathcomp/algebra/matrix.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 18790ee..4469266 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -2053,8 +2053,12 @@ Proof. by apply/matrixP=> k i; rewrite !mxE; apply: eq_bigr => j _; rewrite !mxE. Qed. +Canonical matrix_finLmodType (R : finRingType) m n := + [finLmodType R of 'M[R]_(m, n)]. Canonical matrix_finRingType (R : finRingType) n' := Eval hnf in [finRingType of 'M[R]_n'.+1]. +Canonical matrix_finLalgType (R : finRingType) n' := + [finLalgType R of 'M[R]_n'.+1]. (* Parametricity over the algebra structure. *) Section MapRingMatrix. @@ -2478,6 +2482,9 @@ Implicit Arguments lin_mul_row [R m n]. Implicit Arguments lin_mulmx [R m n p]. Prenex Implicits lin_mul_row lin_mulmx. +Canonical matrix_finAlgType (R : finComRingType) n' := + [finAlgType R of 'M[R]_n'.+1]. + (*****************************************************************************) (********************** Matrix unit ring and inverse matrices ****************) (*****************************************************************************) |