FinMatrix.Matrix.MatrixQ


Require Export QExt.
Require Export MatrixModule.
Require MatrixQc.

Matrix theory come from common implementations


Include (BasicMatrixTheory ElementTypeQ).

Open Scope Q_scope.
Open Scope vec_scope.
Open Scope mat_scope.

Matrix theory applied to this type

Inverse matrix over Q type
Section inv_Q.

  Import MatrixQc.

Check matrix invertibility with lists as input by GE
  Definition minvtblebListGE (n : nat) (dl : dlist Q) : bool :=
    minvtblebListGE n (Q2Qc_dlist dl).

Inverse matrix with lists for input and output by GE
  Definition minvListGE (n : nat) (dl : dlist Q) : dlist Q :=
    Qc2Q_dlist (minvListGE n (Q2Qc_dlist dl)).

Check matrix invertibility with lists as input by AM
  Definition minvtblebListAM (n : nat) (dl : dlist Q) : bool :=
    minvtblebListAM n (Q2Qc_dlist dl).

Inverse matrix with lists for input and output by AM
  Definition minvListAM (n : nat) (dl : dlist Q) : dlist Q :=
    Qc2Q_dlist (minvListAM n (Q2Qc_dlist dl)).

End inv_Q.

Usage demo

Section test.
  Open Scope vec_scope.

  Let u := @l2v 3 [1;2;-3].
  Let v := @f2v 3 (fun i => -1 + nat2Q i).

  Open Scope mat_scope.

  Let M1 := @l2m 3 3 [[1;-3;-2];[-2;1;-4];[-1;4;-1]].
End test.