Theorem Valued.tendsto_zero_pow_of_v_lt_one

Modification history

2025-07-11 09:29

Mathlib/Topology/Algebra/Valued/WithZeroMulInt.lean

feat(Valued/WithZeroMulInt): generalize to any mul-archimedean Valued (#26887) …

Added Valued.tendsto_zero_pow_of_v_lt_one View on Github →