Source indexedlemma · leanprover/lean4:v4.32.0

Erdos392.factorization_prod_eq_count

PrimeNumberTheoremAnd.IEANTN.Erdos392 · PrimeNumberTheoremAnd/IEANTN/Erdos392.lean:376 to 387

Source documentation

The factorization of a product of primes at p equals the count of p in the multiset.

Exact Lean statement

lemma factorization_prod_eq_count {D : Multiset ℕ} (hD : ∀ p ∈ D, p.Prime) (p : ℕ) :
    D.prod.factorization p = D.count p

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma factorization_prod_eq_count {D : Multiset ℕ} (hD : ∀ p ∈ D, p.Prime) (p : ℕ) :    D.prod.factorization p = D.count p := by  induction D using Multiset.induction with  | empty => simp  | cons q D ih =>    have hq : q.Prime := hD q (mem_cons_self q D)    have hD' : ∀ r ∈ D, r.Prime := fun r hr ↦ hD r (Multiset.mem_cons_of_mem hr)    have hprod_ne : D.prod ≠ 0 :=      fun h ↦ by rw [Multiset.prod_eq_zero_iff] at h; exact not_prime_zero (hD' 0 h)    simp only [Multiset.prod_cons, factorization_mul hq.ne_zero hprod_ne, Finsupp.add_apply,      hq.factorization, Finsupp.single_apply, Multiset.count_cons, ih hD']    split_ifs <;> omega