Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-21 06:57 972aa423

View on Github →

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.

Estimated changes

deleted theorem alg_hom.map_int_cast
deleted theorem ring_hom.map_eq_zero
deleted theorem ring_hom.map_ne_zero
added theorem map_eq_zero
added theorem map_ne_zero
modified theorem complex.of_real_int_cast
modified theorem is_R_or_C.of_real_int_cast
added theorem eq_int_cast'
added theorem eq_int_cast
added theorem ext_int'
modified theorem int.cast_id
added theorem map_int_cast
modified theorem pi.coe_int
modified theorem pi.int_apply
modified theorem ring_hom.eq_int_cast'
deleted theorem ring_hom.eq_int_cast
deleted theorem ring_hom.map_int_cast
modified theorem polynomial.C_eq_int_cast
modified theorem polynomial.map_int_cast
modified theorem polynomial.map_eq_zero
modified theorem zmod.cast_int_cast
modified theorem subring.coe_int_cast
modified theorem subring.coe_nat_cast
modified theorem subring_class.coe_int_cast
modified theorem subring_class.coe_nat_cast