mathlib
972aa423 - refactor(data/int/cast): Use hom classes (#16024)

Commit
3 years ago
refactor(data/int/cast): Use hom classes (#16024) Restate `map_eq_zero`, `map_ne_zero`, `map_int_cast`, `eq_int_cast'` using `monoid_with_zero_hom_class`/`ring_hom_class` instead of `monoid_with_zero_hom`/`ring_hom`. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Author
Parents
Loading