Nat.divisors_mul

theorem Nat.divisors_mul : ∀ (m n : ℕ), (m * n).divisors = m.divisors * n.divisors

This theorem states that the divisors of the product of two natural numbers are obtained by taking the pointwise product of the divisors of the individual numbers. In other words, if you have two natural numbers, `m` and `n`, and you find all the divisors of `m` and `n` separately, then create the set of all possible products of a divisor of `m` and a divisor of `n`, that set is exactly the same as the set of all divisors of `m * n`.

More concisely: The set of divisors of the product of two natural numbers is the set of products of a divisor of each factor.