Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-10-17 00:02 2e7651aa

View on Github →

feat(data/num): add tactics for evaluating arithmetic expressions made of literals, including x \le y and x ^ y

Estimated changes

added def cast_znum
added def int.znum_coe
added def num.nat_num_coe
added theorem norm_num.bit0_le_one
added theorem norm_num.bit0_le_zero
added theorem norm_num.bit1_le_bit0
added theorem norm_num.bit1_le_one
added theorem norm_num.bit1_le_zero
added theorem norm_num.one_le_bit0
added theorem norm_num.one_le_bit1
added theorem norm_num.one_le_one
added theorem norm_num.pow_bit0
added theorem norm_num.pow_bit1
added theorem norm_num.pow_one
added theorem norm_num.pow_zero
added theorem norm_num.zero_le_bit0
added theorem norm_num.zero_le_bit1
added theorem norm_num.zero_le_one
added theorem norm_num.zero_le_zero
added def num.add1
added def num.add_n
added theorem num.bit0_le_bit0
added theorem num.denote_add1
added def num.num_le
added theorem num.one_le_denote
added def num.pos_le
added theorem num.zero_le_denote
added def num.znum_le