Mathlib Changelog
v3
Changelog
About
Github
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
Modified
data/num/lemmas.lean
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