Theorems · Theorem · group theory

one_lt_finprod_cond

∀ {ι : Type u_3} {M : Type u_7} [inst : CommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelMonoid M] {f : ι → M}
  {p : ι → Prop},
  (∀ (i : ι), p i → 1 ≤ f i) →
    (∃ i, p i ∧ 1 < f i) → (Function.mulSupport f ∩ {i | p i}).Finite → 1 < ∏ᶠ (i : ι) (_ : p i), f i

Defined in

Mathlib.Algebra.BigOperators.Finprod

Cited by

1 results in Mathlib

Foundations

Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidPartialOrderIsOrderedCancelMonoid