mathlib3
64f6903e - chore(*): migrate `nat/int/rat.eq_cast` to bundled homs (#2427)

Commit
5 years ago
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`. Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Author
Parents
Loading