mathlib3
f00b7c0c - chore(*): work on removing deprecated is_X_hom typeclasses (#3258)

Commit
5 years ago
chore(*): work on removing deprecated is_X_hom typeclasses (#3258) It's far from over, but as I was bumping up against issues in `polynomial.lean` and `mv_polynomial.lean`, I'm going to PR this part for now, and then wait to return to it when other PRs affecting `polynomial.lean` have cleared. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Author
Parents
Loading