Commit 2025-07-11 09:29 2c172273

View on Github →

feat(Valued/WithZeroMulInt): generalize to any mul-archimedean Valued (#26887) in preparation for ValuativeRel the statement of tendsto_zero_pow_of_le_exp_neg_one is really about MulArchimedean group-with-zeros so, helper lemmas were added in upstream files

Estimated changes

Modified Mathlib/Algebra/Order/Archimedean/Basic.lean

added theorem exists_pow_lt

Modified Mathlib/GroupTheory/ArchimedeanDensely.lean

added theorem exists_pow_lt₀

Modified Mathlib/Topology/Algebra/Valued/WithZeroMulInt.lean

modified theorem Valued.exists_pow_lt_of_le_exp_neg_one

modified theorem Valued.tendsto_zero_pow_of_le_exp_neg_one

added theorem Valued.tendsto_zero_pow_of_v_lt_one