mathlib3

89c8112f - feat(topology/algebra/monoid): `finprod` is eventually equal to `finset.prod` (#13013)

feat(topology/algebra/monoid): `finprod` is eventually equal to `finset.prod` (#13013) Motivated by https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Using.20partitions.20of.20unity Co-authored-by: Patrick Massot <patrickmassot@free.fr>