Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-17 16:30 64f6903e

View on Github →

chore(*): migrate nat/int/rat.eq_cast to bundled homs (#2427) Now it is ring_hom.eq_*_cast, ring_hom.map_*_cast, add_monoid_hom.eq_int/nat_cast. Also turn complex.of_real into a ring_hom.

Estimated changes

modified theorem nat.cast_id
deleted theorem nat.eq_cast'
deleted theorem nat.eq_cast
added theorem ring_hom.eq_nat_cast
modified theorem ring_hom.map_nat_cast