# Prime elements #

In this file we define the predicate `Prime p` saying that an element of a commutative monoid with zero is prime. Namely, `Prime p` means that `p` isn't zero, it isn't a unit, and `p ∣ a * b → p ∣ a ∨ p ∣ b` for all `a`, `b`;

In decomposition monoids (e.g., `ℕ`, `ℤ`), this predicate is equivalent to `Irreducible` (see `irreducible_iff_prime`), however this is not true in general.

## Main definitions #

- `Prime`: a prime element of a commutative monoid with zero

## Main results #

- `irreducible_iff_prime`: the two definitions are equivalent in a decomposition monoid.

source
def Prime {M : Type u_1} [CommMonoidWithZero M] (p : M) :
Prop

An element `p` of a commutative monoid with zero (e.g., a ring) is called prime, if it's not zero, not a unit, and `p ∣ a * b → p ∣ a ∨ p ∣ b` for all `a`, `b`.

Equations

- Prime p = (p ≠ 0 ∧ ¬IsUnit p ∧ ∀ (a b : M), p ∣ a * b → p ∣ a ∨ p ∣ b)

Instances For

source
theorem Prime.ne_zero {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) :
p ≠ 0
source
theorem Prime.not_unit {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) :
¬IsUnit p
source
theorem Prime.not_dvd_one {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) :
¬p ∣ 1
source
theorem Prime.ne_one {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) :
p ≠ 1
source
theorem Prime.dvd_or_dvd {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) {a b : M} (h : p ∣ a * b) :
p ∣ a ∨ p ∣ b
source
theorem Prime.dvd_mul {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) {a b : M} :
p ∣ a * b ↔ p ∣ a ∨ p ∣ b
source
theorem Prime.isPrimal {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) :
IsPrimal p
source
theorem Prime.not_dvd_mul {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) {a b : M} (ha : ¬p ∣ a) (hb : ¬p ∣ b) :
¬p ∣ a * b
source
theorem Prime.dvd_of_dvd_pow {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) {a : M} {n : ℕ} (h : p ∣ a ^ n) :
p ∣ a
source
theorem Prime.dvd_pow_iff_dvd {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) {a : M} {n : ℕ} (hn : n ≠ 0) :
p ∣ a ^ n ↔ p ∣ a
source
@[simp]
theorem not_prime_zero {M : Type u_1} [CommMonoidWithZero M] :
¬Prime 0
source
@[simp]
theorem not_prime_one {M : Type u_1} [CommMonoidWithZero M] :
¬Prime 1
source
theorem Irreducible.not_dvd_isUnit {M : Type u_1} [CommMonoid M] {p u : M} (hp : Irreducible p) (hu : IsUnit u) :
¬p ∣ u
source
theorem Irreducible.not_dvd_one {M : Type u_1} [CommMonoid M] {p : M} (hp : Irreducible p) :
¬p ∣ 1
source
theorem Irreducible.not_dvd_unit {M : Type u_1} [CommMonoid M] {p : M} (u : M ˣ) (hp : Irreducible p) :
¬p ∣ ↑u
source
@[simp]
theorem not_irreducible_zero {M : Type u_1} [MonoidWithZero M] :
¬Irreducible 0
source
theorem Irreducible.ne_zero {M : Type u_1} [MonoidWithZero M] {p : M} :
Irreducible p → p ≠ 0
source
theorem Irreducible.dvd_symm {M : Type u_1} [Monoid M] {p q : M} (hp : Irreducible p) (hq : Irreducible q) :
p ∣ q → q ∣ p

If `p` and `q` are irreducible, then `p ∣ q` implies `q ∣ p`.

source
theorem Irreducible.dvd_comm {M : Type u_1} [Monoid M] {p q : M} (hp : Irreducible p) (hq : Irreducible q) :
p ∣ q ↔ q ∣ p
source
theorem Irreducible.prime_of_isPrimal {M : Type u_1} [CommMonoidWithZero M] {a : M} (irr : Irreducible a) (primal : IsPrimal a) :
Prime a
source
theorem Irreducible.prime {M : Type u_1} [CommMonoidWithZero M] [DecompositionMonoid M] {a : M} (irr : Irreducible a) :
Prime a
source
theorem Prime.irreducible {M : Type u_1} [CancelCommMonoidWithZero M] {p : M} (hp : Prime p) :
Irreducible p
source
theorem irreducible_iff_prime {M : Type u_1} [CancelCommMonoidWithZero M] [DecompositionMonoid M] {a : M} :
Irreducible a ↔ Prime a