Commit 2022-09-02 13:28 447cbe9c

refactor({data,linear_algebra}/matrix/block): Generalize block indexing (#14035) Currently many definitions around block matrices are specialized to either ℕ or fin n as the indexing type. This means that some definitions are duplicated and proofs feel unnatural. This PR generalizes them to an arbitrary type (with an order) and subsequently golfs proofs.