Theorem Valued.exists_pow_lt_of_le_exp_neg_one

Modification history

2025-07-11 09:29
Mathlib/Topology/Algebra/Valued/WithZeroMulInt.lean
feat(Valued/WithZeroMulInt): generalize to any mul-archimedean Valued (#26887) …
Modified Valued.exists_pow_lt_of_le_exp_neg_oneView on Github →
2025-07-07 15:08
Mathlib/Topology/Algebra/Valued/WithZeroMulInt.lean
feat: add `Valued.tendsto_zero_pow_of_le_neg_one` (#21162) …
Added Valued.exists_pow_lt_of_le_exp_neg_oneView on Github →