mathlib3
feat(data/matrix/basic): use `⬝` as notation for all products
#15585
Open
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Overview
Commits
1
Changes
View On
GitHub
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
feat(data/matrix/basic): use `⬝` as notation for all products
bd709307
eric-wieser
added
RFC
eric-wieser
added
awaiting-review
eric-wieser
added
awaiting-CI
eric-wieser
removed
awaiting-review
kim-em
added
too-late
Login to write a write a comment.
Login via GitHub
Reviewers
No reviews
Assignees
No one assigned
Labels
RFC
awaiting-CI
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub