Theorems · Theorem · commutative algebra

multiplicity_mul

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

Defined in

Mathlib.RingTheory.Multiplicity

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroIsCancelMulZero