dvd_sum — Mathlib

English

As before, divisibility distributes over sums of lists: if a divides every term, then a divides the sum.

Русский

Как и ранее, делимость распределяется над суммой элементов списка: если a делит каждый член, то a делит их сумма.

LaTeX

$$$\forall x \in l, a \mid x \Rightarrow a \mid \sum l$$$

Lean4

theorem dvd_sum [NonUnitalSemiring R] {a} {l : List R} (h : ∀ x ∈ l, a ∣ x) : a ∣ l.sum := by
  induction l with
  | nil => exact dvd_zero _
  | cons x l ih =>
    rw [List.sum_cons]
    exact dvd_add (h _ mem_cons_self) (ih fun x hx ↦ h x (mem_cons_of_mem _ hx))

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