Theorem: LinearTopology.mem_nhds_zero_iff (DividedPowers/ForMathlib/Topology/LinearTopology.lean)

State before:
α : Type u
inst✝¹ : Ring α
inst✝ : TopologicalSpace α
hL : LinearTopology α
s : Set α
⊢ s ∈ nhds 0 ↔ ∃ i ∈ toIdealBasis.sets, ↑i ∈ nhds 0 ∧ ↑i ≤ s
Tactic:
rw [TopologicalSpace.ext_iff_nhds.mp hL.isTopology,
  hL.toIdealBasis.mem_nhds_zero_iff]
State after:
no goals