Prime elements in rings #
This file contains lemmas about prime elements of commutative rings.
theorem
mul_eq_mul_prime_prod
{R : Type u_1}
[CancelCommMonoidWithZero R]
{α : Type u_2}
[DecidableEq α]
{x y a : R}
{s : Finset α}
{p : α → R}
(hp : ∀ i ∈ s, Prime (p i))
(hx : x * y = a * ∏ i ∈ s, p i)
:
If x * y = a * ∏ i ∈ s, p i
where p i
is always prime, then
x
and y
can both be written as a divisor of a
multiplied by
a product over a subset of s