Mathlib.Algebra.Prime.Defs

Module docstring

{"# 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. "}

Prime definition

(p : M) : Prop

Full source

/-- 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`. -/
def Prime (p : M) : Prop :=
  p ≠ 0p ≠ 0 ∧ ¬IsUnit p ∧ ∀ a b, p ∣ a * b → p ∣ a ∨ p ∣ b

Prime element in a commutative monoid with zero

Informal description

An element $ p $ of a commutative monoid with zero $ M $ is called *prime* if it satisfies the following three conditions: 1. $ p $ is not zero, 2. $ p $ is not a unit (i.e., there is no multiplicative inverse for $ p $ in $ M $), 3. For any elements $ a, b \in M $, if $ p $ divides the product $ a \cdot b $, then $ p $ divides $ a $ or $ p $ divides $ b $.

Prime.ne_zero theorem

: p ≠ 0

Full source

theorem ne_zero : p ≠ 0 :=
  hp.1

Prime elements are nonzero

Informal description

A prime element $p$ in a commutative monoid with zero is nonzero, i.e., $p \neq 0$.

Prime.not_unit theorem

: ¬IsUnit p

Full source

theorem not_unit : ¬IsUnit p :=
  hp.2.1

Prime Elements Are Not Units

Informal description

A prime element $p$ in a commutative monoid with zero is not a unit, i.e., there does not exist an element $u$ such that $p \cdot u = 1$ and $u \cdot p = 1$.

Prime.not_dvd_one theorem

: ¬p ∣ 1

Full source

theorem not_dvd_one : ¬p ∣ 1 :=
  mt (isUnit_of_dvd_one ·) hp.not_unit

Prime Elements Do Not Divide One

Informal description

A prime element $p$ in a commutative monoid with zero does not divide the multiplicative identity $1$, i.e., $\neg (p \mid 1)$.

Prime.ne_one theorem

: p ≠ 1

Full source

theorem ne_one : p ≠ 1 := fun h => hp.2.1 (h.symm ▸ isUnit_one)

Prime elements are not equal to one

Informal description

A prime element $p$ in a commutative monoid with zero is not equal to the multiplicative identity $1$.

Prime.dvd_or_dvd theorem

{a b : M} (h : p ∣ a * b) : p ∣ a ∨ p ∣ b

Full source

theorem dvd_or_dvd {a b : M} (h : p ∣ a * b) : p ∣ ap ∣ a ∨ p ∣ b :=
  hp.2.2 a b h

Prime Element Divisibility Property: $p \mid a b \implies p \mid a \lor p \mid b$

Informal description

Let $p$ be a prime element in a commutative monoid with zero $M$. For any elements $a, b \in M$, if $p$ divides the product $a \cdot b$, then $p$ divides $a$ or $p$ divides $b$.

Prime.dvd_mul theorem

{a b : M} : p ∣ a * b ↔ p ∣ a ∨ p ∣ b

Full source

theorem dvd_mul {a b : M} : p ∣ a * bp ∣ a * b ↔ p ∣ a ∨ p ∣ b :=
  ⟨hp.dvd_or_dvd, (Or.elim · (dvd_mul_of_dvd_left · _) (dvd_mul_of_dvd_right · _))⟩

Prime Divisibility Criterion: $p \mid ab \leftrightarrow p \mid a \lor p \mid b$

Informal description

Let $p$ be a prime element in a commutative monoid with zero $M$. For any elements $a, b \in M$, $p$ divides the product $a \cdot b$ if and only if $p$ divides $a$ or $p$ divides $b$.

Prime.isPrimal theorem

: IsPrimal p

Full source

theorem isPrimal : IsPrimal p := fun _a _b dvd ↦ (hp.dvd_or_dvd dvd).elim
  (fun h ↦ ⟨p, 1, h, one_dvd _, (mul_one p).symm⟩) fun h ↦ ⟨1, p, one_dvd _, h, (one_mul p).symm⟩

Prime Elements are Primal

Informal description

A prime element $p$ in a commutative monoid with zero is primal, meaning that for any elements $a, b$ in the monoid, if $p$ divides the product $a \cdot b$, then there exist elements $p_1, p_2$ such that $p_1$ divides $a$, $p_2$ divides $b$, and $p = p_1 \cdot p_2$.

Prime.not_dvd_mul theorem

{a b : M} (ha : ¬p ∣ a) (hb : ¬p ∣ b) : ¬p ∣ a * b

Full source

theorem not_dvd_mul {a b : M} (ha : ¬ p ∣ a) (hb : ¬ p ∣ b) : ¬ p ∣ a * b :=
  hp.dvd_mul.not.mpr <| not_or.mpr ⟨ha, hb⟩

Prime Element Does Not Divide Product of Non-Divisible Elements

Informal description

Let $p$ be a prime element in a commutative monoid with zero $M$. For any elements $a, b \in M$, if $p$ does not divide $a$ and $p$ does not divide $b$, then $p$ does not divide the product $a \cdot b$.

Prime.dvd_of_dvd_pow theorem

{a : M} {n : ℕ} (h : p ∣ a ^ n) : p ∣ a

Full source

theorem dvd_of_dvd_pow {a : M} {n : ℕ} (h : p ∣ a ^ n) : p ∣ a := by
  induction n with
  | zero =>
    rw [pow_zero] at h
    have := isUnit_of_dvd_one h
    have := not_unit hp
    contradiction
  | succ n ih =>
    rw [pow_succ'] at h
    rcases dvd_or_dvd hp h with dvd_a | dvd_pow
    · assumption
    · exact ih dvd_pow

Prime Element Divisibility Property for Powers: $p \mid a^n \implies p \mid a$

Informal description

Let $p$ be a prime element in a commutative monoid with zero $M$. For any element $a \in M$ and natural number $n$, if $p$ divides $a^n$, then $p$ divides $a$.

Prime.dvd_pow_iff_dvd theorem

{a : M} {n : ℕ} (hn : n ≠ 0) : p ∣ a ^ n ↔ p ∣ a

Full source

theorem dvd_pow_iff_dvd {a : M} {n : ℕ} (hn : n ≠ 0) : p ∣ a ^ np ∣ a ^ n ↔ p ∣ a :=
  ⟨hp.dvd_of_dvd_pow, (dvd_pow · hn)⟩

Prime Divisibility Criterion for Powers: $p \mid a^n \leftrightarrow p \mid a$ for $n \neq 0$

Informal description

Let $p$ be a prime element in a commutative monoid with zero $M$. For any element $a \in M$ and nonzero natural number $n$, $p$ divides $a^n$ if and only if $p$ divides $a$. In other words, $p \mid a^n \leftrightarrow p \mid a$ for $n \neq 0$.

not_prime_zero theorem

: ¬Prime (0 : M)

Full source

@[simp]
theorem not_prime_zero : ¬Prime (0 : M) := fun h => h.ne_zero rfl

Zero is not prime in a commutative monoid with zero

Informal description

The zero element $0$ in a commutative monoid with zero $M$ is not a prime element.

not_prime_one theorem

: ¬Prime (1 : M)

Full source

@[simp]
theorem not_prime_one : ¬Prime (1 : M) := fun h => h.not_unit isUnit_one

One is Not Prime in a Commutative Monoid with Zero

Informal description

The multiplicative identity element $1$ in a commutative monoid with zero $M$ is not a prime element.

Irreducible.not_dvd_one theorem

[CommMonoid M] {p : M} (hp : Irreducible p) : ¬p ∣ 1

Full source

theorem Irreducible.not_dvd_one [CommMonoid M] {p : M} (hp : Irreducible p) : ¬p ∣ 1 :=
  mt (isUnit_of_dvd_one ·) hp.not_isUnit

Irreducible Elements Do Not Divide One

Informal description

Let $M$ be a commutative monoid and $p \in M$ be an irreducible element. Then $p$ does not divide the multiplicative identity $1$, i.e., $\neg (p \mid 1)$.

not_irreducible_zero theorem

[MonoidWithZero M] : ¬Irreducible (0 : M)

Full source

@[simp]
theorem not_irreducible_zero [MonoidWithZero M] : ¬Irreducible (0 : M)
  | ⟨hn0, h⟩ =>
    have : IsUnit (0 : M) ∨ IsUnit (0 : M) := h (mul_zero 0).symm
    this.elim hn0 hn0

Zero is Not Irreducible in a Monoid with Zero

Informal description

In any monoid with zero $M$, the zero element $0$ is not irreducible.

Irreducible.ne_zero theorem

[MonoidWithZero M] : ∀ {p : M}, Irreducible p → p ≠ 0

Full source

theorem Irreducible.ne_zero [MonoidWithZero M] : ∀ {p : M}, Irreducible p → p ≠ 0
  | _, hp, rfl => not_irreducible_zero hp

Nonzero Property of Irreducible Elements in a Monoid with Zero

Informal description

In any monoid with zero $M$, if an element $p$ is irreducible, then $p$ is not equal to the zero element, i.e., $p \neq 0$.

Irreducible.dvd_symm theorem

[Monoid M] {p q : M} (hp : Irreducible p) (hq : Irreducible q) : p ∣ q → q ∣ p

Full source

/-- If `p` and `q` are irreducible, then `p ∣ q` implies `q ∣ p`. -/
theorem Irreducible.dvd_symm [Monoid M] {p q : M} (hp : Irreducible p) (hq : Irreducible q) :
    p ∣ q → q ∣ p := by
  rintro ⟨q', rfl⟩
  rw [IsUnit.mul_right_dvd (Or.resolve_left (of_irreducible_mul hq) hp.not_isUnit)]

Symmetry of Divisibility for Irreducible Elements in a Monoid

Informal description

For any irreducible elements $p$ and $q$ in a monoid $M$, if $p$ divides $q$, then $q$ divides $p$.

Irreducible.dvd_comm theorem

[Monoid M] {p q : M} (hp : Irreducible p) (hq : Irreducible q) : p ∣ q ↔ q ∣ p

Full source

theorem Irreducible.dvd_comm [Monoid M] {p q : M} (hp : Irreducible p) (hq : Irreducible q) :
    p ∣ qp ∣ q ↔ q ∣ p :=
  ⟨hp.dvd_symm hq, hq.dvd_symm hp⟩

Divisibility Symmetry for Irreducible Elements in a Monoid

Informal description

For any irreducible elements $p$ and $q$ in a monoid $M$, $p$ divides $q$ if and only if $q$ divides $p$.

Irreducible.prime_of_isPrimal theorem

{a : M} (irr : Irreducible a) (primal : IsPrimal a) : Prime a

Full source

theorem Irreducible.prime_of_isPrimal {a : M}
    (irr : Irreducible a) (primal : IsPrimal a) : Prime a :=
  ⟨irr.ne_zero, irr.not_isUnit, fun a b dvd ↦ by
    obtain ⟨d₁, d₂, h₁, h₂, rfl⟩ := primal dvd
    exact (of_irreducible_mul irr).symm.imp (·.mul_right_dvd.mpr h₁) (·.mul_left_dvd.mpr h₂)⟩

Primal Irreducible Elements are Prime in a Commutative Monoid with Zero

Informal description

Let $M$ be a commutative monoid with zero and let $a \in M$ be an irreducible element. If $a$ is primal (i.e., for any $b, c \in M$ such that $a$ divides $b \cdot c$, there exist $a_1, a_2 \in M$ such that $a_1$ divides $b$, $a_2$ divides $c$, and $a = a_1 \cdot a_2$), then $a$ is a prime element.

Irreducible.prime theorem

[DecompositionMonoid M] {a : M} (irr : Irreducible a) : Prime a

Full source

theorem Irreducible.prime [DecompositionMonoid M] {a : M} (irr : Irreducible a) : Prime a :=
  irr.prime_of_isPrimal (DecompositionMonoid.primal a)

Irreducible elements are prime in a decomposition monoid

Informal description

Let $M$ be a decomposition monoid. For any irreducible element $a \in M$, $a$ is a prime element.

Prime.irreducible theorem

(hp : Prime p) : Irreducible p

Full source

protected theorem Prime.irreducible (hp : Prime p) : Irreducible p :=
  ⟨hp.not_unit, fun a b ↦ by
    rintro rfl
    exact (hp.dvd_or_dvd dvd_rfl).symm.imp
      (isUnit_of_dvd_one <| (mul_dvd_mul_iff_right <| right_ne_zero_of_mul hp.ne_zero).mp <|
        dvd_mul_of_dvd_right · _)
      (isUnit_of_dvd_one <| (mul_dvd_mul_iff_left <| left_ne_zero_of_mul hp.ne_zero).mp <|
        dvd_mul_of_dvd_left · _)⟩

Prime Elements are Irreducible in a Commutative Monoid with Zero

Informal description

Let $p$ be an element of a commutative monoid with zero $M$. If $p$ is prime (i.e., $p \neq 0$, $p$ is not a unit, and for all $a, b \in M$, $p \mid a \cdot b$ implies $p \mid a$ or $p \mid b$), then $p$ is irreducible (i.e., $p$ is not a unit and any factorization $p = a \cdot b$ implies that either $a$ or $b$ is a unit).

irreducible_iff_prime theorem

[DecompositionMonoid M] {a : M} : Irreducible a ↔ Prime a

Full source

theorem irreducible_iff_prime [DecompositionMonoid M] {a : M} : IrreducibleIrreducible a ↔ Prime a :=
  ⟨Irreducible.prime, Prime.irreducible⟩

Equivalence of Irreducible and Prime Elements in a Decomposition Monoid

Informal description

Let $M$ be a decomposition monoid. For any element $a \in M$, $a$ is irreducible if and only if $a$ is prime. That is, the following are equivalent: 1. $a$ is irreducible (i.e., $a$ is not a unit and any factorization $a = b \cdot c$ implies that either $b$ or $c$ is a unit). 2. $a$ is prime (i.e., $a \neq 0$, $a$ is not a unit, and for all $b, c \in M$, $a \mid b \cdot c$ implies $a \mid b$ or $a \mid c$).