Theorems · Theorem · commutative algebra

UniqueFactorizationMonoid.prod_normalizedFactors_eq

∀ {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : StrongNormalizationMonoid α]
  [inst_2 : UniqueFactorizationMonoid α] {a : α},
  a ≠ 0 → (UniqueFactorizationMonoid.normalizedFactors a).prod = normalize a

Defined in

Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors

Cited by

1 results in Mathlib

Foundations

Depth 49 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidWithZeroStrongNormalizationMonoidUniqueFactorizationMonoid