Commit 2025-01-02 20:35 0b74e84c
View on Github →refactor(NumberTheory/Ostrowski): use AbsoluteValue
instead of MulRingNorm
(#20362)
This PR
- replaces
MulRingNorm R
byAbsoluteValue R ℝ
in the material developed inMathlib.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
toMathlib.Algebra.Order.AbsoluteValue.Basic
andMathlib.Algebra.Order.EuclideanAbsoluteValue
toMathlib.Algebra.Order.AbsoluteValue.Euclidean
- adds some API for
AbsoluteValue
to matchMulRingNorm
(inMathlib.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.