chore(*): a few more type-specific ext lemmas (#4741)
* mark lemmas about homs from `multiplicative nat` and `multiplicative int` as `@[ext]`;
* add a special case lemma about linear maps from the base semiring;
* ext lemmas for ring homs from `(add_)monoid_algebra`;
* ext lemmas for multiplicative homs from `multiplicative (α →₀ M)`;
* make sure that Lean can chain ext lemmas by using hom equalities in lemmas about `finsupp`/`(add_)monoid_algebra`.
