Big operators on a finset in groups with zero involving order #
This file contains the results concerning the interaction of finset big operators with groups with zero, where order is involved.
theorem
Finset.one_le_prod
{α : Type u_1}
{M : Type u_2}
(s : Finset α)
[CommMonoidWithZero M]
[Preorder M]
[ZeroLEOneClass M]
[PosMulMono M]
{f : α → M}
(hf : ∀ (i : α), 1 ≤ f i)
:
A version of Finset.one_le_prod'' for PosMulMono in place of MulLeftMono.