Theorem AbsoluteValue.over_def

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