Theorems · Theorem · commutative algebra

factorization_mul

∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [inst_2 : NormalizationMonoid α]
  [inst_3 : DecidableEq α] {a b : α}, a ≠ 0 → b ≠ 0 → factorization (a * b) = factorization a + factorization b

For nonzero a and b, the power of p in a * b is the sum of the powers in a and b

Defined in

Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroUniqueFactorizationMonoidNormalizationMonoidDecidableEq