diff options
Diffstat (limited to 'mathcomp/algebra/vector.v')
| -rw-r--r-- | mathcomp/algebra/vector.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index c4c62c3..4766c74 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -1355,6 +1355,8 @@ Proof. by elim/big_rec2: _ => [|i _ f _ <-]; rewrite lfunE. Qed. End LfunZmodType. +Arguments fun_of_lfunK {R aT rT}. + Section LfunVectType. Variables (R : comRingType) (aT rT : vectType R). @@ -1603,6 +1605,7 @@ Arguments lfunPn {K aT rT f g}. Arguments lker0P {K aT rT f}. Arguments eqlfunP {K aT rT f g v}. Arguments eqlfun_inP {K aT rT V f g}. +Arguments limg_lfunVK {K aT rT f} [x] f_x. Section FixedSpace. @@ -1718,6 +1721,8 @@ Qed. End LinearPreimage. +Arguments lpreimK {K aT rT f} [W] fW. + Section LfunAlgebra. (* This section is a bit of a place holder: the instances we build here can't *) (* be canonical because we are missing an interface for proper vectTypes, *) @@ -1944,7 +1949,7 @@ Canonical subvs_vectType := VectType K subvs_of subvs_vectMixin. End SubVector. Prenex Implicits vsval vsproj vsvalK. Arguments subvs_inj {K vT U} [x1 x2]. -Arguments vsprojK {K vT U} [x]. +Arguments vsprojK {K vT U} [x] Ux. Section MatrixVectType. |