no goals
𝕜 : Type u
𝕜' : Type u'
E : Type v
F : Type w
G : Type x
inst✝¹¹ : CommRing 𝕜
n : ℕ
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : Module 𝕜 E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : TopologicalAddGroup E
inst✝⁶ : ContinuousConstSMul 𝕜 E
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module 𝕜 F
inst✝³ : TopologicalSpace F
inst✝² : TopologicalAddGroup F
inst✝¹ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
inst✝ : DecidablePred fun n => p n ≠ 0
hp : ∃ n, p n ≠ 0
⊢ order p = Nat.find hp
convert Nat.sInf_def hp