Theorem AbsoluteValue.exists_one_lt_lt_one_pi_of_not_isEquiv

Modification history

2025-10-01 10:39
Mathlib/Analysis/AbsoluteValue/Equivalence.lean
feat: collections of non-trivial and pairwise inequivalent absolute values contain values that diverge around 1 (#27969) …
Added AbsoluteValue.exists_one_lt_lt_one_pi_of_not_isEquivView on Github →