eq_of_factorization_eq — Mathlib

English

If a ≠ 0, b ≠ 0, and a.factorization p = b.factorization p for all p, then a = b.

Русский

Если a ≠ 0, b ≠ 0 и ∀ p, a.factorization p = b.factorization p, тогда a = b.

LaTeX

$$$ (\forall p, a.factorization p = b.factorization p) \Rightarrow a = b $ (under ha, hb)$$

Lean4

theorem eq_of_factorization_eq {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0)
    (h : ∀ p : ℕ, a.factorization p = b.factorization p) : a = b :=
  eq_of_perm_primeFactorsList ha hb (by simpa only [List.perm_iff_count, primeFactorsList_count_eq] using h)

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