Commit 2021-08-02 14:22 9a251f1e

refactor(data/matrix/basic): merge duplicate algebra structures (#8486) By putting the algebra instance in the same file as scalar, a future patch can probably remove matrix.scalar entirely (it's just another spelling of algebra_map). Note that we actually had two instances of algebra R (matrix n n R) in different files, and the second one was strictly more general than the first. This removes the less general one. Moving the imports around like this changes the number of simp lemmas available in downstream files, which can make simp slow enough to push a proof into a timeout. A lot of files were expecting a transitive import of algebra.algebra.basic to import data.fintype.card, which it no longer does; hence the need to add this import explicitly. There are no new lemmas or generalizations in this change; the old matrix_algebra has been deleted, and everything else has been moved with some variables renamed.