Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-06 02:20 f8f8be9a

View on Github →

chore(algebra/order/field): split out file about powers (#17352) This just pulls some material about powers of elements in linearly ordered fields into a separate file, as it isn't on the critical path to linear_ordered_field ℚ. This will break in CI a few times as I find the downstream imports that need it.

Estimated changes

deleted theorem div_pow_le
deleted theorem nat.cast_le_pow_div_sub
deleted theorem nat.zpow_ne_zero_of_pos
deleted theorem one_le_zpow_of_nonneg
deleted theorem one_lt_zpow
deleted theorem zpow_bit0_nonneg
deleted theorem zpow_bit0_pos
deleted theorem zpow_bit1_neg_iff
deleted theorem zpow_bit1_nonneg_iff
deleted theorem zpow_bit1_nonpos_iff
deleted theorem zpow_bit1_pos_iff
deleted theorem zpow_inj
deleted theorem zpow_injective
deleted theorem zpow_le_iff_le
deleted theorem zpow_le_max_iff_min_le
deleted theorem zpow_le_max_of_min_le
deleted theorem zpow_le_of_le
deleted theorem zpow_le_one_of_nonpos
deleted theorem zpow_lt_iff_lt
deleted theorem zpow_strict_anti
deleted theorem zpow_strict_mono
deleted theorem zpow_two_nonneg
deleted theorem zpow_two_pos_of_ne_zero
added theorem div_pow_le
added theorem one_le_zpow_of_nonneg
added theorem one_lt_zpow
added theorem zpow_bit0_nonneg
added theorem zpow_bit0_pos
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_strict_anti
added theorem zpow_strict_mono
added theorem zpow_two_nonneg