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.

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)

theorem Prime.ne_zero {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) : p ≠ 0

theorem Prime.not_isUnit {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) : ¬IsUnit p

@[deprecated Prime.not_isUnit (since := "2026-08-02")]

theorem Prime.not_unit {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) : ¬IsUnit p

Alias of Prime.not_isUnit.

theorem Prime.not_dvd_one {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) : ¬p ∣ 1

theorem Prime.ne_one {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) : p ≠ 1

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

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

theorem Prime.isPrimal {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) : IsPrimal p

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

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

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

@[simp]

theorem not_prime_zero {M : Type u_1} [CommMonoidWithZero M] : ¬Prime 0

@[simp]

theorem not_prime_one {M : Type u_1} [CommMonoidWithZero M] : ¬Prime 1

theorem Irreducible.not_dvd_isUnit {M : Type u_1} [CommMonoid M] {p u : M} (hp : Irreducible p) (hu : IsUnit u) : ¬p ∣ u

theorem Irreducible.not_dvd_one {M : Type u_1} [CommMonoid M] {p : M} (hp : Irreducible p) : ¬p ∣ 1

theorem Irreducible.not_dvd_unit {M : Type u_1} [CommMonoid M] {p : M} (u : Mˣ) (hp : Irreducible p) : ¬p ∣ ↑u

theorem Irreducible.isUnit_of_mul_self_dvd {M : Type u_1} [CommMonoid M] {p a : M} (hp : Irreducible p) (ha : a * a ∣ p) : IsUnit a

@[simp]

theorem not_irreducible_zero {M : Type u_1} [MonoidWithZero M] : ¬Irreducible 0

theorem Irreducible.ne_zero {M : Type u_1} [MonoidWithZero M] {p : M} : Irreducible p → p ≠ 0

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.

theorem Irreducible.dvd_comm {M : Type u_1} [Monoid M] {p q : M} (hp : Irreducible p) (hq : Irreducible q) : p ∣ q ↔ q ∣ p

theorem Irreducible.prime_of_isPrimal {M : Type u_1} [CommMonoidWithZero M] {a : M} (irr : Irreducible a) (primal : IsPrimal a) : Prime a

theorem Irreducible.prime {M : Type u_1} [CommMonoidWithZero M] [DecompositionMonoid M] {a : M} (irr : Irreducible a) : Prime a

theorem Prime.irreducible {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] {p : M} (hp : Prime p) : Irreducible p

theorem irreducible_iff_prime {M : Type u_1} [CommMonoidWithZero M] [IsCancelMulZero M] [DecompositionMonoid M] {a : M} : Irreducible a ↔ Prime a