lcm_ndinsert — Mathlib

English

Let α be as above and a ∈ α. For any multiset s, the least common multiple of ndinsert(a, s) equals the least common multiple of a together with s: lcm(ndinsert(a, s)) = lcm(a, s.lcm).

Русский

Пусть α удовлетворяет условиям и дан элемент a. Тогда наименьшее общее кратное ndinsert(a, s) равно наименьшему общему кратному a и lcm(s): lcm(ndinsert(a, s)) = lcm(a, s.lcm).

LaTeX

$$$(\mathrm{ndinsert}(a,s)).\mathrm{lcm} = \mathrm{GCDMonoid.lcm}(a, s.\mathrm{lcm})$$$

Lean4

@[simp]
theorem lcm_ndinsert (a : α) (s : Multiset α) : (ndinsert a s).lcm = GCDMonoid.lcm a s.lcm :=
  by
  rw [← lcm_dedup, dedup_ext.2, lcm_dedup, lcm_cons]
  simp

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