Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-19 18:51 194bde8f

View on Github →

feat(order/monotone): add monotone_int_of_le_succ etc (#10895) Also use new lemmas to golf zpow_strict_mono and prove zpow_strict_anti.

Estimated changes

Modified src/algebra/field_power.lean

added theorem zpow_strict_anti

Modified src/data/complex/exponential.lean

Modified src/order/monotone.lean

added theorem antitone_int_of_succ_le

deleted theorem forall_ge_le_of_forall_le_succ

added theorem int.rel_of_forall_rel_succ_of_le

added theorem int.rel_of_forall_rel_succ_of_lt

added theorem monotone_int_of_le_succ

added theorem nat.rel_of_forall_rel_succ_of_le

added theorem nat.rel_of_forall_rel_succ_of_le_of_le

added theorem nat.rel_of_forall_rel_succ_of_le_of_lt

added theorem nat.rel_of_forall_rel_succ_of_lt

added theorem strict_anti_int_of_succ_lt

modified theorem strict_anti_nat_of_succ_lt

added theorem strict_mono_int_of_lt_succ

modified theorem strict_mono_nat_of_lt_succ

Modified src/order/order_iso_nat.lean