mem_primeFactorsList — Mathlib

English

Let n be a nonzero natural number. A natural p belongs to the list of prime factors of n if and only if p is prime and p divides n.

Русский

Пусть n — ненулевое натуральное число. Число p принадлежит списку простых делителей n тогда и только тогда, когда p простое и p делит n.

LaTeX

$$$n \neq 0 \rightarrow p \in primeFactorsList(n) \iff (Prime(p) \land p \mid n)$$$

Lean4

theorem mem_primeFactorsList {n p} (hn : n ≠ 0) : p ∈ primeFactorsList n ↔ Prime p ∧ p ∣ n :=
  ⟨fun h => ⟨prime_of_mem_primeFactorsList h, dvd_of_mem_primeFactorsList h⟩, fun ⟨hprime, hdvd⟩ =>
    (mem_primeFactorsList_iff_dvd hn hprime).mpr hdvd⟩

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