factorization_mul_apply_of_coprime

English

If a and b are coprime, then for every p, (a·b).factorization p = a.factorization p + b.factorization p.

Русский

Если a и b взаимно простые, то для любого p выполняется факторизация(a b) по p равна сумме факторизаций.

LaTeX

$$$\\forall p:\\; (a \\cdot b).factorization(p) = a.factorization(p) + b.factorization(p) \\quad (\\text{Coprime}(a,b))$$$

Lean4

/-- For coprime `a` and `b`, the power of `p` in `a * b` is the sum of the powers in `a` and `b` -/
theorem factorization_mul_apply_of_coprime {p a b : ℕ} (hab : Coprime a b) :
    (a * b).factorization p = a.factorization p + b.factorization p := by
  simp only [← primeFactorsList_count_eq, perm_iff_count.mp (perm_primeFactorsList_mul_of_coprime hab), count_append]

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