Irreducible elements in a monoid

This file defines irreducible elements of a monoid (Irreducible), as non-units that can't be written as the product of two non-units. This generalises irreducible elements of a ring. We also define the additive variant (AddIrreducible).

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

structure AddIrreducible {M : Type u_1} [AddMonoid M] (p : M) : Prop

AddIrreducible p states that p is not an additive unit and cannot be written as a sum of additive non-units.

• not_isAddUnit : ¬IsAddUnit p

  An irreducible element is not an additive unit.

• isAddUnit_or_isAddUnit ⦃a b : M⦄ : p = a + b → IsAddUnit a ∨ IsAddUnit b

  If an irreducible element can be written as a sum, then one term is an additive unit.

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_isUnit : ¬IsUnit p

  An irreducible element is not a unit.

• isUnit_or_isUnit ⦃a b : M⦄ : p = a * b → IsUnit a ∨ IsUnit b

  If an irreducible element factors, then one factor is a unit.

@[deprecated Irreducible.not_isUnit (since := "2025-04-09")]

theorem Irreducible.not_unit {M : Type u_1} [Monoid M] {p : M} (self : Irreducible p) : ¬IsUnit p

Alias of Irreducible.not_isUnit.

---

An irreducible element is not a unit.

@[deprecated Irreducible.isUnit_or_isUnit (since := "2025-04-10")]

theorem Irreducible.isUnit_or_isUnit' {M : Type u_1} [Monoid M] {p : M} (self : Irreducible p) ⦃a b : M⦄ : p = a * b → IsUnit a ∨ IsUnit b

Alias of Irreducible.isUnit_or_isUnit.

---

If an irreducible element factors, then one factor is a unit.

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

theorem addIrreducible_iff {M : Type u_1} [AddMonoid M] {p : M} : AddIrreducible p ↔ ¬IsAddUnit p ∧ ∀ ⦃a b : M⦄, p = a + b → IsAddUnit a ∨ IsAddUnit b

@[simp]

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

@[simp]

theorem not_addIrreducible_zero {M : Type u_1} [AddMonoid M] : ¬AddIrreducible 0

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

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

theorem of_irreducible_mul {M : Type u_1} [Monoid M] {a b : M} : Irreducible (a * b) → IsUnit a ∨ IsUnit b

theorem of_addIrreducible_add {M : Type u_1} [AddMonoid M] {a b : M} : AddIrreducible (a + b) → IsAddUnit a ∨ IsAddUnit b

theorem irreducible_or_factor {M : Type u_1} [Monoid M] {p : M} (hp : ¬IsUnit p) : Irreducible p ∨ ∃ (a : M), ∃ (b : M), ¬IsUnit a ∧ ¬IsUnit b ∧ p = a * b

theorem addIrreducible_or_factor {M : Type u_1} [AddMonoid M] {p : M} (hp : ¬IsAddUnit p) : AddIrreducible p ∨ ∃ (a : M), ∃ (b : M), ¬IsAddUnit a ∧ ¬IsAddUnit b ∧ p = a + b

theorem Irreducible.eq_one_or_eq_one {M : Type u_1} [Monoid M] {a b : M} [Subsingleton Mˣ] (hab : Irreducible (a * b)) : a = 1 ∨ b = 1

theorem AddIrreducible.eq_zero_or_eq_zero {M : Type u_1} [AddMonoid M] {a b : M} [Subsingleton (AddUnits M)] (hab : AddIrreducible (a + b)) : a = 0 ∨ b = 0