dvd_gcd_iff — Mathlib

English

An element a divides s.gcd f if and only if a divides f(b) for every b in s.

Русский

Элемент a делит s.gcd f тогда и только тогда, когда a делит f(b) для каждого b ∈ s.

LaTeX

$$$a \mid s.gcd f \iff \forall b \in s,\ a \mid f(b)$$$

Lean4

theorem dvd_gcd_iff {a : α} : a ∣ s.gcd f ↔ ∀ b ∈ s, a ∣ f b :=
  by
  apply Iff.trans Multiset.dvd_gcd
  simp only [Multiset.mem_map, and_imp, exists_imp]
  exact ⟨fun k b hb ↦ k _ _ hb rfl, fun k a' b hb h ↦ h ▸ k _ hb⟩

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