mathlib
905b875e - chore(data/matrix/block): move block matrices into their own file (#8290)

Commit
4 years ago
chore(data/matrix/block): move block matrices into their own file (#8290) This is a straight cut-and-paste, with no reordering or renaming. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/import.20fails/near/245802618)
Author
Parents
Loading