dvd_sum — Mathlib

English

In any nonunital semiring, if a divides every element of a multiset s, then a divides the sum of s: (∀ x ∈ s, a ∣ x) → a ∣ s.sum.

Русский

В неполной безеденной полусистеме: если a делит каждый элемент мультимножества s, то a делит их сумму: (∀ x ∈ s, a | x) → a | ∑_{x ∈ s} x.

LaTeX

$$$$ \big( \forall x \in s,\ a \mid x \big) \Rightarrow a \mid s.\sum. $$$$

Lean4

theorem dvd_sum : (∀ x ∈ s, a ∣ x) → a ∣ s.sum :=
  Multiset.induction_on s (fun _ ↦ dvd_zero _) fun x s ih h ↦
    by
    rw [sum_cons]
    exact dvd_add (h _ (mem_cons_self _ _)) (ih fun y hy ↦ h _ <| mem_cons.2 <| Or.inr hy)

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