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

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 •.

TODO: do the same for ℤ. In another PR, let's keep this one reasonable.

The main pain points in the refactor are the following:

• we have to adjust the definition of pow to make sure that to_additive works. In particular, a ^ 0 is not any more defeq to 1, and a^ (n+1) is not any more defeq to a * a ^ n. Many proofs were using this, so I had to add a lot of rw pow_zero and rw pow_succ. I don't think it's a problem: relying on anecdotal defeqs in proofs is just prone to breaking. To me, the only place where defeq really matters is where the user has no control on it, i.e., on typeclass diamonds.

• to construct structures, refine and refine_struct are often perturbed by opt_params and auto_params that need a typeclass which is not already declared. Here, the autoparam field (nsmul : ℕ → M → M := nsmul_rec) requires typeclasses has_zero M and has_add M, that Lean core somehow provides when declaring the full structure, but when using refine or refine_struct this is not so clear, and there are issues with metavariables left. In some situations, it worked fine, and sometimes not. The most efficient way I found is to use refine_struct, and fill the nsmul field like

  nsmul := @nsmul_rec _ ⟨0⟩ ⟨(+)⟩,

replacing the autoparam by hand.

• Since the structures become more complicated, proofs get slower. In particular, many proofs that were on the edge of timeout became too slow, and had to be fixed by avoiding heavy refls. This has been done in [Merged by Bors] - chore(*): speedup slow proofs #7148 (after which mathlib build time on CI dropped down by roughly 6 minutes).