mathlib3
refactor(data/matrix/basic): Remove matrix.scalar
#8516
Open

refactor(data/matrix/basic): Remove matrix.scalar #8516

eric-wieser wants to merge 3 commits into master from eric-wieser/remove-matrix-scalar
eric-wieser
github-actions github-actions added blocked-by-other-PR
eric-wieser eric-wieser force pushed from 1c962c3a to 86b4c021 5 years ago
github-actions github-actions removed blocked-by-other-PR
eric-wieser
eric-wieser commented on 2021-08-02
eric-wieser eric-wieser added awaiting-author
github-actions github-actions added merge-conflict
eric-wieser refactor(data/matrix/basic): Remove matrix.scalar
dfcf4aa2
eric-wieser move bundled versions
62fc900a
eric-wieser Merge commit '5afd09aace106e3160dacca2484e15e74f35ab7c' into eric-wie…
9f4b19cf
eric-wieser eric-wieser force pushed from 86b4c021 to 9f4b19cf 5 years ago
github-actions github-actions removed merge-conflict
github-actions github-actions added merge-conflict
github-actions
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