theorem
IsLeftRegular.prod
{ι : Type u_2}
{R : Type u_3}
[CommMonoid R]
{s : Finset ι}
{f : ι → R}
(h : ∀ i ∈ s, IsLeftRegular (f i))
:
IsLeftRegular (∏ i ∈ s, f i)
theorem
IsRightRegular.prod
{ι : Type u_2}
{R : Type u_3}
[CommMonoid R]
{s : Finset ι}
{f : ι → R}
(h : ∀ i ∈ s, IsRightRegular (f i))
:
IsRightRegular (∏ i ∈ s, f i)
theorem
IsRegular.prod
{ι : Type u_2}
{R : Type u_3}
[CommMonoid R]
{s : Finset ι}
{f : ι → R}
(h : ∀ i ∈ s, IsRegular (f i))
:
IsRegular (∏ i ∈ s, f i)