Theorems · Theorem · commutative algebra

factorization_pow

∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [inst_2 : NormalizationMonoid α]
  [inst_3 : DecidableEq α] {x : α} {n : ℕ}, factorization (x ^ n) = n • factorization x

For any p, the power of p in x^n is n times the power in x

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