mathlib

456898c7 - feat(data/finsupp/basic): Version of `finsupp.prod_add_index` with weaker premises (#11353)

feat(data/finsupp/basic): Version of `finsupp.prod_add_index` with weaker premises (#11353) A simpler proof of `finsupp.prod_add_index : (f + g).prod h = f.prod h * g.prod h` with weaker premises. Specifically, this only requires: * `[add_zero_class M]` rather than `[add_comm_monoid M]` * `h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 1` rather than `h_zero : ∀a, h a 0 = 1`. * `h_add : ∀ (a ∈ f.support ∪ g.support) b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂` rather than `h_add : ∀ a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂` (thanks to Anne Baanen for spotting this weakening). The original version has been retained and re-named to `finsupp.prod_add_index'`, since in some places this is more convenient to use. (There was already a lemma called `prod_add_index'` which appears not to have been used anywhere. This has been renamed to `prod_hom_add_index`.) Discussed in this Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Variant.20of.20finsupp.2Eprod_add_index.3F