refactor: Multiplicativise abs (#9553)

The current design for `abs` is flawed:
* The `Abs` notation typeclass has exactly two instances: one for `[Neg α] [Sup α]`, one for `[Inv α] [Sup α]`. This means that:
  * We can't write a meaningful hover for `Abs.abs`
  * Fields have two `Abs` instances!
* We have the multiplicative definition but:
  * All the lemmas in `Algebra.Order.Group.Abs` are about the additive version.
  * The only lemmas about the multiplicative version are in `Algebra.Order.Group.PosPart`, and they get additivised to duplicates of the lemmas in `Algebra.Order.Group.Abs`!

This PR changes the notation typeclass with two new definitions (related through `to_additive`): `mabs` and `abs`. `abs` inherits the `|a|` notation and `mabs` gets `|a|ₘ` instead.

The first half of `Algebra.Order.Group.Abs` gets multiplicativised. A later PR will multiplicativise the second half,  and another one will deduplicate the lemmas in `Algebra.Order.Group.PosPart`.

Part of #9411.




Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>

Author: YaelDillies

Mathlib.lean

@@ -1,4 +1,3 @@
-import Mathlib.Algebra.Abs
 import Mathlib.Algebra.AddTorsor
 import Mathlib.Algebra.Algebra.Basic
 import Mathlib.Algebra.Algebra.Bilinear