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 : R} {y : R} {a : R} {s : Finset α} {p : α → R} (hp : ∀ i ∈ s, Prime (p i)) (hx : x * y = a * Finset.prod s fun (i : α) => p i) : ∃ (t : Finset α) (u : Finset α) (b : R) (c : R), 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} [CancelCommMonoidWithZero R] {x : R} {y : R} {a : R} {p : R} {n : ℕ} (hp : Prime p) (hx : x * y = a * p ^ n) : ∃ (i : ℕ) (j : ℕ) (b : R) (c : R), 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} [CommRing α] {p : α} (hp : Prime p) : Prime (-p)

theorem Prime.abs {α : Type u_1} [CommRing α] [LinearOrder α] {p : α} (hp : Prime p) : Prime |p|