Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-31 08:35 85affa45

View on Github →

refactor(*): migrate more files to bundled ring_homs (#2286)

  • refactor(*): migrate more files to bundled ring_homs
  • Fix lint

Estimated changes

added def zmod.cast_hom
added theorem int.coe_cast_ring_hom
deleted theorem int.eq_cast'
deleted theorem is_ring_hom.map_int_cast
added theorem ring_hom.eq_int_cast'
added theorem ring_hom.eq_int_cast
modified theorem ring_hom.map_int_cast
modified theorem mv_polynomial.C_sub
modified theorem mv_polynomial.eval_sub
modified theorem mv_polynomial.eval₂_sub
modified theorem mv_polynomial.map_sub
added theorem nat.coe_cast_ring_hom
modified theorem ring_hom.map_nat_cast