hi everyone,
I want to define a submatrix Mij is formed by throwing away row i and column j :
The initial matrix of order n, this splitting gives n smaller matrix of order
n-1.
I define the definition of submatrix as follow:
val dsyz_matrix = Define`dszy_matrix (A:('n,'n) matrix) (r:num) (c:num) =
(\i j. (FCP x y. if (i < r /\ j < c) then (A %% x %% y) else
if (i < r /\ j > c) then (A %% x %% (y + 1)) else
if(i > r /\ j > c) then (A %% (x + 1) %% (y + 1)) else
(A %% (x + 1) %% y)))`;
And the result is like this:
val dsyz_matrix =
|- !(A :('n, 'n) matrix) (r :num) (c :num).
(dszy_matrix A r c :num -> num ->('a, 'b) matrix) =
(\(i :num) (j :num).
FCP (x :num) (y :num).
(if i < r /\ j < c then
A %% x %% y
else
(if i < r /\ j > c then
A %% x %% (y + (1 :num))
else
(if i > r /\ j > c then
A %% (x + (1 :num)) %% (y + (1 :num))
else
A %% (x + (1 :num)) %% y)))) : thm
But the submatrix of order is not n – 1.
How can I correct the definition that limit the order n – 1 of submatrix? Could
anybody give me some hints about it?
I appreciate your help.
Best wishes,
Amy------------------------------------------------------------------------------
Increase Visibility of Your 3D Game App & Earn a Chance To Win $500!
Tap into the largest installed PC base & get more eyes on your game by
optimizing for Intel(R) Graphics Technology. Get started today with the
Intel(R) Software Partner Program. Five $500 cash prizes are up for grabs.
http://p.sf.net/sfu/intelisp-dev2dev
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
