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 src/algebra/group_power.lean

Modified src/data/complex/basic.lean

modified def complex.of_real

Modified src/data/int/basic.lean

added theorem add_monoid_hom.eq_int_cast

modified theorem int.cast_id

deleted theorem int.eq_cast

added def int.of_nat_hom

Modified src/data/nat/cast.lean

added theorem add_monoid_hom.eq_nat_cast

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

Modified src/data/polynomial.lean

Modified src/data/rat/cast.lean

deleted theorem rat.eq_cast

deleted theorem rat.eq_cast_of_ne_zero

added theorem ring_hom.eq_rat_cast

added theorem ring_hom.map_rat_cast

Modified src/data/real/basic.lean

modified def real.of_rat