V : Type ?u.313710
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.313719
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
x✝ : V₁
⊢ ‖↑0 x✝‖ = 0
V : Type ?u.313710
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.313719
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
x✝ : V₁
⊢ ‖↑0 x✝‖ = 0 * ‖x✝‖
rw [zero_mul]
no goals
V : Type ?u.313710
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.313719
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
x✝ : V₁
⊢ ‖↑0 x✝‖ = 0
exact norm_zero