M : Type u_1
N : Type ?u.359964
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
⊢ 0 ∈ closure ↑S
M : Type u_1
N : Type ?u.359964
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
⊢ ‖0‖ = 0
erw [quotient_norm_eq_zero_iff]
no goals
M : Type u_1
N : Type ?u.359964
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
⊢ 0 ∈ closure ↑S
exact subset_closure S.zero_mem