Theorems · Theorem · commutative algebra
Associates.prod_le_prod_iff_le
∀ {α : Type u_1} [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α] [Nontrivial α]
{p q : Multiset (Associates α)}, (∀ a ∈ p, Irreducible a) → (∀ a ∈ q, Irreducible a) → (p.prod ≤ q.prod ↔ p ≤ q)- Cited by
- 0 results in Mathlib
- Foundations
- Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites20
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
- MulZeroClass.mul_zeroproof · cited by 2,091
- CommMonoidWithZerostatement and proof · cited by 913
- Multiset.prodstatement and proof · cited by 528
- Irreduciblestatement and proof · cited by 496
- UniqueFactorizationMonoidstatement and proof · cited by 279
- Associatesstatement and proof · cited by 210
- Associated.symmproof · cited by 87
- UniqueFactorizationMonoid.factorsproof · cited by 55
- associated_iff_eqproof · cited by 28
- UniqueFactorizationMonoid.factors_prodproof · cited by 18
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.