dvd_gcd — Mathlib

English

For any multiset s and element a, a divides gcd(s) if and only if a divides every element of s.

Русский

Для любого мультисетa s и элемента a: a делит gcd(s) тогда и только тогда, когда a делит каждый элемент s.

LaTeX

$$$a \mid s.\mathrm{gcd} \iff \forall b \in s,\ a \mid b$$$

Lean4

theorem dvd_gcd {s : Multiset α} {a : α} : a ∣ s.gcd ↔ ∀ b ∈ s, a ∣ b :=
  Multiset.induction_on s (by simp) (by simp +contextual [or_imp, forall_and, dvd_gcd_iff])

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