mathlib3
feat(data/matrix/basic): use `⬝` as notation for all products
#15585
Open

feat(data/matrix/basic): use `⬝` as notation for all products #15585

eric-wieser wants to merge 1 commit into master from eric-wieser/matrix-mul-notation
eric-wieser
eric-wieser feat(data/matrix/basic): use `⬝` as notation for all products
bd709307
eric-wieser eric-wieser added RFC
eric-wieser eric-wieser added awaiting-review
eric-wieser eric-wieser added awaiting-CI
eric-wieser eric-wieser removed awaiting-review
kim-em kim-em added too-late

Login to write a write a comment.

Login via GitHub

Reviewers
No reviews
Assignees
No one assigned
Labels
Milestone