prod_dvd_prod_of_dvd — Mathlib

English

If for every a in S we have g1(a) divides g2(a) in a commutative monoid N, then the product of g1 over S divides the product of g2 over S.

Русский

Если для каждого элемента a множества S выполняется, что g1(a) делит g2(a) в коммутативном моноиде N, то произведение g1 по S делит произведение g2 по S.

LaTeX

$$$\\big( \\mathrm{prod}(\\mathrm{map} g_1 S) \\big) \\mid \\big( \\mathrm{prod}(\\mathrm{map} g_2 S) \\big)$$$

Lean4

theorem prod_dvd_prod_of_dvd [CommMonoid N] {S : Multiset M} (g1 g2 : M → N) (h : ∀ a ∈ S, g1 a ∣ g2 a) :
    (Multiset.map g1 S).prod ∣ (Multiset.map g2 S).prod :=
  by
  apply Multiset.induction_on' S
  · simp
  intro a T haS _ IH
  simp [mul_dvd_mul (h a haS) IH]

Похожие утверждения