prod_dvd_prod — Mathlib

English

If l1 is a sublist of l2, then the product of l1 divides the product of l2.

Русский

Если l1 является подпоследовательностью l2, то произведение элементов l1 делит произведение элементов l2.

LaTeX

$$$$ l_1 <+ l_2 \Rightarrow l_1.prod \mid l_2.prod $$$$

Lean4

theorem prod_dvd_prod [CommMonoid M] {l₁ l₂ : List M} (h : l₁ <+ l₂) : l₁.prod ∣ l₂.prod :=
  by
  obtain ⟨l, hl⟩ := h.exists_perm_append
  rw [hl.prod_eq, prod_append]
  exact dvd_mul_right _ _

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