Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-29 08:02 03374ee3

View on Github →

feat(algebra/order/field): Linearly ordered semifields (#15027) Define linear_ordered_semifield and generalize lemmas within algebra.order.field.

Estimated changes

modified theorem div_pow_le
modified theorem min_le_of_zpow_le_max
modified theorem nat.zpow_ne_zero_of_pos
deleted theorem nat.zpow_pos_of_pos
modified theorem one_le_zpow_of_nonneg
modified theorem one_lt_zpow
modified theorem pos_div_pow_pos
modified theorem pow_le_max_of_min_le
modified theorem rat.cast_zpow
modified theorem ring_equiv.map_zpow
modified theorem ring_hom.map_zpow
modified theorem zpow_bit0_nonneg
modified theorem zpow_bit0_pos
modified theorem zpow_bit1_neg
modified theorem zpow_inj
modified theorem zpow_injective
modified theorem zpow_le_iff_le
modified theorem zpow_le_of_le
modified theorem zpow_le_one_of_nonpos
modified theorem zpow_lt_iff_lt
modified theorem zpow_nonneg
modified theorem zpow_pos_of_pos
modified theorem zpow_strict_anti
modified theorem zpow_strict_mono
modified theorem zpow_two_nonneg
modified theorem zpow_two_pos_of_ne_zero
modified theorem abs_one_div
modified theorem div_neg_iff
modified theorem div_pos_iff
modified theorem exists_add_lt_and_pos_of_lt
modified theorem max_div_div_right_of_nonpos
modified theorem min_div_div_right_of_nonpos
modified theorem nat.cast_le_pow_div_sub
modified theorem nat.cast_le_pow_sub_div_sub
modified theorem sub_one_div_inv_le_two