mem_primeFactorsList_iff_dvd — Mathlib

English

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

Русский

Для n ≠ 0 и p простого, p ∈ primeFactorsList n эквивалентно p ∣ n.

LaTeX

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

Lean4

theorem mem_primeFactorsList_iff_dvd {n p : ℕ} (hn : n ≠ 0) (hp : Prime p) : p ∈ primeFactorsList n ↔ p ∣ n
    where
  mp h := prod_primeFactorsList hn ▸ List.dvd_prod h
  mpr
    h :=
    mem_list_primes_of_dvd_prod (prime_iff.mp hp) (fun _ h ↦ prime_iff.mp (prime_of_mem_primeFactorsList h))
      ((prod_primeFactorsList hn).symm ▸ h)

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