Commit 2025-09-17 11:12 88520b7e

refactor(AbsoluteValue): generalise equivalence to non-real valued absolute values (#27964)

• Abstract the definition of AbsoluteValue.IsEquiv to any AbsoluteValue R S via preservation of partial orders (previously defined only for real absolute value using the power relation (v .)^c = w)
• Show AbsoluteValue.IsEquiv is equivalent to the power definition when the values are real
• Two inequivalent absolute values v and w have a point x at which 1 < v x and w x < 1