# Documentation

Mathlib.RingTheory.Prime

# Prime elements in rings #

This file contains lemmas about prime elements of commutative rings.

theorem mul_eq_mul_prime_prod {R : Type u_2} [inst : ] {α : Type u_1} [inst : ] {x : R} {y : R} {a : R} {s : } {p : αR} (hp : ∀ (i : α), i sPrime (p i)) (hx : x * y = a * Finset.prod s fun i => p i) :
t u b c, t u = s Disjoint t u a = b * c (x = b * Finset.prod t fun i => p i) y = c * Finset.prod u fun 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} [inst : ] {x : R} {y : R} {a : R} {p : R} {n : } (hp : ) (hx : x * y = a * p ^ n) :
i j b c, i + j = n a = b * c x = b * p ^ i y = c * p ^ j

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.

theorem Prime.neg {α : Type u_1} [inst : ] {p : α} (hp : ) :
Prime (-p)
theorem Prime.abs {α : Type u_1} [inst : ] [inst : ] {p : α} (hp : ) :