Re: [isabelle-dev] [isabelle] Matrix-Vector operation

Is there a realistic prospect for uniting these two formalisations of linear algebra? Larry > On 27 Feb 2018, at 11:05, Thiemann, Rene wrote: > > But indeed, Fabian is completely right that lemmas for determinants, etc. are > duplicates. Actually, the JNF-matrices

Re: [isabelle-dev] Fwd: [isabelle] Matrix-Vector operation

Dear all, with HMA_Connect you have a bidirectional connection between “‘a^’n’^m” and “‘a mat”. However, when you transfer something from “‘a^’n^’m” to “‘a mat”, then you get the additional constraint that the dimensions of the matrix must be non-zero. To be more precise, assume the following