Commit 2025-10-01 10:39 6edd0677

feat: collections of non-trivial and pairwise inequivalent absolute values contain values that diverge around 1 (#27969) If $v_1, ..., v_k$ is a a finite collection of non-trivial and pairwise inequivalent absolute values in a field, then for each $v_i$ there is a point $a$ for which $1 < v_i(a)$ while $v_j(a) < 1$ for all $j \neq i$. This generalises the corresponding result on pairs of absolute values PR'd in #27964 This PR continues the work from #22142. Original PR: https://github.com/leanprover-community/mathlib4/pull/22142