Commit 2025-01-10 11:19 e6e79027

feat: AbsoluteValue.IsNontrivial (#20588) This introduces v.IsNontrivial : Prop for v : AbsoluteValue R S; this states that v x ≠ 1 for some x ≠ 0. This is more convenient to use than v ≠ .trivial since it does not require additional assumptions on R or S (whereas AbsoluteValue.trivial needs x = 0 to be decidable in R, R to have no zero divisors and S to be nontrivial). We also adapt NumberTheory.Ostrowski to use IsNontrivial instead of ≠ .trivial.