Prime elements in rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file contains lemmas about prime elements of commutative rings.

source

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)) :

∃ (t u : finset α) (b c : R), t ∪ u = s ∧ disjoint t u ∧ a = b * c ∧ x = b * t.prod (λ (i : α), p i) ∧ y = c * u.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

source

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) :

∃ (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.

source

theorem prime.neg {α : Type u_1} [comm_ring α] {p : α} (hp : prime p) :

prime (-p)

source

theorem prime.abs {α : Type u_1} [comm_ring α] [linear_order α] {p : α} (hp : prime p) :

prime |p|