card_divisors_mul — Mathlib

English

If m and n are coprime natural numbers, then the number of divisors of mn equals the product of the numbers of divisors of m and n.

Русский

Если m и n взаимно просты, то число делителей mn равно произведению числа делителей m и числа делителей n.

LaTeX

$$$\text{If } \gcd(m,n)=1:\quad |(mn).divisors| = |m.divisors| \cdot |n.divisors|$$$

Lean4

theorem card_divisors_mul {m n : ℕ} (hmn : m.Coprime n) : #(m * n).divisors = #m.divisors * #n.divisors := by
  simp only [← sigma_zero_apply, isMultiplicative_sigma.map_mul_of_coprime hmn]

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