English
Let α be a type with a Cancel–CommMonoidWithZero structure and a NormalizedGCDMonoid, and assume a decidable equality. For any multiset s, the least common multiple of its deduplicated version equals the least common multiple of s itself: lcm(dedup(s)) = lcm(s).
Русский
Пусть α — тип сCancelCommMonoidWithZero и NormalizedGCDMonoid, и задано декартово равенство. Для любой мультисеты s наибольший общий кратник после устранения повторов равен наибольшему общему кратнику самой mультсет: lcm(dedup(s)) = lcm(s).
LaTeX
$$$(\operatorname{dedup} s).\mathrm{lcm} = s.\mathrm{lcm}$$$
Lean4
@[simp]
theorem lcm_dedup (s : Multiset α) : (dedup s).lcm = s.lcm :=
Multiset.induction_on s (by simp) fun a s IH ↦ by
by_cases h : a ∈ s; swap; · simp [IH, h]
simp only [h, dedup_cons_of_mem, IH, lcm_cons]
unfold lcm
rw [← cons_erase h, fold_cons_left, ← lcm_assoc, lcm_same]
apply lcm_eq_of_associated_left (associated_normalize _)
