factorization_mul_of_coprime — Mathlib

English

Equivalent to the previous: for coprime a,b, (a·b).factorization = a.factorization + b.factorization.

Русский

Эквивалентно предшедшему: если a и b взаимно простые, тогда факторизация произведения равна сумме факторизаций.

LaTeX

$$$\\forall a,b:\\; (a \\cdot b).factorization = a.factorization + b.factorization \\quad (a,b \\neq 0,\\; \\gcd(a,b)=1)$$$

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_of_coprime {a b : ℕ} (hab : Coprime a b) :
    (a * b).factorization = a.factorization + b.factorization :=
  by
  ext q
  rw [Finsupp.add_apply, factorization_mul_apply_of_coprime hab]

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