Theorems · Theorem · ring theory
Finsupp.prod_dvd_prod_of_subset_of_dvd
∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] {f1 f2 : α →₀ M}
{g1 g2 : α → M → N}, f1.support ⊆ f2.support → (∀ a ∈ f1.support, g1 a (f1 a) ∣ g2 a (f2 a)) → f1.prod g1 ∣ f2.prod g2- Cited by
- 4 results in Mathlib
- Foundations
- Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- ZeroCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Finsetstatement and proof · cited by 13,712
- Finsuppstatement and proof · cited by 5,255
- Finset.prodproof · cited by 2,356
- CommMonoidstatement and proof · cited by 2,264
- Finsupp.supportstatement and proof · cited by 828
- Finsupp.prodstatement · cited by 231
- Finset.prod_unionproof · cited by 31
- dvd_mul_of_dvd_rightproof · cited by 29
- Finset.sdiff_disjointproof · cited by 20
- Finset.sdiff_union_of_subsetproof · cited by 12
- Finset.prod_dvd_prod_of_dvdproof · cited by 8
Cited by4
Results whose statement or proof uses this declaration.
- Nat.factorization_le_iff_dvdproof · cited by 18
- Nat.totient_dvd_of_dvdproof · cited by 2
- Nat.coe_divisors_eq_prod_pow_le_factorizationproof · cited by 0
- Nat.coe_properDivisors_eq_prod_pow_lt_factorizationproof · cited by 0