Theorem AbsoluteValue.under_liesOver_iff

Modification history

2026-10-21 16:48

Mathlib/Analysis/Normed/Ring/WithAbs.lean

feat(Analysis/Normed/Ring/WithAbs): more API for `AbsoluteValue.under` (#43841) …

Added AbsoluteValue.under_liesOver_iff View on Github →