Re: Symbolic verification of determinant identities

[Bill Allombert <Bill.Allombert@math.u-bordeaux.fr>]

On Fri, Sep 08, 2017 at 09:56:52PM +0000, Jacques Gélinas wrote:
> Compound determinants such as D3 in
>  D1  = matdet([ a, b; b, c ]); D2  = matdet([ a, c; b, d ]);
>  D3  = matdet([ a, 2*b; D1, D2 ]);
> are manipulated to prove that D3>0. 
> 
> How can PARI/GP be used to verify the formal equivalence of such expressions ?
> Of course, I would prefer not to have to write the determinants twice
> in original and in final form, if possible.
> 
> Now I run into problems in verifying, for example, the simple identity
>  D1 == matdet([ a,  b + L*a; b + L*a, c + 2*L*b + L^2*a ]) 
> by using substitutions 
> 
>   D1 == subst(subst(D1,b,b+L*a),c,c+2*L*b+L^2*a)          \\ seems to work ?
>   D1 == subst(subst(D1,c,c+2*L*b+L^2*a),b,b+L*a)          \\ oups !!! Nope!

You should use substvec if you need to do simultaneous substitutions.

? D1 == substvec(D1,[b,c],[b+L*a,c+2*L*b+L^2*a])
%3 = 1

Cheers,
Bill.