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)