Documentation

Mathlib.Algebra.Prime.Defs

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

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

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

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

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

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

@[simp]

theorem not_prime_one {M : Type u_1} [CommMonoidWithZero M] :

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

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

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

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

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

Irreducible a ↔ Prime a