feat(Topology/Algebra/Support): compact multiplicative support under product operations (#38022)

Add compact-multiplicative-support closure under product-like operations to `Mathlib/Topology/Algebra/Support.lean`. The main abstraction is a `Submonoid (α → β)` consisting of functions with compact multiplicative support; `List`, `Multiset`, and `Finset` product closures then follow by applying `Submonoid.{list,multiset,}_prod_mem`. All declarations carry `@[to_additive]` to generate `HasCompactSupport.{addSubmonoid, list_sum, multiset_sum, finset_sum}`.

New declarations:
- `HasCompactMulSupport.submonoid` (+ `HasCompactSupport.addSubmonoid`)
- `HasCompactMulSupport.list_prod` (+ `.list_sum`)
- `HasCompactMulSupport.multiset_prod` (+ `.multiset_sum`)
- `HasCompactMulSupport.finset_prod` (+ `.finset_sum`)

Type class hypotheses minimised per result: `MulOneClass` for the submonoid, `Monoid` for `list_prod`, `CommMonoid` for `multiset_prod` and `finset_prod`. Single new import: `Mathlib.Algebra.Group.Submonoid.BigOperators`.

Drafted with assistance from Claude Opus 4.6 for Lean-syntax help and Mathlib API lookup; the choice of declarations, type class minimisation, and final verification are my own. Scope expansion (submonoid extraction + `list_prod` / `multiset_prod`) was [suggested on Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/small.20PR.3A.20finset_prod.20for.20compact.20support/with/585291281) by Eric Wieser.

Co-authored-by: alejandrosotofranco <soto.alejandro2025@gmail.com>

Author: alejandro-soto-franco

Mathlib/Topology/Algebra/Support.lean

@@ -5,6 +5,7 @@ Authors: Floris van Doorn, Patrick Massot
 -/
 module
 
+public import Mathlib.Algebra.Group.Submonoid.BigOperators
 public import Mathlib.Algebra.GroupWithZero.Indicator
 public import Mathlib.Algebra.Module.Basic
 public import Mathlib.Algebra.Order.Group.Unbundled.Abs
@@ -393,8 +394,45 @@ protected lemma HasCompactMulSupport.one {α β : Type*} [TopologicalSpace α] [
     HasCompactMulSupport (1 : α → β) := by
   simp [HasCompactMulSupport]
 
+variable (α β) in
+/-- The submonoid of functions `α → β` with compact multiplicative support. -/
+@[to_additive /-- The additive submonoid of functions `α → β` with compact support. -/]
+def HasCompactMulSupport.submonoid : Submonoid (α → β) where
+  carrier := {f | HasCompactMulSupport f}
+  one_mem' := .one
+  mul_mem' := .mul
+
+@[to_additive (attr := simp)]
+theorem HasCompactMulSupport.mem_submonoid_iff {f : α → β} :
+    f ∈ HasCompactMulSupport.submonoid α β ↔ HasCompactMulSupport f :=
+  Iff.rfl
+
+@[to_additive]
+theorem HasCompactMulSupport.list_prod {α β : Type*} [TopologicalSpace α] [Monoid β]
+    {l : List (α → β)} (hl : ∀ f ∈ l, HasCompactMulSupport f) :
+    HasCompactMulSupport l.prod :=
+  list_prod_mem (S := HasCompactMulSupport.submonoid α β) hl
+
 end Monoid
 
+section CommMonoid
+
+variable [TopologicalSpace α] [CommMonoid β]
+
+@[to_additive]
+theorem HasCompactMulSupport.multiset_prod
+    (m : Multiset (α → β)) (hm : ∀ f ∈ m, HasCompactMulSupport f) :
+    HasCompactMulSupport m.prod :=
+  multiset_prod_mem (S := HasCompactMulSupport.submonoid α β) m hm
+
+@[to_additive]
+theorem HasCompactMulSupport.finset_prod {ι : Type*}
+    {s : Finset ι} {f : ι → α → β} (hf : ∀ i ∈ s, HasCompactMulSupport (f i)) :
+    HasCompactMulSupport (∏ i ∈ s, f i) :=
+  prod_mem (S := HasCompactMulSupport.submonoid α β) hf
+
+end CommMonoid
+
 section DivisionMonoid
 
 @[to_additive]