Commit 2022-02-28 16:08 456898c7

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