Commit 2025-01-02 20:35 0b74e84c

View on Github →

refactor(NumberTheory/Ostrowski): use AbsoluteValue instead of MulRingNorm (#20362) This PR

  • replaces MulRingNorm R by AbsoluteValue R ℝ in the material developed in Mathlib.NumberTheory.Ostrowski
  • does some cleanup (naming convention, remove redundant name parts etc.)
  • and also some golfing... In addition, it
  • creates a new folder Mathlib.Algebra.Order.AbsoluteValue
  • moves Mathlib.Algebra.Order.AbsoluteValue to Mathlib.Algebra.Order.AbsoluteValue.Basic and Mathlib.Algebra.Order.EuclideanAbsoluteValueto Mathlib.Algebra.Order.AbsoluteValue.Euclidean
  • adds some API for AbsoluteValue to match MulRingNorm (in Mathlib.Algebra.Order.AbsoluteValue.Basic)
  • adds a new file Mathlib.Algebra.Order.AbsoluteValue.Equivalence with material on equivalence of real-valued absolute values. See the discussion on Zulip.

Estimated changes