English
If a and b are coprime and p is a prime factor of b, then the exponent of p in a b equals the exponent of p in b.
Русский
Если a и b взаимно просты и p — простой делитель b, то показатель p в ab равен показателю p в b.
LaTeX
$$$ (a \cdot b).factorization p = b.factorization p \quad$ при $\gcd(a,b)=1$ и $p \in b.primeFactorsList$$$
Lean4
/-- If `p` is a prime factor of `a` then the power of `p` in `a` is the same that in `a * b`,
for any `b` coprime to `a`. -/
theorem factorization_eq_of_coprime_left {p a b : ℕ} (hab : Coprime a b) (hpa : p ∈ a.primeFactorsList) :
(a * b).factorization p = a.factorization p := by
rw [factorization_mul_apply_of_coprime hab, ← primeFactorsList_count_eq, ← primeFactorsList_count_eq,
count_eq_zero_of_not_mem (coprime_primeFactorsList_disjoint hab hpa), add_zero]
