mathlib3
c1a7c195 - chore(data/polynomial/basic): add missing is_scalar_tower and smul_comm_class instances (#6592)

Commit
4 years ago
chore(data/polynomial/basic): add missing is_scalar_tower and smul_comm_class instances (#6592) These already exist for `mv_polynomial`, but the PR that I added them in forgot to add them for `polynomial`. Notably, this provides the instance `is_scalar_tower R (mv_polynomial S₁ R) (polynomial (mv_polynomial S₁ R))`.
Author
Parents
Loading