Prime elements in rings
This file contains lemmas about prime elements of commutative rings.
theorem
mul_eq_mul_prime_prod
{R : Type u_1}
[integral_domain R]
{α : Type u_2}
[decidable_eq α]
{x y a : R}
{s : finset α}
{p : α → R} :
If x * y = a * ∏ i in 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
If x * y = a * p ^ n where p is prime, then x and y can both be written
as the product of a power of p and a divisor of a.