basic): add more general smul compatibility instances
#19187

Closed

[Merged by Bors] - feat(data/mv_polynomial/basic): add more general smul compatibility instances #19187

eric-wieser wants to merge 1 commit into master from eric-wieser/mv_polynomial-tower

feat(data/mv_polynomial/basic): add more general smul compatibility i…

7fbdfdc2

eric-wieser added awaiting-review

eric-wieser added mathport

eric-wieser added awaiting-CI

eric-wieser requested a review from

riccardobrasca 2 years ago

github-actions added modifies-synchronized-file

github-actions added delegated

github-actions removed awaiting-review

github-actions removed awaiting-CI

github-actions added ready-to-merge

bors changed the title ~~feat(data/mv_polynomial/basic): add more general smul compatibility instances~~ [Merged by Bors] - feat(data/mv_polynomial/basic): add more general smul compatibility instances 2 years ago

bors closed this 2 years ago

bors deleted the eric-wieser/mv_polynomial-tower branch 2 years ago

Reviewers

riccardobrasca

Assignees

No one assigned

Labels

ready-to-merge delegated mathport modifies-synchronized-file

Milestone

No milestone

mathlib3 [Merged by Bors] - feat(data/mv_polynomial/basic): add more general smul compatibility instances #19187 Closed

[Merged by Bors] - feat(data/mv_polynomial/basic): add more general smul compatibility instances #19187

mathlib3
[Merged by Bors] - feat(data/mv_polynomial/basic): add more general smul compatibility instances
#19187

Closed