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

deleted theorem is_ring_hom.map_fpow
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
modified theorem gaussian_int.to_complex_add
modified theorem gaussian_int.to_complex_mul
modified theorem gaussian_int.to_complex_neg
modified theorem gaussian_int.to_complex_one
modified theorem gaussian_int.to_complex_sub
deleted theorem is_ring_hom.injective
deleted theorem is_ring_hom.map_div
deleted theorem is_ring_hom.map_eq_zero
deleted theorem is_ring_hom.map_inv
deleted theorem is_ring_hom.map_ne_zero
modified def equiv.perm.of_subtype
deleted theorem equiv.perm.of_subtype_one