Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-01 17:12 f00b7c0c

View on Github →

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.

Estimated changes

modified def complex.conj
deleted theorem complex.conj_add
deleted theorem complex.conj_div
deleted theorem complex.conj_inv
deleted theorem complex.conj_mul
deleted theorem complex.conj_neg
deleted theorem complex.conj_one
deleted theorem complex.conj_pow
deleted theorem complex.conj_sub
deleted theorem complex.conj_zero