Commit 2017-11-02 17:13 2da9bef0

View on Github →

feat(data/nat/cast,...): add char_zero typeclass for cast_inj As pointed out by @kbuzzard, the complex numbers are an important example of an unordered characteristic zero field for which we will want cast_inj to be available.

Estimated changes

Modified data/int/basic.lean

modified theorem int.cast_eq_zero

modified theorem int.cast_inj

modified theorem int.cast_ne_zero

Modified data/nat/cast.lean

added theorem add_group.char_zero_of_inj_zero

added theorem char_zero_of_inj_zero

modified theorem nat.cast_eq_zero

modified theorem nat.cast_inj

modified theorem nat.cast_ne_zero

added theorem ordered_cancel_comm_monoid.char_zero_of_inj_zero

Modified data/rat.lean

modified theorem rat.cast_add

modified theorem rat.cast_bit0

modified theorem rat.cast_bit1

modified theorem rat.cast_div

modified theorem rat.cast_eq_zero

modified theorem rat.cast_inj

modified theorem rat.cast_inv

modified theorem rat.cast_mk

modified theorem rat.cast_mul

modified theorem rat.cast_ne_zero

modified theorem rat.cast_sub