Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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>
- Loading branch information