sum_divisors_mul — Mathlib

English

If m and n are coprime then the sum of divisors function is multiplicative: sum_{d|mn} d = (sum_{d|m} d) (sum_{d|n} d).

Русский

Если m и n взаимно просты, то сумма делителей является мультипликативной: сумма по делителям mn равна произведению сумм по делителям m и n.

LaTeX

$$$\gcd(m,n)=1 \Rightarrow \sum_{d|mn} d = \left(\sum_{d|m} d\right) \left(\sum_{d|n} d\right)$$$

Lean4

theorem sum_divisors_mul {m n : ℕ} (hmn : m.Coprime n) :
    ∑ d ∈ (m * n).divisors, d = (∑ d ∈ m.divisors, d) * ∑ d ∈ n.divisors, d := by
  simp only [← sigma_one_apply, isMultiplicative_sigma.map_mul_of_coprime hmn]

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