Structures · Algebra
DecompositionMonoid
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
- Shape
- One type argument · adds primal
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- Polynomial
- Associates
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by41
- irreducible_iff_prime
- Squarefree.isRadical
- exists_dvd_and_dvd_of_dvd_mul
- DecompositionMonoid.primal
- squarefree_mul_iff
- Irreducible.prime
- IsRelPrime.prod_right
- IsRelPrime.dvd_of_dvd_mul_right
- Finset.prod_dvd_of_isRelPrime
- IsRelPrime.mul_left
- IsRelPrime.pow_left
- IsRelPrime.mul_dvd
- IsRelPrime.prod_right_iff
- Squarefree.dvd_of_squarefree_of_mul_dvd_mul_right
- IsRelPrime.pow_left_iff
- IsRelPrime.prod_left_iff
- IsRelPrime.prod_left
- isRadical_iff_squarefree_or_zero
- IsRelPrime.pow_right_iff
- Finset.squarefree_prod_of_pairwise_isCoprime
- Squarefree.dvd_of_squarefree_of_mul_dvd_mul_left
- IsRelPrime.of_prod_left
- IsRelPrime.dvd_of_dvd_mul_left
- IsRelPrime.pow_right
- IsRelPrime.mul_right
- isRadical_iff_squarefree_of_ne_zero
- IsRelPrime.mul_left_iff
- IsRelPrime.of_prod_right
- Associates.instDecompositionMonoid
- instDecompositionMonoidProd
- IsRelPrime.pow_iff
- Squarefree.dvd_pow_iff_dvd
- pairwise_isRelPrime_iff_isRelPrime_prod
- Fintype.prod_dvd_of_isRelPrime
- MulEquiv.decompositionMonoid
- IsRelPrime.pow
- IsRelPrime.mul_right_iff
- ufm_of_decomposition_of_wfDvdMonoid
- instDecompositionMonoidForall
- dvd_mul
- associates_irreducible_iff_prime
Ancestors0
No ancestors.