finprod of elements of a submonoid

Stream: Is there code for X?

[Kevin Buzzard]

Do we have this:

import Mathlib.Algebra.BigOperators.Finprod
import Mathlib.Algebra.Group.Submonoid.Basic

lemma Submonoid.finprod_mem {G : Type*} [CommMonoid G] {M : Submonoid G} {ι : Type*}
    {S : Set ι} {f : ι → G} (hf : ∀ i ∈ S, f i ∈ M) : (∏ᶠ i ∈ S, f i) ∈ M := by
  sorry

[Kevin Buzzard]

lemma Submonoid.finprod_mem {G : Type*} [CommMonoid G] {M : Submonoid G} {ι : Type*}
    {S : Set ι}
    {f : ι → G} (hf : ∀ i ∈ S, f i ∈ M) : (∏ᶠ i ∈ S, f i) ∈ M := by
  by_cases hS : (S ∩ mulSupport f).Finite
  · rw [finprod_mem_eq_prod _ hS]
    apply Submonoid.prod_mem M <| fun i hi ↦ hf _ ?_
    exact mem_of_mem_diff ((Finite.mem_toFinset hS).mp hi)
  · exact finprod_mem_eq_one_of_infinite hS ▸ M.one_mem

[Johan Commelin]

I hope we have a generic docs#prod_mem

[Kevin Buzzard]

yeah but for finsets.

[Johan Commelin]

Aah, oops

[Edward van de Meent]

docs#finprod_induction seems relevant

[Eric Wieser]

lemma Submonoid.finprod_mem {G : Type*} [CommMonoid G] {M : Submonoid G} {ι : Type*}
    {S : Set ι} {f : ι → G} (hf : ∀ i ∈ S, f i ∈ M) : (∏ᶠ i ∈ S, f i) ∈ M :=
  finprod_mem_induction (· ∈ M) (one_mem _) (fun _ _ => mul_mem) hf

[Yury G. Kudryashov]

You should prove it for a finprod indexed on i : (_ : Sort*)