Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-24 07:00 44de64f1

View on Github →

chore(algebra/order/with_zero): Move unrelated lemmas (#15676) Move a bunch of lemmas that were not about whatever_with_zero from algebra.order.with_zero to algebra.group_power.order. Delete nat.le_zero_iff in favor of le_zero_iff.

Estimated changes

added theorem left.one_le_pow_of_le
added theorem left.pow_le_one_of_le
added theorem left.pow_lt_one_iff
added theorem left.pow_lt_one_of_lt
added theorem monoid_hom.map_neg
added theorem monoid_hom.map_neg_one
modified theorem pow_le_pow_of_le_left'
added theorem pow_lt_pow_succ
added theorem pow_lt_pow₀
added theorem pow_pos_iff
added theorem right.one_le_pow_of_le
added theorem right.pow_le_one_of_le
added theorem right.pow_lt_one_iff
added theorem right.pow_lt_one_of_lt
deleted theorem left.one_le_pow_of_le
deleted theorem left.pow_lt_one_iff
deleted theorem left.pow_lt_one_of_lt
deleted theorem monoid_hom.map_neg
deleted theorem monoid_hom.map_neg_one
deleted theorem monoid_hom.map_sub_swap
deleted theorem pow_le_pow_of_le
deleted theorem pow_lt_pow_succ
deleted theorem pow_lt_pow₀
deleted theorem pow_pos_iff
deleted theorem right.one_le_pow_of_le
deleted theorem right.pow_le_one_of_le
deleted theorem right.pow_lt_one_iff
deleted theorem right.pow_lt_one_of_lt
deleted theorem nat.le_zero_iff