Commit 2020-10-23 20:04 5afeb9b9

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.