mem_list_primes_of_dvd_prod — Mathlib

English

Let p be prime and L a list of primes; if p divides the product L.prod, then p belongs to L.

Русский

Пусть p простое и L — список простых чисел; если p делит произведение L.prod, то p ∈ L.

LaTeX

$$$\forall {M}, [\text{CancelCommMonoidWithZero } M] (pp : Prime p) (hL : ∀ q \in L, Prime q) (hpL : p \mid L.prod) : p \in L$$$

Lean4

theorem mem_list_primes_of_dvd_prod {p : M} (hp : Prime p) {L : List M} (hL : ∀ q ∈ L, Prime q) (hpL : p ∣ L.prod) :
    p ∈ L := by
  obtain ⟨x, hx1, hx2⟩ := hp.dvd_prod_iff.mp hpL
  rwa [(prime_dvd_prime_iff_eq hp (hL x hx1)).mp hx2]

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