Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-09-17 09:00 a4f6c41e

View on Github →

move(algebra/field_power): Put lemmas in the correct place (#16465) algebra.field_power is only made of lemmas that belong elsewhere. Move them and delete the file. Golf proofs while we're at it and make min_le_of_zpow_le_max an iff.

Estimated changes

added theorem zpow_bit1_neg
deleted theorem div_pow_le
deleted theorem min_le_of_zpow_le_max
deleted theorem nat.zpow_ne_zero_of_pos
deleted theorem one_le_zpow_of_nonneg
deleted theorem one_lt_zpow
deleted theorem pos_div_pow_pos
deleted theorem pow_le_max_of_min_le
deleted theorem rat.cast_zpow
deleted theorem zpow_bit0_nonneg
deleted theorem zpow_bit0_pos
deleted theorem zpow_bit1_neg
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_of_le
deleted theorem zpow_le_one_of_nonpos
deleted theorem zpow_lt_iff_lt
deleted theorem zpow_nonneg
deleted theorem zpow_pos_of_pos
deleted theorem zpow_strict_anti
deleted theorem zpow_strict_mono
deleted theorem zpow_two_nonneg
deleted theorem zpow_two_pos_of_ne_zero
modified theorem pow_lt_pow_of_lt_left
modified theorem strict_mono_on_pow
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_nonneg
added theorem zpow_pos_of_pos
added theorem zpow_strict_anti
added theorem zpow_strict_mono
added theorem zpow_two_nonneg
added theorem pos_div_pow_pos
added theorem rat.cast_zpow