lcm_dvd — Mathlib

English

The lcm of a multiset divides a if and only if every element of the multiset divides a.

Русский

LCM мультимножества делится на a тогда и только тогда каждый элемент множества делит a.

LaTeX

$$s.lcm ∣ a ↔ ∀ b ∈ s, b ∣ a$$

Lean4

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

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