Structures · Algebra
NormalizationMonoid
Normalization monoid: multiplying with normUnit gives a normal form for associated
elements.
- Defined in
- Mathlib.Algebra.GCDMonoid.Basic
- Shape
- One type argument · adds normUnit, normUnit_zero, normUnit_one, normUnit_mul_units
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances1
- Polynomial
How is a type an instance?
Loading the hierarchy index…
Assumed by183
- UniqueFactorizationMonoid.normalizedFactors
- normalize
- UniqueFactorizationMonoid.radical
- NormalizationMonoid.normUnit
- UniqueFactorizationMonoid.primeFactors
- UniqueFactorizationMonoid.prod_normalizedFactors
- UniqueFactorizationMonoid.prime_of_normalized_factor
- UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors
- normalize_zero
- dvd_antisymm_of_normalize_eq
- Associates.out
- UniqueFactorizationMonoid.irreducible_of_normalized_factor
- UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors
- UniqueFactorizationMonoid.normalizedFactors_zero
- EuclideanDomain.divRadical
- UniqueFactorizationMonoid.dvd_iff_normalizedFactors_le_normalizedFactors
- associated_normalize
- UniqueFactorizationMonoid.normalizedFactors_mul
- normalize_one
- UniqueFactorizationMonoid.normalizedFactors_irreducible
- normalize_eq_one
- factorization
- UniqueFactorizationMonoid.normalize_normalized_factor
- UniqueFactorizationMonoid.exists_mem_normalizedFactors_of_dvd
- normalize_apply
- UniqueFactorizationMonoid.normalizedFactors_pow
- UniqueFactorizationMonoid.normalizedFactors_one
- UniqueFactorizationMonoid.radical_dvd_self
- UniqueFactorizationMonoid.radical_zero
- normalize_associated
- Polynomial.coe_normUnit
- UniqueFactorizationMonoid.radical.congr_simp
- Ideal.normalizedFactorsEquivSpanNormalizedFactors
- UniqueFactorizationMonoid.radical_ne_zero
- UniqueFactorizationMonoid.radical_one
- UniqueFactorizationMonoid.normalizedFactors.congr_simp
- UniqueFactorizationMonoid.primeFactors_radical
- normalize_eq_normalize
- Associated.eq_of_normalized
- normalize_eq_normalize_iff_associated
- EuclideanDomain.radical_mul_divRadical
- UniqueFactorizationMonoid.zero_notMem_normalizedFactors
- normalize_idem
- UniqueFactorizationMonoid.radical_eq_of_associated
- UniqueFactorizationMonoid.primeFactors_zero
- NormalizationMonoid.normUnit_one
- UniqueFactorizationMonoid.radical_pow
- UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors
- UniqueFactorizationMonoid.radical_of_isUnit
- NormalizationMonoid.normUnit_zero
Ancestors0
No ancestors.