dvd_setGcd_iff — Mathlib

English

For any n, n divides setGcd(s) if and only if every m ∈ s is divisible by n.

Русский

Для любого n верно: n делит setGcd(s) тогда и только тогда, когда каждый элемент m ∈ s делится на n.

LaTeX

$$$n \\mid \\mathrm{setGcd}(s) \\iff \\forall m \\in s,\\; n \\mid m$$$

Lean4

/-- The characterizing property of `Nat.setGcd`. -/
theorem dvd_setGcd_iff : n ∣ setGcd s ↔ ∀ m ∈ s, n ∣ m := by
  simp_rw [setGcd, ← Int.natCast_dvd, dvd_generator_span_iff, Set.forall_mem_image, Int.natCast_dvd_natCast]

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