Structures · Algebra
GCDMonoid
GCD monoid: a cancellative CommMonoidWithZero with gcd (greatest common divisor) and
lcm (least common multiple) operations, determined up to a unit. 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 gcd, lcm, gcd_dvd_left, gcd_dvd_right, dvd_gcd, gcd_mul_lcm, lcm_zero_left, lcm_zero_right
Extends1
Extended by2
Concrete types that are instances3
- Int
- Nat
- Associates
How is a type an instance?
Loading the hierarchy index…
Assumed by94
- GCDMonoid.gcd
- GCDMonoid.lcm
- GCDMonoid.gcd_dvd_left
- GCDMonoid.gcd_dvd_right
- GCDMonoid.dvd_gcd
- dvd_lcm_left
- dvd_lcm_right
- lcm_dvd
- gcd_dvd_gcd
- lcm_dvd_lcm
- dvd_gcd_iff
- lcm_dvd_iff
- gcd_isUnit_iff
- right_div_gcd_ne_zero
- gcd_mul_left'
- Associated.gcd
- GCDMonoid.lcm_zero_left
- dvd_gcd_mul_of_dvd_mul
- GCDMonoid.gcd_mul_lcm
- exists_associated_pow_of_mul_eq_pow
- gcd_eq_zero_iff
- isUnit_gcd_of_eq_mul_gcd
- span_gcd
- GCDMonoid.lcm_zero_right
- gcd_mul_right'
- dvd_lcm_of_dvd_right
- dvd_lcm_of_dvd_left
- gcd_mul_dvd_mul_gcd
- gcd_comm'
- isCoprime_div_gcd_div_gcd
- gcd_ne_zero_of_right
- Prime.dvd_lcm
- neg_gcd'
- lcm_dvd_mul
- gcd_neg'
- gcd_one_left'
- gcd_one_right'
- exists_eq_pow_of_mul_eq_pow
- extract_gcd
- gcd_ne_zero_of_left
- Prime.dvd_or_dvd_of_dvd_lcm
- pow_dvd_of_mul_eq_pow
- Irreducible.isUnit_gcd_iff
- gcd_pow_right_dvd_pow_gcd
- isCoprime_div_gcd_div_gcd_of_gcd_ne_zero
- gcd_greatest_associated
- Polynomial.one_lt_rootMultiplicity_iff_isRoot_gcd
- gcd_zero_right'
- dvd_mul_gcd_of_dvd_mul
- gcd_dvd_iff_exists