Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-01 23:18 76f41e7e

View on Github →

chore(data/nat): split out data/nat/pow (#7758) Split lemmas about the power operation on natural numbers into its own file; slightly reduces imports.

Estimated changes

deleted theorem nat.succ_eq_one_add
added theorem nat.succ_eq_one_add
deleted theorem nat.dvd_of_pow_dvd
deleted theorem nat.lt_pow_self
deleted theorem nat.lt_size
deleted theorem nat.lt_size_self
deleted theorem nat.lt_two_pow
deleted theorem nat.mod_pow_succ
deleted theorem nat.mul_lt_mul_pow_succ
deleted theorem nat.not_pos_pow_dvd
deleted theorem nat.one_le_pow'
deleted theorem nat.one_le_pow
deleted theorem nat.one_le_two_pow
deleted theorem nat.one_lt_pow'
deleted theorem nat.one_lt_pow
deleted theorem nat.one_lt_two_pow'
deleted theorem nat.one_lt_two_pow
deleted theorem nat.one_shiftl
deleted theorem nat.pow_div
deleted theorem nat.pow_le_iff_le_left
deleted theorem nat.pow_le_iff_le_right
deleted theorem nat.pow_left_injective
deleted theorem nat.pow_left_strict_mono
deleted theorem nat.pow_lt_iff_lt_left
deleted theorem nat.pow_lt_iff_lt_right
deleted theorem nat.pow_lt_pow_of_lt_left
deleted theorem nat.pow_lt_pow_succ
deleted theorem nat.pow_right_injective
deleted theorem nat.pow_right_strict_mono
deleted theorem nat.shiftl'_ne_zero_left
deleted theorem nat.shiftl'_tt_eq_mul_pow
deleted theorem nat.shiftl'_tt_ne_zero
deleted theorem nat.shiftl_eq_mul_pow
deleted theorem nat.shiftr_eq_div_pow
deleted theorem nat.size_bit0
deleted theorem nat.size_bit1
deleted theorem nat.size_bit
deleted theorem nat.size_eq_zero
deleted theorem nat.size_le
deleted theorem nat.size_le_size
deleted theorem nat.size_one
deleted theorem nat.size_pos
deleted theorem nat.size_pow
deleted theorem nat.size_shiftl'
deleted theorem nat.size_shiftl
deleted theorem nat.size_zero
deleted theorem nat.sq_sub_sq
deleted theorem nat.zero_shiftl
deleted theorem nat.zero_shiftr
deleted theorem strict_mono.nat_pow
added theorem nat.dvd_of_pow_dvd
added theorem nat.lt_pow_self
added theorem nat.lt_size
added theorem nat.lt_size_self
added theorem nat.lt_two_pow
added theorem nat.mod_pow_succ
added theorem nat.not_pos_pow_dvd
added theorem nat.one_le_pow'
added theorem nat.one_le_pow
added theorem nat.one_le_two_pow
added theorem nat.one_lt_pow'
added theorem nat.one_lt_pow
added theorem nat.one_lt_two_pow'
added theorem nat.one_lt_two_pow
added theorem nat.one_shiftl
added theorem nat.pow_div
added theorem nat.pow_le_iff_le_left
added theorem nat.pow_left_injective
added theorem nat.pow_lt_iff_lt_left
added theorem nat.pow_lt_pow_succ
added theorem nat.shiftl'_tt_ne_zero
added theorem nat.shiftl_eq_mul_pow
added theorem nat.shiftr_eq_div_pow
added theorem nat.size_bit0
added theorem nat.size_bit1
added theorem nat.size_bit
added theorem nat.size_eq_zero
added theorem nat.size_le
added theorem nat.size_le_size
added theorem nat.size_one
added theorem nat.size_pos
added theorem nat.size_pow
added theorem nat.size_shiftl'
added theorem nat.size_shiftl
added theorem nat.size_zero
added theorem nat.sq_sub_sq
added theorem nat.zero_shiftl
added theorem nat.zero_shiftr
added theorem strict_mono.nat_pow