Structures · Algebra
IsGCDMonoid
Existence of a GCDMonoid structure on a CommMonoidWithZero.
- Defined in
- Mathlib.Algebra.GCDMonoid.Basic
- Shape
- One type argument, not a structure
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Polynomial
How is a type an instance?
Loading the hierarchy index…
Assumed by14
- Polynomial.IsPrimitive.irreducible_iff_irreducible_map_fraction_map
- Polynomial.IsPrimitive.mul_map_mem_lifts_iff
- IsGCDMonoid.isPrincipal_of_exists_mul_ne_zero_isPrincipal
- Polynomial.IsPrimitive.dvd_of_fraction_map_dvd_fraction_map
- Polynomial.IsPrimitive.dvd_iff_fraction_map_dvd_fraction_map
- Polynomial.IsPrimitive.map_mul_mem_lifts_iff
- NormalizedGCDMonoid.isPrincipal_of_exists_mul_ne_zero_isPrincipal
- GCDMonoid.toIsIntegrallyClosed
- instNonemptyNormalizedGCDMonoidOfIsGCDMonoid
- IsGCDMonoid.subsingleton_classGroup
- instDecompositionMonoidOfIsGCDMonoid
- Polynomial.instIsGCDMonoid
- IsGCDMonoid.isCancelMulZero
- instSubsingletonPicOfIsDomainOfIsGCDMonoid
Ancestors0
No ancestors.