refactor(*): kill nat multiplication diamonds (#7084)
An `add_monoid` has a natural `ℕ`-action, defined by `n • a = a + ... + a`, that we want to declare
as an instance as it makes it possible to use the language of linear algebra. However, there are
often other natural `ℕ`-actions. For instance, for any semiring `R`, the space of polynomials
`polynomial R` has a natural `R`-action defined by multiplication on the coefficients. This means
that `polynomial ℕ` has two natural `ℕ`-actions, which are equal but not defeq. The same
goes for linear maps, tensor products, and so on (and even for `ℕ` itself). This is the case on current
mathlib, with such non-defeq diamonds all over the place.
To solve this issue, we embed an `ℕ`-action in the definition of an `add_monoid` (which is by
default the naive action `a + ... + a`, but can be adjusted when needed -- it should always be equal
to this one, but not necessarily definitionally), and declare
a `has_scalar ℕ α` instance using this action. This is yet another example of the forgetful inheritance
pattern that we use in metric spaces, embedding a topology and a uniform structure in it (except that
here the functor from additive monoids to nat-modules is faithful instead of forgetful, but it doesn't
make a difference).
More precisely, we define
```lean
def nsmul_rec [has_add M] [has_zero M] : ℕ → M → M
| 0 a := 0
| (n+1) a := nsmul_rec n a + a
class add_monoid (M : Type u) extends add_semigroup M, add_zero_class M :=
(nsmul : ℕ → M → M := nsmul_rec)
(nsmul_zero' : ∀ x, nsmul 0 x = 0 . try_refl_tac)
(nsmul_succ' : ∀ (n : ℕ) x, nsmul n.succ x = nsmul n x + x . try_refl_tac)
```
For example, when we define `polynomial R`, then we declare the `ℕ`-action to be by multiplication
on each coefficient (using the `ℕ`-action on `R` that comes from the fact that `R` is
an `add_monoid`). In this way, the two natural `has_scalar ℕ (polynomial ℕ)` instances are defeq.
The tactic `to_additive` transfers definitions and results from multiplicative monoids to additive
monoids. To work, it has to map fields to fields. This means that we should also add corresponding
fields to the multiplicative structure `monoid`, which could solve defeq problems for powers if
needed. These problems do not come up in practice, so most of the time we will not need to adjust
the `npow` field when defining multiplicative objects.
With this refactor, all the diamonds are gone. Or rather, all the diamonds I noticed are gone, but if
there are still some diamonds then they can be fixed, contrary to before.
Also, the notation `•ℕ` is gone, just use `•`.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
