no goals
p : ℕ
inst✝ : Fact (Nat.Prime p)
ncs : CauSeq ℤ_[p] norm
F : Polynomial ℤ_[p]
hnorm : Tendsto (fun i => ‖Polynomial.eval (↑ncs i) F‖) atTop (𝓝 0)
⊢ Tendsto (fun e => ‖Polynomial.eval (↑ncs e) F - 0‖) atTop (𝓝 0)
simpa using hnorm