eq_of_perm_primeFactorsList — Mathlib

English

For hn: n ≠ 0 and p prime, p ∈ primeFactorsList n iff p ∣ n.

Русский

Для hn: n ≠ 0 и p простое, p ∈ primeFactorsList n тогда и только тогда, когда p делит n.

LaTeX

$$$ \forall {n,p}, n \neq 0 \to \text{Prime}(p) \Rightarrow (p \in \text{primeFactorsList}(n) \iff p \mid n) $$$

Lean4

theorem eq_of_perm_primeFactorsList {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) (h : a.primeFactorsList ~ b.primeFactorsList) :
    a = b := by simpa [prod_primeFactorsList ha, prod_primeFactorsList hb] using List.Perm.prod_eq h

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