Naming & notation: `Algebra.Order.AbsoluteValue`

Stream: mathlib4

[Arien Malec]

I might back away from this, but I'm looking this file, and it's got the notation R →ₙ* S, which isn't yet defined in Mathlib4 (looking at the mathlib docs, it's defined in algebra.group.hom as the multiplicative homomorphism), and I'm not sure I understand how the notation is picked up in mathlib?

In addition, it defines both a structure and a class for AbsoluteValue -- the latter is currently called IsAbsoluteValue -- wondering if LawfulAbsoluteValue is the right name here?

[Kevin Buzzard]

We're not ready to port AbsoluteValue, it's on the list in error.

[Yaël Dillies]

We want to get rid of is_absolute_value

[Scott Morrison]

No, no renames like this are happening during the port. is_absolute_value will turn into IsAbsoluteValue.