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 “‘a mat”
> have been develop
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 t