Theorems · Theorem · order theory
Finset.prod_pos
∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [ZeroLEOneClass R]
[PosMulStrictMono R] [Nontrivial R] {f : ι → R} {s : Finset ι}, (∀ i ∈ s, 0 < f i) → 0 < ∏ i ∈ s, f i- Cited by
- 25 results in Mathlib
- Foundations
- Depth 55 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- PartialOrderstatement and proof · cited by 6,410
- Nontrivialstatement and proof · cited by 2,416
- Finset.prodstatement · cited by 2,356
- CommMonoidWithZerostatement and proof · cited by 913
- zero_lt_oneproof · cited by 598
- mul_posproof · cited by 374
- ZeroLEOneClassstatement and proof · cited by 304
- PosMulStrictMonostatement and proof · cited by 151
- Finset.prod_inductionproof · cited by 18
Cited by25
Results whose statement or proof uses this declaration.
- BoundingSieve.nu_pos_of_dvd_prodPrimesproof · cited by 4
- AddMonoid.exponent_ne_zero_iff_range_addOrderOf_finiteproof · cited by 3
- MultilinearMap.bound_of_shell_of_norm_map_coord_zeroproof · cited by 3
- Monoid.exponent_ne_zero_iff_range_orderOf_finiteproof · cited by 3
- Nat.multinomial_consproof · cited by 3
- integral_sin_pow_posproof · cited by 3
- primorial_posproof · cited by 3
- Height.mulHeight₁_sum_leproof · cited by 2
- MvPowerSeries.gaussNorm_eq_zero_iffproof · cited by 2
- Multiset.bell_mul_eqproof · cited by 2
- Nat.totient_eq_div_primeFactors_mulproof · cited by 2