cardFactors_mul — Mathlib

English

If m,n > 0, then Ω(mn) = Ω(m) + Ω(n).

Русский

Если m,n > 0, то Ω(mn) = Ω(m) + Ω(n).

LaTeX

$$$$\Omega(mn) = \Omega(m) + \Omega(n) \quad (m,n > 0)$$$$

Lean4

theorem cardFactors_mul {m n : ℕ} (m0 : m ≠ 0) (n0 : n ≠ 0) : Ω (m * n) = Ω m + Ω n := by
  rw [cardFactors_apply, cardFactors_apply, cardFactors_apply, ← Multiset.coe_card, ← factors_eq,
    UniqueFactorizationMonoid.normalizedFactors_mul m0 n0, factors_eq, factors_eq, Multiset.card_add, Multiset.coe_card,
    Multiset.coe_card]

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