English
If f1 and f2 are finsupps with f1.support ⊆ f2.support and for each a ∈ f1.support we have g1 a (f1 a) ∣ g2 a (f2 a), then f1.prod g1 divides f2.prod g2.
Русский
Пусть f1 и f2 — финспы, поддержка f1 содержится в поддержке f2, и для каждого a ∈ поддержка f1 верно g1 a (f1 a) делит g2 a (f2 a); тогда произведение f1 по g1 делит произведение f2 по g2.
LaTeX
$$$f_1.prod g_1 \mid f_2.prod g_2$ при $f_1.support \subseteq f_2.support$ и $g_1 a (f_1 a) \mid g_2 a (f_2 a)$ для всех $a$ в $f_1.support$.$$
Lean4
theorem prod_dvd_prod_of_subset_of_dvd [Zero M] [CommMonoid N] {f1 f2 : α →₀ M} {g1 g2 : α → M → N}
(h1 : f1.support ⊆ f2.support) (h2 : ∀ a : α, a ∈ f1.support → g1 a (f1 a) ∣ g2 a (f2 a)) :
f1.prod g1 ∣ f2.prod g2 := by
classical
simp only [Finsupp.prod]
rw [← sdiff_union_of_subset h1, prod_union sdiff_disjoint]
apply dvd_mul_of_dvd_right
apply prod_dvd_prod_of_dvd
exact h2
