cardFactors_multiset_prod — Mathlib

English

For a multiset s of positive integers with s.prod ≠ 0, Ω(prod s) = sum Ω(s_i) over all elements s_i of s.

Русский

Для мультисета s положительных чисел с s.prod ≠ 0 выполняется Ω(∏ s) = ∑ Ω(s_i).

LaTeX

$$$$\Omega\left(\prod s\right) = \sum_{t \in s} \Omega(t)$$$$

Lean4

theorem cardFactors_multiset_prod {s : Multiset ℕ} (h0 : s.prod ≠ 0) : Ω s.prod = (Multiset.map Ω s).sum := by
  induction s using Multiset.induction_on with
  | empty => simp
  | cons ih => simp_all [cardFactors_mul, not_or]

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