Documentation

Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Unique factorization and normalization #

Main definitions #

@[simp]

An arbitrary choice of factors of x : M is exactly the (unique) normalized set of factors, if M has a trivial group of units.

@[deprecated UniqueFactorizationMonoid.prod_normalizedFactors (since := "2024-12-04")]

Alias of UniqueFactorizationMonoid.prod_normalizedFactors.

@[deprecated UniqueFactorizationMonoid.zero_notMem_normalizedFactors (since := "2025-05-23")]

Alias of UniqueFactorizationMonoid.zero_notMem_normalizedFactors.

If the monoid equiv f : α ≃* β commutes with normalize then, for a : α, it yields a bijection between the normalizedFactors of a and of f a.

Equations
@[simp]
@[simp]
theorem UniqueFactorizationMonoid.normalizedFactorsEquiv_symm_apply {α : Type u_1} [CancelCommMonoidWithZero α] [NormalizationMonoid α] [UniqueFactorizationMonoid α] {β : Type u_2} [CancelCommMonoidWithZero β] [NormalizationMonoid β] [UniqueFactorizationMonoid β] {F : Type u_3} [EquivLike F α β] [MulEquivClass F α β] {f : F} [DecidableEq α] (he : ∀ (x : α), normalize (f x) = f (normalize x)) {a : α} {q : β} (hq : q normalizedFactors (f a)) :
((normalizedFactorsEquiv he a).symm q, hq) = (↑f).symm q

Noncomputably defines a normalizationMonoid structure on a UniqueFactorizationMonoid.

Equations
  • One or more equations did not get rendered due to their size.