dvd_prod — Mathlib

English

In a commutative monoid, if a is an element of a finite list l, then a divides the product of all elements of l.

Русский

В коммутативном моноиде, если элемент a принадлежит списку l, то a делит произведение всех элементов списка l.

LaTeX

$$$$ a \in l \Rightarrow a \mid l.prod $$$$

Lean4

theorem dvd_prod [CommMonoid M] {a} {l : List M} (ha : a ∈ l) : a ∣ l.prod :=
  by
  let ⟨s, t, h⟩ := append_of_mem ha
  rw [h, prod_append, prod_cons, mul_left_comm]
  exact dvd_mul_right _ _

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