Theorem AbsoluteValue.under_under

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_under View on Github →