Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-11-02 02:32 2883c1bb

View on Github →

feat(data/num/lemmas): finish znum isomorphism proof

Estimated changes

added theorem num.cast_add
modified theorem num.cast_inj
modified theorem num.cast_le
modified theorem num.cast_lt
modified theorem num.cast_mul
modified theorem pos_num.cast_inj
modified theorem pos_num.cast_le
modified theorem pos_num.cast_lt
modified theorem pos_num.cast_mul
deleted theorem znum.add_of_nat
modified theorem znum.cast_add
added theorem znum.cast_inj
added theorem znum.cast_le
added theorem znum.cast_lt
added theorem znum.cast_mul
added theorem znum.cast_succ
added theorem znum.cmp_to_int
added theorem znum.le_to_int
added theorem znum.lt_to_int
added theorem znum.mul_to_int
added theorem znum.to_int_inj
added theorem znum.to_of_int