Theorems · Theorem · group theory
Finset.prod_eq_zero_iff
∀ {ι : Type u_1} {M₀ : Type u_4} [inst : CommMonoidWithZero M₀] {f : ι → M₀} {s : Finset ι} [Nontrivial M₀]
[NoZeroDivisors M₀], ∏ x ∈ s, f x = 0 ↔ ∃ a ∈ s, f a = 0- Cited by
- 9 results in Mathlib
- Foundations
- Depth 61 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
- Nontrivialstatement and proof · cited by 2,416
- Finset.prodstatement and proof · cited by 2,356
- CommMonoidWithZerostatement and proof · cited by 913
- one_ne_zeroproof · cited by 885
- NoZeroDivisorsstatement and proof · cited by 545
- Finset.induction_onproof · cited by 167
- Finset.prod_insertproof · cited by 109
- mul_eq_zeroproof · cited by 94
- Finset.exists_mem_insertproof · cited by 2
Cited by9
Results whose statement or proof uses this declaration.
- Finset.prod_ne_zero_iffproof · cited by 45
- Affine.Triangle.prod_eq_prod_one_sub_of_mem_line_point_lineMapproof · cited by 2
- int_prod_range_posproof · cited by 1
- Real.iSup_prod_eq_prod_iSup_of_nonnegproof · cited by 1
- AddSubgroup.relIndex_iInf_leproof · cited by 1
- NumberField.InfiniteAdeleRing.norm_eq_zero_of_not_isUnitproof · cited by 0
- DFinsupp.prod_eq_zero_iffproof · cited by 0
- Subgroup.relIndex_iInf_leproof · cited by 0
- Finsupp.prod_eq_zero_iffproof · cited by 0