Commit 2022-12-16 03:06 f30d8e52

View on Github →

feat port Data.Nat.Pow (#1050) aba57d4d3dae35460225919dcd82fe91355162f9

depends on #1043

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Pow.lean

added theorem Nat.dvd_of_pow_dvd

added theorem Nat.lt_of_pow_dvd_right

added theorem Nat.lt_pow_self

added theorem Nat.lt_two_pow

added theorem Nat.mod_pow_succ

added theorem Nat.mul_lt_mul_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_pow_iff

added theorem Nat.one_lt_two_pow'

added theorem Nat.one_lt_two_pow

added theorem Nat.pow_div

added theorem Nat.pow_dvd_of_le_of_pow_dvd

added theorem Nat.pow_dvd_pow_iff_le_right'

added theorem Nat.pow_dvd_pow_iff_le_right

added theorem Nat.pow_dvd_pow_iff_pow_le_pow

added theorem Nat.pow_le_iff_le_left

added theorem Nat.pow_le_iff_le_right

added theorem Nat.pow_left_injective

added theorem Nat.pow_left_strict_mono

added theorem Nat.pow_lt_iff_lt_left

added theorem Nat.pow_lt_iff_lt_right

added theorem Nat.pow_lt_pow_of_lt_left

added theorem Nat.pow_lt_pow_of_lt_right

added theorem Nat.pow_lt_pow_succ

added theorem Nat.pow_mod

added theorem Nat.pow_right_injective

added theorem Nat.pow_right_strict_mono

added theorem Nat.sq_sub_sq

added theorem StrictMono.nat_pow