Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-09 08:54 cc75e4ef

View on Github →

chore(data/nat/cast): a few simp/norm_cast lemmas (#4549)

Estimated changes

modified theorem nat.cast_le
added theorem nat.cast_le_one
added theorem nat.cast_lt_one
modified theorem nat.coe_nat_dvd
added theorem nat.one_le_cast
added theorem nat.one_lt_cast
added theorem nat.strict_mono_cast