Prime elements in rings #
This file contains lemmas about prime elements of commutative rings.
theorem
mul_eq_mul_prime_prod
{R : Type u_1}
[cancel_comm_monoid_with_zero R]
{α : Type u_2}
[decidable_eq α]
{x y a : R}
{s : finset α}
{p : α → R}
(hp : ∀ (i : α), i ∈ s → prime (p i))
(hx : x * y = a * s.prod (λ (i : α), p i)) :
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
theorem
mul_eq_mul_prime_pow
{R : Type u_1}
[cancel_comm_monoid_with_zero R]
{x y a p : R}
{n : ℕ}
(hp : prime p)
(hx : x * y = a * p ^ n) :
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
.