This seems like a good move. Let's also bench it.

!bench

!bench

Here are the benchmark results for commit b3d2126.
There were significant changes against commit 68f3af6:

  Benchmark                     Metric         Change
  ===================================================
- build                         wall-clock      22.2%
- ~Mathlib.Algebra.Module.PID   instructions     5.7%

Maybe not so good an idea!

@tb65536 Given this bench result, what do you think? Do you want to attempt to improve performance, or shall we punt on this?

Probably just punt for now.