Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-29 01:36 16daabf7

View on Github →

chore(algebra/group_power): golf a few proofs (#10498)

  • move pow_lt_pow_of_lt_one and pow_lt_pow_iff_of_lt_one from algebra.group_power.lemmas to algebra.group_power.order;
  • add strict_anti_pow, use it to golf the proofs of the two lemmas above;
  • golf a few other proofs;
  • add nnreal.exists_pow_lt_of_lt_one.

Estimated changes

deleted theorem pow_lt_pow_iff_of_lt_one
deleted theorem pow_lt_pow_of_lt_one
modified theorem one_lt_pow
added theorem pow_lt_pow_of_lt_one
added theorem strict_anti_pow