p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Part.get (multiplicity p p) (_ : multiplicity.Finite p p) = 1
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ padicValNat p p = 1
rw [padicValNat_def (@Fact.out p.Prime).pos]
no goals
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Part.get (multiplicity p p) (_ : multiplicity.Finite p p) = 1
simp