Structures · Algebra
StrongNormalizedGCDMonoid
Strong normalized GCD monoid: a NormalizedGCDMonoid whose normalize function is a
monoid homomorphism.
- 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 instances5
- Int
- Nat
- Polynomial
- PUnit
- Ideal
How is a type an instance?
Loading the hierarchy index…
Assumed by16
- gcd_mul_left
- lcm_mul_left
- Finset.gcd_mul_left
- Polynomial.content_mul
- StrongNormalizedGCDMonoid.normalize_lcm
- instNormalizedGCDMonoidOfStrongNormalizedGCDMonoid
- lcm_mul_right
- gcd_mul_right
- Finset.gcd_mul_right
- Multiset.gcd_map_mul
- StrongNormalizedGCDMonoid.normalize_gcd
- StrongNormalizedGCDMonoid.toGCDMonoid
- Polynomial.content_C_mul
- Polynomial.primPart_mul
- Polynomial.instStrongNormalizedGCDMonoid
- StrongNormalizedGCDMonoid.toStrongNormalizationMonoid