Commit 2023-07-03 14:48 e0de6cd4

feat: add lemma tendsto_pow_atTop_nhds_0_iff_lt_1 (#5656) Add lemma tendsto_pow_atTop_nhds_0_iff_lt_1 showing the reverse implication of tendsto_pow_atTop_nhds_0_of_lt_1: if the geometric progression of an element in an Archimedean field tends to 0, the element is strictly less than 1.