A prime that divides no factor of a product of powers of primes #
A candidate for Mathlib.Data.List.Prime, next to Prime.not_dvd_prod and
mem_list_primes_of_dvd_prod: in a cancellative commutative monoid with zero whose only unit is
1, a prime that is none of the primes f x does not divide the product of their powers
f x ^ e x.
Main statements #
Prime.not_dvd_prod_map_pow: a prime other than the primes of a list of prime powers does not divide their product.
theorem
Prime.not_dvd_prod_map_pow
{M : Type u_1}
{α : Type u_2}
[CommMonoidWithZero M]
[IsCancelMulZero M]
[Subsingleton Mˣ]
{p : M}
(hp : Prime p)
{l : List α}
{f : α → M}
{e : α → ℕ}
(hl : ∀ (x : α), x ∈ l → Prime (f x) ∧ f x ≠ p)
:
A prime p that is none of the primes f x, for x in the list l, does not divide the
product of the powers f x ^ e x.