Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-05 08:41 31ceb624

View on Github →

feat(data/int|nat/basic): add add_monoid_hom.ext_nat/int (#2957)

Estimated changes

added theorem monoid_hom.eq_on_inv
modified theorem add_monoid_hom.eq_int_cast
added theorem add_monoid_hom.ext_int
added def int.cast_add_hom
added theorem int.coe_cast_add_hom
modified theorem add_monoid_hom.eq_nat_cast
added theorem add_monoid_hom.ext_nat
modified theorem nat.abs_cast
modified theorem nat.cast_bit0
modified theorem nat.cast_bit1
modified theorem nat.cast_max
modified theorem nat.cast_min
modified theorem nat.cast_pred
modified theorem nat.cast_sub
modified theorem nat.coe_cast_add_monoid_hom
modified theorem ring_hom.eq_nat_cast
modified theorem ring_hom.ext_nat
modified theorem ring_hom.map_nat_cast