Commit 2026-10-21 16:48 573535ab

View on Github →

feat(Analysis/Normed/Ring/WithAbs): more API for AbsoluteValue.under (#43841) This PR adds more API for AbsoluteValue.under, following the analogous API for Ideal.under.

Estimated changes

Modified Mathlib/Analysis/Normed/Ring/WithAbs.lean

added theorem AbsoluteValue.LiesOver.trans

added theorem AbsoluteValue.over_def

added theorem AbsoluteValue.under_apply

added theorem AbsoluteValue.under_liesOver_iff

added theorem AbsoluteValue.under_under