Theorems · Inductive type · group theory
DecompositionMonoid
(α : Type u_1) → [Semigroup α] → Prop
A monoid is a decomposition monoid if every element is primal. An integral domain whose multiplicative monoid is a decomposition monoid, is called a pre-Schreier domain; it is a Schreier domain if it is moreover integrally closed.
- Defined in
- Mathlib.Algebra.Divisibility.Basic
- Cited by
- 39 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- Semigroup
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Semigroupstatement · cited by 202
Cited by41
Results whose statement or proof uses this declaration.
- irreducible_iff_primestatement and proof · cited by 15
- Squarefree.isRadicalstatement and proof · cited by 7
- exists_dvd_and_dvd_of_dvd_mulstatement and proof · cited by 6
- DecompositionMonoid.primalstatement and proof · cited by 5
- Irreducible.primestatement and proof · cited by 4
- IsRelPrime.dvd_of_dvd_mul_rightstatement and proof · cited by 4
- IsRelPrime.prod_rightstatement and proof · cited by 4
- squarefree_mul_iffstatement and proof · cited by 4
- IsRelPrime.mul_leftstatement and proof · cited by 3
- Finset.prod_dvd_of_isRelPrimestatement and proof · cited by 3
- IsRelPrime.mul_dvdstatement and proof · cited by 2
- Squarefree.dvd_of_squarefree_of_mul_dvd_mul_rightstatement and proof · cited by 2