Structures · Algebra
NormalizedGCDMonoid
Normalized GCD monoid: a cancellative CommMonoidWithZero with normalization and gcd
(greatest common divisor) and lcm (least common multiple) operations. In this setting gcd and
lcm form a bounded lattice on the associated elements where gcd is the infimum, lcm is the
supremum, 1 is bottom, and 0 is top. The type class focuses on gcd and we derive the
corresponding lcm facts from gcd.
- Defined in
- Mathlib.Algebra.GCDMonoid.Basic
- Shape
- One type argument · adds normalize_gcd, normalize_lcm
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Polynomial
- PUnit
How is a type an instance?
Loading the hierarchy index…
Assumed by167
- Finset.gcd
- Polynomial.content
- Finset.lcm
- Multiset.gcd
- Multiset.lcm
- Polynomial.primPart
- Polynomial.eq_C_content_mul_primPart
- normalize_gcd
- Finset.dvd_lcm
- Finset.gcd_insert
- Finset.dvd_gcd_iff
- normalize_lcm
- Polynomial.normalize_content
- gcd_same
- Polynomial.content_eq_zero_iff
- Finset.gcd_dvd
- Multiset.gcd_cons
- Finset.lcm_dvd
- Multiset.lcm_cons
- Finset.normalize_gcd
- Multiset.gcd_zero
- gcd_eq_normalize
- gcd_comm
- Multiset.lcm_dvd
- Polynomial.associated_content_mul
- Finset.lcm_insert
- Polynomial.content_zero
- Finset.gcd_mul_left'
- Finset.gcd_eq_zero_iff
- Polynomial.IsPrimitive.content_eq_one
- gcd_one_right
- lcm_same
- Polynomial.content_C
- Multiset.lcm_zero
- Multiset.lcm_singleton
- Polynomial.isPrimitive_iff_content_eq_one
- Finset.gcd_singleton
- lcm_eq_normalize
- Polynomial.associated_content_C_mul
- Polynomial.isPrimitive_primPart
- Multiset.gcd_dedup
- Multiset.dvd_gcd
- Polynomial.primPart_zero
- lcm_units_coe_left
- Multiset.lcm_dedup
- Multiset.normalize_gcd
- Multiset.lcm_add
- Polynomial.IsPrimitive.mul
- Polynomial.content_dvd_coeff
- Multiset.gcd_dvd