Matrix overhaul

[lowasser]

DO NOT SUBMIT: to be broken up into several smaller PRs; this PR exists to prototype the entire whole and to show the long-term goal of the sub-PRs.

This PR:

• renames the existing tuple-based matrix concept to "grid"
• defines a "matrix" concept around finite sequences instead of tuples
• gets addition and scalar multiplication on matrices "for free" from the dependent product of modules (one of several reasons to use finite sequences)
• defines square matrices, diagonal matrices, and identity matrices
• defines matrix multiplication and shows its properties (which never happened for the original tuple-based matrix concept)
• shows that square matrices on commutative rings form a unital associative algebra

That's probably enough to start with; matrix similarity, diagonalizability, determinants, traces, and more can come next...