factorization_eq_of_coprime_right

English

If two positive integers have the same factorization at every prime, then they are equal; conversely equal numbers have identical factorizations.

Русский

Если две положительные числа имеют одинаковую факторизацию по каждому простому, то они равны; наоборот, равные числа имеют идентичную факторизацию.

LaTeX

$$$ a, b > 0 \; \land \; (\forall p, a.factorization p = b.factorization p) \Rightarrow a = b $$$

Lean4

/-- If `p` is a prime factor of `b` then the power of `p` in `b` is the same that in `a * b`,
for any `a` coprime to `b`. -/
theorem factorization_eq_of_coprime_right {p a b : ℕ} (hab : Coprime a b) (hpb : p ∈ b.primeFactorsList) :
    (a * b).factorization p = b.factorization p := by
  rw [mul_comm]
  exact factorization_eq_of_coprime_left (coprime_comm.mp hab) hpb

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