Theorems · Theorem · order theory
WithTop.prod_ne_top
∀ {ι : Type u_1} {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] [inst_1 : NoZeroDivisors M₀] [inst_2 : Nontrivial M₀]
[inst_3 : DecidableEq M₀] {s : Finset ι} {f : ι → WithTop M₀}, (∀ i ∈ s, f i ≠ ⊤) → ∏ i ∈ s, f i ≠ ⊤A product of finite terms is finite.
- Defined in
- Mathlib.Algebra.BigOperators.WithTop
- Cited by
- 3 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
- Top.topstatement and proof · cited by 9,680
- WithTopstatement and proof · cited by 3,754
- Nontrivialstatement and proof · cited by 2,416
- Finset.prodstatement · cited by 2,356
- CommMonoidWithZerostatement and proof · cited by 913
- NoZeroDivisorsstatement and proof · cited by 545
- WithTop.coe_ne_topproof · cited by 43
- Finset.prod_inductionproof · cited by 18
- WithTop.mul_ne_topproof · cited by 4
Cited by3
Results whose statement or proof uses this declaration.
- ENNReal.prod_ne_topproof · cited by 6
- WithTop.prod_eq_top_ex_topproof · cited by 1
- ENat.prod_ne_topproof · cited by 0