mathlib
17424431 - refactor(archive/imo) shorten imo1013_q5 using pow_unbounded_of_one_lt (#7373)

Commit

4 years ago

refactor(archive/imo) shorten imo1013_q5 using pow_unbounded_of_one_lt (#7373) Replaces a usage of `one_add_mul_sub_le_pow` with the more direct `pow_unbounded_of_one_lt`.

Author

dwrensha

Parents

3093fd81

mathlib 17424431 - refactor(archive/imo) shorten imo1013_q5 using pow_unbounded_of_one_lt (#7373)

mathlib
17424431 - refactor(archive/imo) shorten imo1013_q5 using pow_unbounded_of_one_lt (#7373)