no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a : α
hp : Prime p
⊢ multiplicity p (a ^ 0) = 0 • multiplicity p a
simp [one_right hp.not_unit]
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
p a : α
hp : Prime p
k : ℕ
⊢ multiplicity p (a ^ succ k) = succ k • multiplicity p a
simp [_root_.pow_succ, succ_nsmul, pow hp, multiplicity.mul hp]