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
⊢ order p = 0 ↔ p = 0 ∨ p 0 ≠ 0
simpa [order, Nat.sInf_eq_zero, FormalMultilinearSeries.ext_iff, eq_empty_iff_forall_not_mem]
  using or_comm