English
Let m, n be natural numbers and f a function from primes to a commutative monoid β. Then the product over primes of f(p) taken with respect to gcd(m, n) and with respect to m n satisfies the multiplicative identity: ∏ p | gcd(m, n) f(p) · ∏ p | m n f(p) = ∏ p | m f(p) · ∏ p | n f(p). In words, the prime-factor product is multiplicative with respect to gcd and multiplication.
Русский
Пусть m, n — натуральные числа и f : ℕ → β, где β — коммутативный моноид. Тогда произведение по простым делителям gcd(m, n) и по простым делителям m n удовлетворяет тождеству: ∏ p | gcd(m, n) f(p) · ∏ p | m n f(p) = ∏ p | m f(p) · ∏ p | n f(p).
LaTeX
$$$ (m \gcd n).primeFactors.prod f \\cdot (m \cdot n).primeFactors.prod f = m.primeFactors.prod f \\cdot n.primeFactors.prod f $$$
Lean4
@[to_additive sum_primeFactors_gcd_add_sum_primeFactors_mul]
theorem prod_primeFactors_gcd_mul_prod_primeFactors_mul {β : Type*} [CommMonoid β] (m n : ℕ) (f : ℕ → β) :
(m.gcd n).primeFactors.prod f * (m * n).primeFactors.prod f = m.primeFactors.prod f * n.primeFactors.prod f :=
by
obtain rfl | hm₀ := eq_or_ne m 0
· simp
obtain rfl | hn₀ := eq_or_ne n 0
· simp
· rw [primeFactors_mul hm₀ hn₀, primeFactors_gcd hm₀ hn₀, mul_comm, Finset.prod_union_inter]
