Commit 2025-03-04 13:13 a247779a

View on Github →

chore: generalize some absolute value results (#22432) And golf a few proofs.

Estimated changes

Modified Mathlib/Algebra/Order/AbsoluteValue/Basic.lean

modified theorem AbsoluteValue.IsNontrivial.exists_abv_gt_one

modified theorem AbsoluteValue.IsNontrivial.exists_abv_lt_one

deleted def AbsoluteValue.trivial:

added def AbsoluteValue.trivial