feat: `add_monoid_with_one`, `add_group_with_one` (#12182)
Adds two type classes `add_monoid_with_one R` and `add_group_with_one R` with operations for `ℕ → R` and `ℤ → R`, resp. The type classes extend `add_monoid` and `add_group` because those seem to be the weakest type classes where such a `+₀₁`-homomorphism is guaranteed to exist. The `nat.cast` function as well as `coe : ℕ → R` are implemented in terms of `add_monoid_with_one R`, removing the infamous `nat.cast` diamond. Fixes #946.
Some lemmas are less general now because the algebraic hierarchy is not fine-grained enough, or because the lawful coercion only exists for monoids and above. This generality was not used in mathlib as far as I could tell. For example:
- `char_p.char_p_to_char_zero` now requires a group instead of a left-cancellative monoid, because we don't have the `add_left_cancel_monoid_with_one` class
- `nat.norm_cast_le` now requires a seminormed ring instead of a seminormed group, because we don't have `semi_normed_group_with_one`
