notation): split into 2 files (#10199)

Commit

4 years ago

chore(data/matrix/notation): split into 2 files (#10199) I want to use `![a, b]` notation in some files that don't need to import `data.matrix.basic`.

Author

urkud

Parents

daac8545

mathlib 7d240ce1 - chore(data/matrix/notation): split into 2 files (#10199)

mathlib
7d240ce1 - chore(data/matrix/notation): split into 2 files (#10199)