English
The divisors of a product m n are the pointwise product of divisors of m and divisors of n: Divisors(m n) = Divisors(m) · Divisors(n).
Русский
Делители произведения m n равны попарному произведению делителей m и делителей n: Divisors(m n) = Divisors(m) · Divisors(n).
LaTeX
$$divisors (m * n) = divisors m * divisors n$$
Lean4
/-- The divisors of a product of natural numbers are the pointwise product of the divisors of the
factors. -/
theorem divisors_mul (m n : ℕ) : divisors (m * n) = divisors m * divisors n :=
by
ext k
simp_rw [mem_mul, mem_divisors, Nat.dvd_mul, mul_ne_zero_iff, ← exists_and_left, ← exists_and_right]
simp only [and_assoc, and_comm, and_left_comm]
