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} [DecidableRel Dvd.dvd] (hp : Prime p) : AddValuation R PartENat

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

Equations

• multiplicity.addValuation hp = AddValuation.of (multiplicity p) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem multiplicity.addValuation_apply {R : Type u_1} [CommRing R] [IsDomain R] {p : R} [DecidableRel Dvd.dvd] {hp : Prime p} {r : R} : (multiplicity.addValuation hp) r = multiplicity p r