Theorems · Theorem · commutative algebra

FiniteMultiplicity.multiplicity_pow

∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {p a : α},
  Prime p → FiniteMultiplicity p a → ∀ {k : ℕ}, multiplicity p (a ^ k) = k * multiplicity p a

Defined in

Mathlib.RingTheory.Multiplicity

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroIsCancelMulZero