Theorems · Theorem · ring theory
Multiset.prod_eq_zero_iff
∀ {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] {s : Multiset M₀},
s.prod = 0 ↔ 0 ∈ s- Cited by
- 7 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Multisetstatement and proof · cited by 2,627
- Nontrivialstatement and proof · cited by 2,416
- CommMonoidWithZerostatement and proof · cited by 913
- NoZeroDivisorsstatement and proof · cited by 545
- Multiset.prodstatement and proof · cited by 528
- Multiset.ofListproof · cited by 290
- Multiset.prod_coeproof · cited by 12
- List.prod_eq_zero_iffproof · cited by 4
- Multiset.quot_mk_to_coeproof · cited by 3
Cited by7
Results whose statement or proof uses this declaration.
- Multiset.prod_ne_zeroproof · cited by 4
- Associates.FactorSet.prod_eq_zero_iffproof · cited by 2
- Height.logHeight₁_eqproof · cited by 1
- Nat.divisors_filter_squarefreeproof · cited by 1
- Ideal.multiset_prod_eq_botproof · cited by 0
- Associates.prod_le_prod_iff_leproof · cited by 0
- Nat.factors_multiset_prod_of_irreducibleproof · cited by 0