Documentation

Mathlib.Algebra.Group.Irreducible.Defs

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

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

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

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 * bIsUnit 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 * bIsUnit a IsUnit b
theorem addIrreducible_iff {M : Type u_1} [AddMonoid M] {p : M} :
AddIrreducible p ¬IsAddUnit p ∀ ⦃a b : M⦄, p = a + bIsAddUnit a IsAddUnit b
@[simp]
theorem not_irreducible_one {M : Type u_1} [Monoid M] :
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} :
theorem irreducible_or_factor {M : Type u_1} [Monoid M] {p : M} (hp : ¬IsUnit p) :
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