multiplicity of a prime in an integral domain as an additive valuation

noncomputable def multiplicity_addValuation {R : Type u_1} [CommRing R] [IsDomain R] {p : R} (hp : Prime p) : AddValuation R ℕ∞

multiplicity of a prime in an integral domain as an additive valuation to ℕ∞.

Equations

• multiplicity_addValuation hp = AddValuation.of (emultiplicity p) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem multiplicity_addValuation_apply {R : Type u_1} [CommRing R] [IsDomain R] {p : R} {hp : Prime p} {r : R} : (multiplicity_addValuation hp) r = emultiplicity p r