Commit 2025-07-07 15:08 695db8d2

feat: add Valued.tendsto_zero_pow_of_le_neg_one (#21162) If K is a valued ring taking values in the multiplicative integers wth a zero adjoined, then Valued.tendsto_zero_pow_of_le_neg_one is the result that x ^ n tends to zero in this ring if v x is at most -1 valued.