Prime and irreducible 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
• Irreducible: an irreducible 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_unit {M : Type u_1} [CommMonoidWithZero M] {p : M} (hp : Prime p) : ¬IsUnit p

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

structure Irreducible {M : Type u_1} [Monoid M] (p : M) : Prop

Irreducible p states that p is non-unit and only factors into units.

We explicitly avoid stating that p is non-zero, this would require a semiring. Assuming only a monoid allows us to reuse irreducible for associated elements.

• not_unit : ¬IsUnit p

  p is not a unit

• isUnit_or_isUnit' : ∀ (a b : M), p = a * b → IsUnit a ∨ IsUnit b

  if p factors then one factor is a unit

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

theorem Irreducible.isUnit_or_isUnit {M : Type u_1} [Monoid M] {p : M} (hp : Irreducible p) {a b : M} (h : p = a * b) : IsUnit a ∨ IsUnit b

theorem irreducible_iff {M : Type u_1} [Monoid M] {p : M} : Irreducible p ↔ ¬IsUnit p ∧ ∀ (a b : M), p = a * b → IsUnit a ∨ IsUnit b

@[simp]

theorem not_irreducible_one {M : Type u_1} [Monoid M] : ¬Irreducible 1

theorem Irreducible.ne_one {M : Type u_1} [Monoid M] {p : M} : Irreducible p → p ≠ 1

@[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 of_irreducible_mul {M : Type u_2} [Monoid M] {x y : M} : Irreducible (x * y) → IsUnit x ∨ IsUnit y

theorem irreducible_or_factor {M : Type u_2} [Monoid M] (x : M) (h : ¬IsUnit x) : Irreducible x ∨ ∃ (a : M), ∃ (b : M), ¬IsUnit a ∧ ¬IsUnit b ∧ a * b = x

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} [CancelCommMonoidWithZero M] {p : M} (hp : Prime p) : Irreducible p

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