Theorems · Inductive type · commutative algebra
NormalizedGCDMonoid
(α : Type u_2) → [CommMonoidWithZero α] → Type u_2
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
- Cited by
- 159 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- CommMonoidWithZero
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.
- CommMonoidWithZerostatement · cited by 913
Cited by179
Results whose statement or proof uses this declaration.
- Finset.gcdstatement and proof · cited by 49
- Polynomial.contentstatement and proof · cited by 41
- Finset.lcmstatement and proof · cited by 37
- Multiset.gcdstatement and proof · cited by 21
- Multiset.lcmstatement and proof · cited by 20
- Polynomial.primPartstatement and proof · cited by 19
- Polynomial.eq_C_content_mul_primPartstatement and proof · cited by 14
- normalize_gcdstatement and proof · cited by 13
- Finset.dvd_lcmstatement and proof · cited by 10
- Finset.dvd_gcd_iffstatement and proof · cited by 9
- Finset.gcd_insertstatement and proof · cited by 9
- normalize_lcmstatement and proof · cited by 8