mathlib documentation

ring_theory.prime

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} :
(∀ (i : α), i sprime (p i))x * y = a * ∏ (i : α) in s, p i(∃ (t u : finset α) (b c : R), t u = s disjoint t u a = b * c x = b * ∏ (i : α) in t, p i y = c * ∏ (i : α) in u, 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} [integral_domain R] {x y a p : R} {n : } :
prime px * y = a * p ^ n(∃ (i j : ) (b 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.