Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-08 10:23 43f52dd7

View on Github →

chore(algebra/char_zero): rename vars, add with_top instance (#4523) Motivated by #3135.

  • Use R as a Type* variable;
  • Add add_monoid_hom.map_nat_cast and with_top.coe_add_hom;
  • Drop versions of char_zero_of_inj_zero, use [add_left_cancel_monoid R] instead.

Estimated changes

modified theorem add_halves'
modified theorem add_self_eq_zero
modified theorem bit0_eq_zero
modified theorem char_zero_of_inj_zero
modified theorem half_add_self
modified theorem half_sub
modified theorem nat.cast_add_one_ne_zero
modified theorem nat.cast_dvd_char_zero
modified theorem nat.cast_eq_zero
modified theorem nat.cast_inj
modified theorem nat.cast_injective
modified theorem nat.cast_ne_zero
modified theorem sub_half
modified theorem two_ne_zero'
modified theorem add_monoid_hom.eq_nat_cast