Structures · Algebra
StrongNormalizationMonoid
Strong normalization monoid: multiplying with normUnit gives a normal form for associated
elements. It is stronger in that it ensures the normalization map is a monoid homomorphism.
- Defined in
- Mathlib.Algebra.GCDMonoid.Basic
- Shape
- One type argument · adds normUnit_mul, normUnit_coe_units
Extends1
Extended by1
Concrete types that are instances4
- Int
- Polynomial
- PowerSeries
- Ideal
How is a type an instance?
Loading the hierarchy index…
Assumed by13
- normalize_mul
- normalizeHom
- UniqueFactorizationMonoid.prod_normalizedFactors_eq
- StrongNormalizationMonoid.normUnit_mul
- strongNormalizedGCDMonoidOfExistsGCD
- coe_normalizeHom
- StrongNormalizationMonoid.toNormalizationMonoid
- StrongNormalizationMonoid.normUnit_coe_units
- Associates.out_mul
- Polynomial.instStrongNormalizationMonoid
- strongNormalizedGCDMonoidOfExistsLCM
- instNonemptyStrongNormalizationMonoid
- UniqueFactorizationMonoid.toStrongNormalizedGCDMonoid