Theorem AbsoluteValue.exists_lt_one_one_le_of_not_isEquiv

Modification history

2025-09-17 11:12
Mathlib/Analysis/AbsoluteValue/Equivalence.lean
refactor(AbsoluteValue): generalise equivalence to non-real valued absolute values (#27964) …
Added AbsoluteValue.exists_lt_one_one_le_of_not_isEquivView on Github →