mathlib

447cbe9c - refactor({data,linear_algebra}/matrix/block): Generalize block indexing (#14035)

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. Co-authored-by: Eric <ericrboidi@gmail.com> Co-authored-by: Alexander Bentkamp <bentkamp@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>