Refactor linear algebra to use "tuples" for what was "vectors"

[lowasser]

Addresses #1389 .

[fredrik-bakke]

How about using the terminology "finite sequence" (finite-sequence) for functions Fin n -> A. This is consistent with our use of the term "sequence", and leaves the confusing term "functional" available to only be used for linear functionals.

[fredrik-bakke]

Thank you for taking this on, by the way! Sorry if my appreciation is not sufficiently communicated through my other comments.

[fredrik-bakke]

Also, to verify, you are not making any other changes in this PR aside from renaming the concepts, the appropriate files, and fixing the appropriate prose to reflect this renaming, correct?

[lowasser]

That's correct.

[lowasser]

That might no longer be correct. While splitting out files for tuples and finite sequences, I might fill out parts that got left out for one or the other.

[fredrik-bakke]

no worries!

[lowasser]

How would we feel, by the way, about moving the definition of tuples and finite sequences from linear-algebra to lists? It feels more accurate to me.

[fredrik-bakke]

Thank you so much again for implementing these terminological fixes. They turned out to be a lot more involved than I had anticipated, but I'm very glad you implemented them!

[fredrik-bakke]

Does this PR completely resolve #1389, or are there further changes you want to implement, such as regarding "componentwise"?