English
If a Multiset s of ι has the property that each element a has count(a, s) divisible by k, then s = k • u for some Multiset u.
Русский
Пусть мультсет s по ι имеет свойство: для каждого элемента a кратность count(a, s) делится на k. Тогда существует мультсет u such that s = k • u.
LaTeX
$$$$ \\exists u : \\text{Multiset } ι,\\ s = k \\cdot u \\quad \\text{при условии } \\forall a, a \\in s \\Rightarrow k \\mid \\mathrm{count}(a,s). $$$$
Lean4
theorem exists_smul_of_dvd_count (s : Multiset ι) {k : ℕ} (h : ∀ a : ι, a ∈ s → k ∣ Multiset.count a s) :
∃ u : Multiset ι, s = k • u := by
use ∑ a ∈ s.toFinset, (s.count a / k) • { a }
have h₂ : (∑ x ∈ s.toFinset, k • (count x s / k) • ({ x } : Multiset ι)) = ∑ x ∈ s.toFinset, count x s • { x } :=
by
apply Finset.sum_congr rfl
intro x hx
rw [← mul_nsmul', Nat.mul_div_cancel' (h x (mem_toFinset.mp hx))]
rw [← Finset.sum_nsmul, h₂, toFinset_sum_count_nsmul_eq]
