M : Type ?u.171187
α : Type u_1
β : Type ?u.171193
Γ : Type ?u.171196
inst✝⁷ : Group Γ
T : Type ?u.171202
inst✝⁶ : TopologicalSpace T
inst✝⁵ : MulAction Γ T
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : AddMonoid α
inst✝² : DistribMulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
s : Set α
c : G₀
hc : c ≠ 0
⊢ c • s ∈ 𝓝 0 ↔ c • s ∈ 𝓝 (c • 0)
M : Type ?u.171187
α : Type u_1
β : Type ?u.171193
Γ : Type ?u.171196
inst✝⁷ : Group Γ
T : Type ?u.171202
inst✝⁶ : TopologicalSpace T
inst✝⁵ : MulAction Γ T
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : AddMonoid α
inst✝² : DistribMulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
s : Set α
c : G₀
hc : c ≠ 0
⊢ c • s ∈ 𝓝 0 ↔ s ∈ 𝓝 0
refine' Iff.trans _ (set_smul_mem_nhds_smul_iff hc)
no goals
M : Type ?u.171187
α : Type u_1
β : Type ?u.171193
Γ : Type ?u.171196
inst✝⁷ : Group Γ
T : Type ?u.171202
inst✝⁶ : TopologicalSpace T
inst✝⁵ : MulAction Γ T
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : AddMonoid α
inst✝² : DistribMulAction G₀ α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousConstSMul G₀ α
s : Set α
c : G₀
hc : c ≠ 0
⊢ c • s ∈ 𝓝 0 ↔ c • s ∈ 𝓝 (c • 0)
rw [smul_zero]