lcm_dvd_iff — Mathlib

English

For a finite set s and function f, s.lcm f divides a if and only if every mapped element divides a.

Русский

Для конечного множества s и функции f, s.lcm f делит a тогда и только тогда, когда каждое f(b) делит a.

LaTeX

$$$$ \\mathrm{lcm}(s,f) \\mid a \\iff \\forall b \\in s, \\; f(b) \\mid a. $$$$

Lean4

@[simp]
theorem lcm_dvd_iff {a : α} : s.lcm f ∣ a ↔ ∀ b ∈ s, f b ∣ a :=
  by
  apply Iff.trans Multiset.lcm_dvd
  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⟩

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