Theorems · Inductive type · commutative algebra

Irreducible

{M : Type u_1} → [Monoid M] → 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. [Wikidata Q2989575](https://www.wikidata.org/wiki/Q2989575)

Defined in

Mathlib.Algebra.Group.Irreducible.Defs

Cited by

496 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

Monoid