On 02/09/2020 23:25, 'fl' via Metamath wrote:
The best to do is redefine the <" ...>" operator so that it takes (1
... N) as its set of indices and then fix up all the proofs referring
to the definition.
You should have only one definition for matrices, tuples and words
since all that is the same story. Or at most two: one with a abstract
finite
set of indices and another one with (1... N).
Like mentioned by Norm in the original thread about index start for
words, I'm afraid that would be a huge work, there are already hundreds
of theorems making use of that range.
That's why I would like to ask the same about matrices now, before
writing more theorems within whichever convention.
Of course we shall try to use arbitrary sets whenever possible... which
leads me to the other point:
On the other hand, does any one have any idea or suggestion about
how I could have expressed the Laplace expansion without integer
indices, on any finite set index?
The laplace expansion of the determinant (just one level of expansion,
not recursive) requires a choice of row to expand over (which is an
element of the index set), and then it's an unordered finite sum. No
integers needed.
Yes, but what is the factor you apply to each submatrix determinant ?
The textbooks all have ` -1 ^ ( i + j ) ` , where i and j are /integer/
indices. Of course, start index does not matter, but where do those
numbers come from when working with arbitrary sets?
_
Thierry
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/df59b8f5-d216-cfc2-4530-9871f945cbaf%40gmx.net.
