Commit 2023-01-02 21:04 1d18deec

View on Github →

feat: port algebra.order.field.power (#1256)

depends on: #1159
depends on: #1251

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Field/Power.lean

added theorem Even.zpow_abs

added theorem Even.zpow_pos_iff

added theorem Nat.cast_le_pow_div_sub

added theorem Nat.cast_le_pow_sub_div_sub

added theorem Nat.zpow_ne_zero_of_pos

added theorem Odd.zpow_neg_iff

added theorem Odd.zpow_nonpos_iff

added theorem Odd.zpow_pos_iff

added theorem div_pow_le

added theorem one_le_zpow_of_nonneg

added theorem one_lt_zpow

added theorem zpow_bit0_abs

added theorem zpow_bit0_nonneg

added theorem zpow_bit0_pos

added theorem zpow_bit0_pos_iff

added theorem zpow_bit1_neg_iff

added theorem zpow_bit1_nonneg_iff

added theorem zpow_bit1_nonpos_iff

added theorem zpow_bit1_pos_iff

added theorem zpow_inj

added theorem zpow_injective

added theorem zpow_le_iff_le

added theorem zpow_le_max_iff_min_le

added theorem zpow_le_max_of_min_le

added theorem zpow_le_of_le

added theorem zpow_le_one_of_nonpos

added theorem zpow_lt_iff_lt

added theorem zpow_strictAnti

added theorem zpow_strictMono

added theorem zpow_two_nonneg

added theorem zpow_two_pos_of_ne_zero