Hello! I am looking for information about math-comp type VectType (for finite-dimensional vector space)
1) Is there information other than https://math-comp.github.io/htmldoc_1_12_0/mathcomp.algebra.vector.html ?
2) Are there bijections from and to different VectTypes when their dimension is equal?
3) Is there a proof that polynomials of a given degree (smaller than n) form a VectType?
Thanks!
Sylvie Boldo said:
Hello! I am looking for information about math-comp type VectType (for finite-dimensional vector space)
1) Is there information other than https://math-comp.github.io/htmldoc_1_12_0/mathcomp.algebra.vector.html ?
I don't think there is another doc, no.
2) Are there bijections from and to different VectTypes when their dimension is equal?
I'm not aware of such a contribution. It wouldn't be too hard to add though, I could do it or guide anyone trying to do it.
3) Is there a proof that polynomials of a given degree (smaller than n) form a VectType?
There is this old PR which should be refreshed and merged.
I suggest to define:
Definition vspace_fun {vT vT' : vectType} (U : {vspace vT}) (V : {vspace vT'}) (v : vT) :=
\sum_(i < \dim U) coord (vbasis U) i v *: (vbasis V)`_i
And prove stuff like:
Lemma vspace_fun (vT vT' : vectType) (U : {vspace vT}) (V : {vspace vT'}) : \dim U <= \dim V ->
cancel (vspace_fun U V) (vspace_fun V U).
Proof. ... Admitted.
and
Lemma vspace_is_linear (vT vT' : vectType) (U : {vspace vT}) (V : {vspace vT'}) :
linear (vspace_fun U V).
Proof. ... Admitted.
Canonical vspace_fun_linear (vT vT' : vectType) (U : {vspace vT}) (V : {vspace vT'}) :=
Linear (vspace_is_linear U V).
Thanks! I'll have a look at all that.
(U <= V)%VS was not typing indeed. I also changed it to (\dim U <= \dim V)%nat :-)
But I have problems proving the cancel property on vspace_fun as it seems to require that v \in U. Did I miss something?
Last updated: Mar 28 2024 at 18:02 UTC